Decidable Hybrid Systems

. One of the most important analysis problems of hybrid systems is the reachability problem. State of the art computational tools perform reachability computation for timed automata, multirate automata, and rectangular automata. In this paper, we extend the decidability frontier for classes of linear hybrid systems, which are introduced as hybrid systems with linear vector fields in each discrete location. This extension is important given the applicability of linear vector fields in control systems. This result is achieved by showing that any such hybrid system admits a finite bisimulation, and by providing an algorithm that computes it using decision methods from mathematical logic. Keywords: Hybrid systems, reachability, decidability, bisimulations, o-minimality 1. Introduction Technological advances in computation and communication allow the control of large scale, multiagent, and concurrent systems, like automated highway systems, air traffic management systems, manufacturing, an..