The Theory of Hybrid Automata

Ahybrid automatonis a formalmodelfor a mixeddiscrete-continuous system. We classify hybrid automata acoording to what questions about their behavior can be answered algorithmically. The classi cation reveals structure on mixed discrete-continuous state spaces that was previously studied on purely discrete state spaces only. In particular, various classes of hybrid automata induce nitary trace equivalence (or similarity, or bisimilarity) relations on an uncountable state space, thus permitting the application of various model-checking techniques that were originally developed for nite-state systems. 1 Hybrid Automata A hybrid system is a dynamical system with both discrete and continuous components. For example, an automobile engine whose fuel injection (continuous) is regulated by a microprocessor (discrete) is a hybrid system. As embedded computing becomes ubiquitous, hybrid systems are increasingly employed in safety-critical applications, thus making reliability a prime concern. Rig...

• Type: Conference
• Year: 1996
• Where: LICS
• Authors: Thomas A. Henzinger
• Keywords: Automated Reasoning, Hybrid Automata, Hybrid Systems, LICS 1996, State Space