## Hybrid Automata with Finite Bisimulations

*
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 *B*^{n} and a euclidean automaton
with a continuous dynamics on the infinite state space
*R*^{n}. 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.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1995 Springer.