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.



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.