Safety Verification of Non-linear Hybrid Systems is Quasi-Semidecidable

0344069 - ÚI 2011 RIV DE eng C - Conference Paper (international conference)
Ratschan, Stefan
Safety Verification of Non-linear Hybrid Systems is Quasi-Semidecidable.
Theory and Applications of Models of Computation. Berlin: Springer, 2010 - (Kratochvíl, J.; Li, A.; Fiala, J.; Kolman, P.), s. 397-408. Lecture Notes in Computer Science, 6108. ISBN 978-3-642-13561-3. ISSN 0302-9743.
[TAMC 2010. Theory and Applications of Models of Computation Annual Conference /7./. Prague, (CZ), 07.06.2010-11.06.2010]
R&D Projects: GA ČR GC201/08/J020
Institutional research plan: CEZ:AV0Z10300504
Keywords : verification * hybrid systems * decidebility
Subject RIV: IN - Informatics, Computer Science

Safety verification of hybrid systems is undecidable, except for very special cases. In this paper, we circumvent undecidability by providing an algorithm that can verify safety and provably terminates for all robust and safe problem instances. It need not necessarily terminate for problem instances that are unsafe or non-robust. A problem instance x is robust iff the given property holds not only for x itself, but also when x is perturbed a little bit. Since, in practice, well-designed hybrid systems are usually robust, this implies that the algorithm terminates for the cases occurring in practice. In contrast to earlier work, our result holds for a very general class of hybrid systems, and it uses a continuous time model.
Permanent Link: http://hdl.handle.net/11104/0186379