[HahnNPWZ11]
Game-based Abstraction and Controller Synthesis for Probabilistic
Hybrid Systems
In Eighth International Conference on Quantitative Evaluation
of Systems (QEST), pages 69-78, IEEE Computer Society, 2011.
Downloads: pdf, bibURL: http://doi.ieeecomputersociety.org/10.1109/QEST.2011.17
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.