[FranzleHHWZ11]
Measurability and safety verification for stochastic hybrid
systems
In Proceedings of the 14th ACM International Conference on
Hybrid Systems: Computation and Control (HSCC), pages 43-52, ACM, 2011.
Downloads: pdf, bibURL: http://doi.acm.org/10.1145/1967701.1967710
Abstract. Dealing with the interplay of randomness and continuous time is
important for the formal verification of many real systems. Considering both
facets is especially important for wireless sensor networks, distributed
control applications, and many other systems of growing importance. An
important traditional design and verification goal for such systems is to
ensure that unsafe states can never be reached. In the stochastic setting,
this translates to the question whether the probability to reach unsafe states
remains tolerable. In this paper, we consider stochastic hybrid systems where
the continuous-time behaviour is given by differential equations, as for usual
hybrid systems, but the targets of discrete jumps are chosen by probability
distributions. These distributions may be general measures on state sets. Also
non-determinism is supported, and the latter is exploited in an abstraction
and evaluation method that establishes safe upper bounds on reachability
probabilities. To arrive there requires us to solve semantic intricacies as
well as practical problems. In particular, we show that measurability of a
complete system follows from the measurability of its constituent parts. On
the practical side, we enhance tool support to work effectively on such
general models. Experimental evidence is provided demonstrating the
applicability of our approach on three case studies, tackled using a
prototypical implementation.