Safety Verification for Probabilistic Hybrid Systems

Autoři: doc. Dipl. Ing. Stefan Ratschan, Dr. tech.
Rok vydání: 2010
Typ publikace: Konferenční příspěvek (mezinárodní konf.)
Periodikum: CAV 2010. Computer Aided Verification
Projekty: Verifikace hybridních systémů využitím spolupráce s řešením omezujících podmínek
Bibliografická citace: 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

Abstrakt

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.