Olivier Roux and Vlad Rusu. Uniformity for the Decidability of Hybrid Automata. In International Static Analysis Symposium (SAS'96), Aachen (Germany), pp 301-316, 1996. LNCS 1145.
Abstract
We present some decidability results on the verification of hybrid
automata by symbolic analysis (abstract interpretation using polyhedra). The
results include defining a class of hybrid automata for which all properties
expressed in the logic TCTL are decidable. The obtained class of automata is
shown powerful enough to model reactive applications in which every task
eventually terminates within bounded time. Indeed, the restrictions we use
for obtaining decidability have a physical meaning, and they all impose some
kind of uniformity to the runs of hybrid automata.
Full postscript text.