Measurability and safety verification for stochastic hybrid systems

Martin Fränzle, Ernst Moritz Hahn, Holger Hermanns, Nicolás Wolovick, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

49 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationProceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011
Pages43-52
Number of pages10
DOIs
Publication statusPublished - 2011
Externally publishedYes

Fingerprint Dive into the research topics of 'Measurability and safety verification for stochastic hybrid systems'. Together they form a unique fingerprint.

  • Cite this

    Fränzle, M., Hahn, E. M., Hermanns, H., Wolovick, N., & Zhang, L. (2011). Measurability and safety verification for stochastic hybrid systems. In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011 (pp. 43-52) https://doi.org/10.1145/1967701.1967710