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

Autoři: doc. Dipl. Ing. Stefan Ratschan, Dr. tech.
Rok vydání: 2010
Typ publikace: Konferenční příspěvek (mezinárodní konf.)
Periodikum: Theory and Applications of Models of Computation
Projekty: Verifikace hybridních systémů využitím spolupráce s řešením omezujících podmínek
Bibliografická citace: RATSCHAN, Stefan. Safety Verification of Non-linear Hybrid Systems is Quasi-Semidecidable. In: KRATOCHVÍL, J., LI, A., FIALA, J., KOLMAN, P., eds. Theory and Applications of Models of Computation. Berlin: Springer, 2010, S. 397-408. Lecture Notes in Computer Science, 6108. ISBN 978-3-642-13561-3. ISSN 0302-9743
Dostupné z: doi:10.1007/978-3-642-13562-0_36
DOI: 10.1007/978-3-642-13562-0_36
ID: 344069

Abstrakt

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.