A simple example is a room-thermostat-heater system where the temperature of the room evolves according to laws of thermodynamics and the state of the heater ; the thermostat senses the temperature, performs certain computations and turns the heater on and off. In general, hybrid automata have been used to model and analyze a variety of embedded systems including vehicle control systems, air traffic control systems, mobile robots, and processes from systems biology.
Formal Definition
An Alur-Henzinger hybrid automaton comprises the following components:
A finite set of real-numbered variables. The number is called the dimension of. Let be the set of dotted variables that represent first derivatives during continuous change, and let be the set of primed variables that represent values at the conclusion of discrete change.
A finite multidigraph. The vertices in are called control modes. The edges in are called control switches.
Three vertex labeling functions init, inv, and flow that assign to each control mode three predicates. Each initial conditioninit is a predicate whose free variables are from. Each invariant condition inv is a predicate whose free variables are from. Each flow condition flow is a predicate whose free variables are from.
An edge labeling function jump that assigns to each control switch a predicate. Each jump condition jump is a predicate whose free variables are from.
A finite set of events, and an edge labeling function event: that assigns to each control switch an event.
Related models
Hybrid automata come in several flavors: The Alur-Henzinger hybrid automaton is a popular model; it was developed primarily for algorithmic analysis of hybrid systemsmodel checking. The model checking tool is based on this model. The Hybrid Input/Output Automaton model has been developed more recently. This model enables compositional modeling and analysis of hybrid systems. Another formalism which is useful to model implementations of hybrid automaton is the lazy linear hybrid automaton.
Decidable Subclass of Hybrid Automata
Given the expressiveness of hybrid automata it is not surprising that simple reachability questions are undecidable for general hybrid automata. In fact, a straightforward reduction from Counter machine to three variables hybrid automata proves the undecidablity of the reachability problem for hybrid automata. A sub-class of hybrid automata are timed automata where all of the variables grow with uniform rate. Such restricted variables can act as timer variables, called clocks, and permit modeling of real-time systems. Other notable decidable subclasses include initialized rectangular hybrid automata, one-dimensional piecewise-constant derivatives systems, priced timed automata, and constant-rate multi-mode systems.
