Safety verification for probabilistic hybrid systems

Lijun Zhang*, Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst Moritz Hahn

*Corresponding author for this work

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

33 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings
EditorsTayssir Touili, Byron Cook, Paul Jackson
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages196-211
Number of pages16
ISBN (Electronic)978-3-642-14295-6
ISBN (Print)978-3-642-14294-9
DOIs
Publication statusPublished - 2010
Externally publishedYes
Event22nd International Conference on Computer Aided Verification, CAV 2010 - Edinburgh, United Kingdom
Duration: 15 Jul 201019 Jul 2010
Conference number: 22

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6174
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference22nd International Conference on Computer Aided Verification, CAV 2010
Abbreviated titleCAV 2020
CountryUnited Kingdom
CityEdinburgh
Period15/07/1019/07/10

Fingerprint

Dive into the research topics of 'Safety verification for probabilistic hybrid systems'. Together they form a unique fingerprint.

Cite this