## The Theory of Hybrid Automata

*
Thomas A. Henzinger*

Hybrid automata, which combine discrete transition graphs with
continuous dynamical systems, are mathematical models for digital
systems that interact with analog environments. Hybrid automata can
be viewed as infinite-state transition systems, and this view gives
insights into the structure of hybrid state spaces. For example, for
certain interesting classes of hybrid automata, language equivalence,
mutual similarity, or bisimilarity induce finite quotients of infinite
state spaces. These results can be exploited by analysis techniques
for finite-state systems.

We summarize several recent results about hybrid automata. Our goal
is to demonstrate that concepts from the theory of discrete concurrent
systems can give insights into partly continuous systems, and that
methods for the verification of finite-state systems can be used to
analyze certain systems with uncountable state spaces.

*Proceedings of the
11th Annual Symposium on Logic in Computer Science*
(LICS), IEEE Computer Society Press, 1996, pp. 278-292.
An extended version appeared in
*Verification of Digital and Hybrid Systems*
(M.K. Inan, R.P. Kurshan, eds.),
NATO ASI Series F: Computer and Systems Sciences,
Vol. 170,
Springer, 2000, pp. 265-292.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1996 IEEE,
2000 Springer.