[ZhangSRHH10]
Safety Verification for Probabilistic Hybrid Systems
In Computer Aided Verification, 22nd International Conference (CAV), pages 196-211, Springer, Lecture Notes in Computer Science 6174, 2010.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-14295-6_21
Abstract. The interplay of random phenomena and continuous real-time
control deserves increased attention for instance in wireless sensing and
control applications. Safety verification for such systems thus needs to
consider probabilistic variations of systems with hybrid dynamics. In safety
verification of classical hybrid systems we are interested in whether a
certain set of unsafe system states can be reached from a set of initial
states. In the probabilistic setting, we may ask instead whether the
probability of reaching unsafe states is below some given threshold. In this
paper, we consider probabilistic hybrid systems and develop a general
abstraction technique for verifying probabilistic safety problems. This gives
rise to the first mechanisable technique that can, in practice, formally
verify safety properties of non-trivial continuous-time stochastic hybrid
systems - without resorting to point-wise discretisation. Moreover, being
based on arbitrary abstractions computed by tools for the analysis of
non-probabilistic hybrid systems, improvements in effectivity of such tools
directly carry over to improvements in effectivity of the technique we
describe. We demonstrate the applicability of our approach on a number of
case studies, tackled using a prototypical implementation.