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.