*banner
 

Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties and its Application to Cyber-Physical Systems
Puggelli Alberto

Citation
Puggelli Alberto . "Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties and its Application to Cyber-Physical Systems". Talk or presentation, 26, November, 2013.

Abstract
Accurate modeling of cyber-physical systems (CPS) is a notoriously challenging problem due, among other reasons, to the intrinsic limitations in representing the physical part of the system, whose behavior can only be inferred through finite resolution measurements. The problem is even exacerbated in the context of the formal verification of these system, where the generated guarantees on the system properties are only as accurate as the model itself. In this talk, we present a framework that allows the formal verification of quantitative properties of CPS while taking into account uncertainties in the modeling process. We first present the model of Convex Markov Decision Processes (CMDPs), i.e., MDPs in which transition probabilities are only known to lie in convex uncertainty sets. These convex sets can be used to formally capture the uncertainties that are present in the modeling process. Using results on strong duality for convex programs, we then present a verification algorithm for Probabilistic Computation Tree (PCTL) properties of CMDPs, and prove that it runs in time polynomial in the size of a CMDP for a rich subclass of convex uncertainty models. This result allows us to lower the previously known algorithmic complexity upper bound for PCTL properties of CMDPs from co-NP to PTIME. We conclude the talk by describing how we recently applied the proposed technique to the verification of the behavior of car drivers performing complex maneuvers. Results show that we can quantitatively evaluate the performance of the drivers depending on their attention level, i.e., whether they are attentive or distracted while driving. The proposed framework is currently being added to the public distribution of PRISM, the state-of-the-art tool for the probabilistic verification of stochastic systems.

Electronic downloads

Citation formats  
  • HTML
    Puggelli Alberto . <a
    href="http://chess.eecs.berkeley.edu/pubs/1046.html"
    ><i>Polynomial-Time Verification of PCTL Properties
    of MDPs with Convex Uncertainties and its Application to
    Cyber-Physical Systems</i></a>, Talk or
    presentation,  26, November, 2013.
  • Plain text
    Puggelli Alberto . "Polynomial-Time Verification of
    PCTL Properties of MDPs with Convex Uncertainties and its
    Application to Cyber-Physical Systems". Talk or
    presentation,  26, November, 2013.
  • BibTeX
    @presentation{Alberto13_PolynomialTimeVerificationOfPCTLPropertiesOfMDPsWith,
        author = {Puggelli Alberto },
        title = {Polynomial-Time Verification of PCTL Properties of
                  MDPs with Convex Uncertainties and its Application
                  to Cyber-Physical Systems},
        day = {26},
        month = {November},
        year = {2013},
        abstract = {Accurate modeling of cyber-physical systems (CPS)
                  is a notoriously challenging problem due, among
                  other reasons, to the intrinsic limitations in
                  representing the physical part of the system,
                  whose behavior can only be inferred through finite
                  resolution measurements. The problem is even
                  exacerbated in the context of the formal
                  verification of these system, where the generated
                  guarantees on the system properties are only as
                  accurate as the model itself. In this talk, we
                  present a framework that allows the formal
                  verification of quantitative properties of CPS
                  while taking into account uncertainties in the
                  modeling process. We first present the model of
                  Convex Markov Decision Processes (CMDPs), i.e.,
                  MDPs in which transition probabilities are only
                  known to lie in convex uncertainty sets. These
                  convex sets can be used to formally capture the
                  uncertainties that are present in the modeling
                  process. Using results on strong duality for
                  convex programs, we then present a verification
                  algorithm for Probabilistic Computation Tree
                  (PCTL) properties of CMDPs, and prove that it runs
                  in time polynomial in the size of a CMDP for a
                  rich subclass of convex uncertainty models. This
                  result allows us to lower the previously known
                  algorithmic complexity upper bound for PCTL
                  properties of CMDPs from co-NP to PTIME. We
                  conclude the talk by describing how we recently
                  applied the proposed technique to the verification
                  of the behavior of car drivers performing complex
                  maneuvers. Results show that we can quantitatively
                  evaluate the performance of the drivers depending
                  on their attention level, i.e., whether they are
                  attentive or distracted while driving. The
                  proposed framework is currently being added to the
                  public distribution of PRISM, the state-of-the-art
                  tool for the probabilistic verification of
                  stochastic systems.},
        URL = {http://chess.eecs.berkeley.edu/pubs/1046.html}
    }
    

Posted by Armin Wasicek on 6 Jan 2014.
Groups: chessworkshop
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

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.

©2002-2018 Chess