Safety Verification for Probabilistic Hybrid Systems

0351300 - ÚI 2011 RIV DE eng C - Konferenční příspěvek (zahraniční konf.)
Zhang, L. - She, Z. - Ratschan, Stefan - Hermanns, H. - Hahn, E.M.
Safety Verification for Probabilistic Hybrid Systems.
CAV 2010. Computer Aided Verification. Berlin: Springer, 2010 - (Touili, T.; Cook, B.; Jackson, P.), s. 196-211. Lecture Notes in Computer Science, 6174. ISBN 978-3-642-14294-9. ISSN 0302-9743.
[CAV 2010. International conference on Computer Aided Verification /55./. Edinburgh (GB), 15.07.2010-19.07.2010]
Grant CEP: GA ČR GC201/08/J020
Výzkumný záměr: CEZ:AV0Z10300504
Klíčová slova: verification * hybrid dynamical systems
Kód oboru RIV: IN - Informatika

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.
Trvalý link: http://hdl.handle.net/11104/0191084