Measurability and safety verification for stochastic hybrid systems

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

54 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 publicationHSCC'11 - Proceedings of the 2011 ACM/SIGBED Hybrid Systems
Subtitle of host publicationComputation and Control
Pages43-52
Number of pages10
DOIs
Publication statusPublished - 2011
Externally publishedYes
Event14th International Conference on Hybrid Systems: Computation and Control, HSCC 2011 - Chicago, United States
Duration: 12 Apr 201114 Apr 2011
Conference number: 14

Conference

Conference14th International Conference on Hybrid Systems: Computation and Control, HSCC 2011
Abbreviated titleHSCC 2011
CountryUnited States
CityChicago
Period12/04/1114/04/11

Fingerprint

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

Cite this