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 proceedingArticle in proceedingsResearchpeer-review

    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 international conference on Hybrid systems: computation and control
    PublisherAssociation for Computing Machinery
    Publication date2011
    Pages43-52
    ISBN (Print)9781450306294
    DOIs
    Publication statusPublished - 2011
    EventInternational Conference on Hybrid Systems : Computation and Control - Chicago, Illinois, USA
    Duration: 1 Jan 2011 → …
    Conference number: 14

    Conference

    ConferenceInternational Conference on Hybrid Systems : Computation and Control
    Number14
    CityChicago, Illinois, USA
    Period01/01/2011 → …

    Fingerprint

    Dive into the research topics of 'Measurability and Safety Verification for Stochastic Hybrid Systems'. Together they form a unique fingerprint.

    Cite this