Game-based abstraction and controller synthesis for probabilistic hybrid systems

Ernst Moritz Hahn*, Gethin Norman, David Parker, Björn Wachter, Lijun Zhang

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

17 Citations (Scopus)

Abstract

We consider a class of hybrid systems that involve random phenomena, in addition to discrete and continuous behaviour. Examples of such systems include wireless sensing and control applications. We propose and compare two abstraction techniques for this class of models, which yield lower and upper bounds on the optimal probability of reaching a particular class of states. We also demonstrate the applicability of these abstraction techniques to the computation of long-run average reward properties and the synthesis of controllers. The first of the two abstractions yields more precise information, while the second is easier to construct. For the latter, we demonstrate how existing solvers for hybrid systems can be leveraged to perform the computation.

Original languageEnglish
Title of host publication20118th International Conference on Quantitative Evaluation of Systems, QEST 2011
Place of PublicationPiscataway, NJ
PublisherIEEE
Pages69-78
Number of pages10
ISBN (Print)978-1-4577-0973-9
DOIs
Publication statusPublished - 2011
Externally publishedYes
Event8th International Conference on Quantitative Evaluation of SysTems, QEST 2011 - RWTH Aachen University, Aachen, Germany
Duration: 5 Sep 20118 Sep 2011
Conference number: 8

Conference

Conference8th International Conference on Quantitative Evaluation of SysTems, QEST 2011
Abbreviated titleQEST
CountryGermany
CityAachen
Period5/09/118/09/11

Keywords

  • abstraction refinement
  • controller synthesis
  • long-run average
  • probabilistic hybrid systems
  • probabilistic reachability
  • stochastic games

Fingerprint Dive into the research topics of 'Game-based abstraction and controller synthesis for probabilistic hybrid systems'. Together they form a unique fingerprint.

Cite this