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". Talk or presentation, 5, November, 2013; Poster presented at the 2013 TerraSwarm Annual Meeting.

Abstract
We address 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. We first introduce the model of Convex-MDPs (CMDPs), i.e., MDPs with convex uncertainty sets. Using results on strong duality for convex programs, we then present a PCTL verification algorithm for CMDPs, and prove that it runs in time polynomial in the size of a CMDP. This result allows us to lower the previously known algorithmic complexity upper bound for CMDPs from co-NP to PTIME. We validate the proposed approach on two case studies: the verification of a consensus protocol and of 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/162.html"><i>Polynomial-Time
  Verification of PCTL Properties of MDPs with Convex
  Uncertainties</i></a>, Talk or presentation,  5,
  November, 2013; Poster presented at the <a
  href="http://www.terraswarm.org/conferences/13/annual"
  >2013 TerraSwarm Annual Meeting</a>.

• Plain text

  Alberto Puggelli, Wenchao Li, Alberto
  Sangiovanni-Vincentelli, Sanjit Seshia.
  "Polynomial-Time Verification of PCTL Properties of
  MDPs with Convex Uncertainties". Talk or presentation, 
  5, November, 2013; Poster presented at the <a
  href="http://www.terraswarm.org/conferences/13/annual"
  >2013 TerraSwarm Annual Meeting</a>.

• BibTeX

  @presentation{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},
      day = {5},
      month = {November},
      year = {2013},
      note = {Poster presented at the <a
                href="http://www.terraswarm.org/conferences/13/annual"
                >2013 TerraSwarm Annual Meeting</a>.},
      abstract = {We address 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. We first introduce the model of
                Convex-MDPs (CMDPs), i.e., MDPs with convex
                uncertainty sets. Using results on strong duality
                for convex programs, we then present a PCTL
                verification algorithm for CMDPs, and prove that
                it runs in time polynomial in the size of a CMDP.
                This result allows us to lower the previously
                known algorithmic complexity upper bound for CMDPs
                from co-NP to PTIME. We validate the proposed
                approach on two case studies: the verification of
                a consensus protocol and of a dynamic
                configuration protocol for IPv4 addresses. },
      URL = {http://terraswarm.org/pubs/162.html}
  }
  

Posted by Alberto Puggelli on 3 Nov 2013.
Groups: tools