Semi-Algebraic Constant Reset Hybrid Automata - SACoRe


In this paper we introduce and study a special class of hybrid automata, Semi-Algebraic Constant Reset hybrid automata (SACoRe). SACoRe automata are an extension of O-minimal semi-algebraic automata over the reals in the case of flows obtained from non-autonomous systems of differential inclusions. Even though SACoRe automata do not have the finite bisimulation property, they do admit decision procedures for reachability and model checking for a limited fragment of CTL, by combining Tarski’s decidability result over the reals and Michael’s selection theorem.

Proc. of Joint IEEE Int. Conference on Decision and Control and European Control Conference (CDC-ECC'05)