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