Citation
Dave Parker. "Probabilistic Model Checking andS trategy Synthesis". Talk or presentation, 28, October, 2014.

Abstract
Probabilistic model checking is an automated technique to verify whether a probabilistic system, e.g., a robot operating in an unknown environment, satisfies a temporal logic property, e.g., "the minimum probability of completing the task within 15 minutes is above 0.98". Dually, we can also synthesise, from a model and a property specification, a strategy for controlling the system in order to satisfy or optimise the property. This talk will give an overview of automated verification and strategy synthesis for probabilistic systems, and present some recent advances in this area, including: multi-objective model checking (to investigate trade-offs between several conflicting properties), extensions to stochastic game models (to model competitive or collaborative behaviour) and permissive strategy synthesis (to generate flexible and robust controllers). I will describe the tool support for these techniques, in the form of the probabilistic model checker PRISM and its extensions, and present results from the application of these techniques to examples such as robotic motion planning, dynamic power management controllers and task scheduling.

Electronic downloads

• dave-berkeley-nov14.pdf · application/pdf · 3020 kbytes

• HTML

  Dave Parker. <a
  href="http://chess.eecs.berkeley.edu/pubs/1079.html"
  ><i>Probabilistic Model Checking andS trategy
  Synthesis</i></a>, Talk or presentation,  28,
  October, 2014.

• Plain text

  Dave Parker. "Probabilistic Model Checking andS trategy
  Synthesis". Talk or presentation,  28, October, 2014.

• BibTeX

  @presentation{Parker14_ProbabilisticModelCheckingAndSTrategySynthesis,
      author = {Dave Parker},
      title = {Probabilistic Model Checking andS trategy Synthesis},
      day = {28},
      month = {October},
      year = {2014},
      abstract = {Probabilistic model checking is an automated
                technique to verify whether a probabilistic
                system, e.g., a robot operating in an unknown
                environment, satisfies a temporal logic property,
                e.g., "the minimum probability of completing the
                task within 15 minutes is above 0.98". Dually, we
                can also synthesise, from a model and a property
                specification, a strategy for controlling the
                system in order to satisfy or optimise the
                property. This talk will give an overview of
                automated verification and strategy synthesis for
                probabilistic systems, and present some recent
                advances in this area, including: multi-objective
                model checking (to investigate trade-offs between
                several conflicting properties), extensions to
                stochastic game models (to model competitive or
                collaborative behaviour) and permissive strategy
                synthesis (to generate flexible and robust
                controllers). I will describe the tool support for
                these techniques, in the form of the probabilistic
                model checker PRISM and its extensions, and
                present results from the application of these
                techniques to examples such as robotic motion
                planning, dynamic power management controllers and
                task scheduling.},
      URL = {http://chess.eecs.berkeley.edu/pubs/1079.html}
  }
  

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