Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
Alberto Puggelli, Wenchao Li, Alberto Sangiovanni-Vincentelli, Sanjit Seshia

Citation
Alberto Puggelli, Wenchao Li, Alberto Sangiovanni-Vincentelli, Sanjit Seshia. "Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties". Proceedings of CAV 2013, July, 2013.

Abstract
The paper addresses the problem of verifying Probabilistic Computation Tree Logic (PCTL) properties of Markov Decision Processes (MDPs) whose state transition probabilities are only known to lie within uncertainty sets. First, the model of Convex-MDPs (CMDPs), i.e., MDPs with convex uncertainty sets,is introduced. CMDPs generalize Interval-MDPs (IMDPs) by allowing also more expressive (convex) descriptions of uncertainty. Using results on strong duality for convex programs, a PCTL verification algorithm for CMDPs is then presented, and proved to run in time polynomial in the size of a CMDP for a rich subclass of convex uncertainty models. This result lowers the previously known algorithmic complexity upper bound for IMDPs from co-NP to PTIME. The practical effectiveness of the proposed approach is demonstrated by verifying a consensus protocol and a dynamic configuration protocol for IPv4 addresses.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Alberto  Puggelli, Wenchao Li, Alberto
  Sangiovanni-Vincentelli, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/52.html"
  >Polynomial-Time Verification of PCTL Properties of MDPs
  with Convex Uncertainties</a>, Proceedings of CAV
  2013, July, 2013.

• Plain text

  Alberto  Puggelli, Wenchao Li, Alberto
  Sangiovanni-Vincentelli, Sanjit Seshia.
  "Polynomial-Time Verification of PCTL Properties of
  MDPs with Convex Uncertainties". Proceedings of CAV
  2013, July, 2013.

• BibTeX

  @inproceedings{PuggelliLiSangiovanniVincentelliSeshia13_PolynomialTimeVerificationOfPCTLPropertiesOfMDPsWith,
      author = {Alberto  Puggelli and Wenchao Li and Alberto
                Sangiovanni-Vincentelli and Sanjit Seshia},
      title = {Polynomial-Time Verification of PCTL Properties of
                MDPs with Convex Uncertainties},
      booktitle = {Proceedings of CAV 2013},
      month = {July},
      year = {2013},
      abstract = {The paper addresses the problem of verifying
                Probabilistic Computation Tree Logic (PCTL)
                properties of Markov Decision Processes (MDPs)
                whose state transition probabilities are only
                known to lie within uncertainty sets. First, the
                model of Convex-MDPs (CMDPs), i.e., MDPs with
                convex uncertainty sets,is introduced. CMDPs
                generalize Interval-MDPs (IMDPs) by allowing also
                more expressive (convex) descriptions of
                uncertainty. Using results on strong duality for
                convex programs, a PCTL verification algorithm for
                CMDPs is then presented, and proved to run in time
                polynomial in the size of a CMDP for a rich
                subclass of convex uncertainty models. This result
                lowers the previously known algorithmic complexity
                upper bound for IMDPs from co-NP to PTIME. The
                practical effectiveness of the proposed approach
                is demonstrated by verifying a consensus protocol
                and a dynamic configuration protocol for IPv4
                addresses. },
      URL = {http://terraswarm.org/pubs/52.html}
  }
  

Posted by Mila MacBain on 26 Apr 2013.