Počet záznamů: 1

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

  1. 1.
    0344069 - UIVT-O 2011 RIV DE eng C - Konferenční příspěvek (zahraniční konf.)
    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]
    Grant CEP: GA ČR GC201/08/J020
    Výzkumný záměr: CEZ:AV0Z10300504
    Klíčová slova: verification * hybrid systems * decidebility
    Kód oboru RIV: IN - Informatika

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