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.
Semi-Algebraic Constant Reset Hybrid Automata - SACoRe / Casagrande, Alberto; Piazza, C; Mishra, B.. - STAMPA. - (2005), pp. 678-683. ( 44th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC) Seville, Spain December 12-15, 2005) [10.1109/CDC.2005.1582234].
Semi-Algebraic Constant Reset Hybrid Automata - SACoRe
CASAGRANDE, ALBERTO;
2005-01-01
Abstract
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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
