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

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F10%3A00344069" target="_blank" >RIV/67985807:_____/10:00344069 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Safety Verification of Non-linear Hybrid Systems is Quasi-Semidecidable
Original language description
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.
Czech name
—
Czech description
—

Project
<a href="/en/project/GC201%2F08%2FJ020" target="_blank" >GC201/08/J020: Verification of Hybrid Systems - Exploiting the Synergy with Underlying Constraint Solving Technology</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2010
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)