[ZhangSRHH12]
Safety Verification for Probabilistic Hybrid Systems
In European Journal of Control, 18: 572-587, 2012.
Downloads: pdf, bibURL: http://dx.doi.org/10.3166/ejc.18.572-587
Abstract. The interplay of random phenomena and continuous dynamics
deserves increased attention, especially in the context of wireless sensing
and control applications. Safety verification for such systems thus needs to
consider probabilistic variants 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. Moreover, being based on 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.