@article{Ratschan2014,
    Abstract = {Safety verification of hybrid systems is undecidable, except for very special cases. In this paper, we circumvent undecidability by providing a verification algorithm that provably terminates for all robust problem instances, but need not necessarily terminate for non-robust problem instances. 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.},
    Author = {Ratschan, Stefan},
    ISSN = {1572-8102},
    Journal = {Formal Methods in System Design},
    Month = {Feb},
    Number = {1},
    Pages = {71--90},
    Title = {Safety verification of non-linear hybrid systems is quasi-decidable},
    URL = {https://doi.org/10.1007/s10703-013-0196-2},
    Volume = {44},
    Year = {2014},
    bdsk-url-1 = {https://doi.org/10.1007/s10703-013-0196-2},
    bdsk-url-2 = {http://dx.doi.org/10.1007/s10703-013-0196-2},
    date-added = {2017-11-02 09:50:51 +0000},
    date-modified = {2017-11-02 09:50:51 +0000},
    day = {01},
    doi = {10.1007/s10703-013-0196-2}
}

@article{Ratschan2014, Abstract = {Safety verification of hybrid systems is undecidable, except for very special cases. In this paper, we circumvent undecidability by providing a verification algorithm that provably terminates for all robust problem instances, but need not necessarily terminate for non-robust problem instances. 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.}, Author = {Ratschan, Stefan}, ISSN = {1572-8102}, Journal = {Formal Methods in System Design}, Month = {Feb}, Number = {1}, Pages = {71--90}, Title = {Safety verification of non-linear hybrid systems is quasi-decidable}, URL = {https://doi.org/10.1007/s10703-013-0196-2}, Volume = {44}, Year = {2014}, bdsk-url-1 = {https://doi.org/10.1007/s10703-013-0196-2}, bdsk-url-2 = {http://dx.doi.org/10.1007/s10703-013-0196-2}, date-added = {2017-11-02 09:50:51 +0000}, date-modified = {2017-11-02 09:50:51 +0000}, day = {01}, doi = {10.1007/s10703-013-0196-2} }