Safety Verification for Probabilistic Hybrid Systems

Authors: L. Zhang, Z. She, Stefan Ratschan, H. Hermanns, E.M. Hahn
Publication year: 2010
Publication type: Konferenční příspěvek (mezinárodní konf.)
Periodical: CAV 2010. Computer Aided Verification
Projects: Verification of Hybrid Systems - Exploiting the Synergy with Underlying Constraint Solving Technology
Bibliographic citation: ZHANG, L., SHE, Z., RATSCHAN, Stefan, HERMANNS, H., HAHN, E.M. Safety Verification for Probabilistic Hybrid Systems. In: TOUILI, T., COOK, B., JACKSON, P., eds. CAV 2010. Computer Aided Verification. Berlin: Springer, 2010, S. 196-211. Lecture Notes in Computer Science, 6174. ISBN 978-3-642-14294-9. ISSN 0302-9743
Dostupné z: doi:10.1007/978-3-642-14295-6_21
DOI: 10.1007/978-3-642-14295-6_21
ID: 351300

Abstract

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.