Analysis of hybrid systems: An ounce of realism can save an infinity of states

Martin Fränzle, J. Flum (Editor), M. Rodriguez-Artalejo (Editor)

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    95 Downloads (Pure)

    Abstract

    Hybrid automata have been introduced in both control engineering and computer science as a formal model for the dynamics of hybrid discrete-continuous systems. In the case of so-called linear hybrid automata this formalization supports semi-decision procedures for state reachability, yet no decision procedures due to inherent undecidability. Thus, unlike finite or timed automata, already linear hybrid automata are out-of-scope of fully automatic verification. In this article, we devise a new semi-decision method for safety of linear and polynomial hybrid systems which may only fail on pathological, practically uninteresting cases. These remaining cases are such that their safety depends on the complete absence of noise, a situation unlikely to occur in real hybrid systems. Furthermore, we show that if low probability effects of noise are ignored akin to the way they are suppressed in digital modelling then safety becomes fully decidable.
    Original languageEnglish
    Title of host publicationComputer Science Logic (CSL'99)
    PublisherSpringer Verlag
    Publication date1999
    Pages126-140
    Publication statusPublished - 1999
    EventProceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science -
    Duration: 1 Jan 1999 → …

    Conference

    ConferenceProceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science
    Period01/01/1999 → …

    Keywords

    • Hybrid Systems
    • Verification
    • Decision Procedures

    Fingerprint Dive into the research topics of 'Analysis of hybrid systems: An ounce of realism can save an infinity of states'. Together they form a unique fingerprint.

    Cite this