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

• Puggelli_Dreams.pdf · application/pdf · 6608 kbytes

• 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.