Analysis of hybrid systems: An ounce of realism can save an infinity of states. (English) Zbl 0944.68119

Fränzle, Martin

Flum, Jörg (ed.) et al., Computer science logic. 13th international workshop, CSL ’99. 8th annual conference of the EACSL, Madrid, Spain, September 20-25, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1683, 126-140 (1999).

Summary: 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 or 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.
For the entire collection see [Zbl 0929.00039].

MSC:

68Q45

Formal languages and automata

Keywords:

hybrid automata