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

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.