Verification of Bounded Discrete Horizon Hybrid Automata

We consider the class of o-minimally definable hybrid automata with a bounded discrete-transition horizon. We show that for every hybrid automata in this class, there exists a bisimulation of finite index, and that the bisimulation quotient can be effectively constructed when the underlying o-minimal theory is decidable. More importantly, we give natural specifications for hybrid automata which ensure the boundedness of discrete-transition horizons. In addition, we show that these specifications are reasonably tight with respect to the decidability of the models and that they can model modern day real-time and embedded systems. As a result, the analysis of several problems for these systems admit effective algorithms. We provide a representative example of a hybrid automaton in this class. Unlike previously examined subclasses of o-minimally defined hybrid automata with decidable verification properties and extended o-minimal hybrid automata, we do not impose re-initialization of the continuous variables in a memoryless fashion when a discrete transition is taken. Our class of hybrid systems has both rich continuous dynamics and strong discrete-continuous coupling, showing that it is not necessary to either simplify the continuous dynamics or restrict the discrete dynamics to achieve decidability.