Thomas A. Henzinger
The analysis, verification, and control of hybrid automata with finite bisimulations can be reduced to finite-state problems. We advocate a time-abstract, phase-based methodology for checking if a given hybrid automaton has a finite bisimulation. First, we factor the automaton into two components, a boolean automaton with a discrete dynamics on the finite state space Bn and a euclidean automaton with a continuous dynamics on the infinite state space Rn. Second, we investigate the phase portrait of the euclidean component. In this fashion, we obtain new decidability results for hybrid systems as well as new, uniform proofs of known decidability results. For example, we prove that if two hybrid automata have finite bisimulations, and both can be calibrated to a common time scale, then their product also has a finite bisimulation.
Proceedings of the 22nd International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science 944, Springer, 1995, pp. 324-335.