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.