Specifications for Decidable Hybrid Automata and Games
Vladimeros Vladimerou · 2009
Using hybrid automata, one is able to model many types of systems and express their properties in various formal languages. Being extremely general and rich, however, the class of hybrid automata exhibits the inherent problems of automata theory: even the simplest of properties for general hybrid automata are undecidable. Therefore, one must restrict attention only to subclasses of this very general class. The literature to date has seemed to indicate that for a whole subclass of hybrid automata to have decidable properties it would either have to have very simple continuous dynamics (timed automata, piecewise affine inclusions, etc.) or decoupled discrete and continuous dynamics (o-minimal hybrid systems, initialized rectangular automata), where the continuous components of the system are reset in a memoryless manner after each discrete transition. The thesis of this dissertation is that this need not be the case! STORMED hybrid systems are introduced in this dissertation and form a subclass of hybrid automata which lie on the boundary of decidability and admit