Hybrid automaton

From Wikipedia, the free encyclopedia

A hybrid automaton (plural hybrid automata) is a mathematical model for precisely describing systems where computational processes interact with physical processes. Its behavior consists of discrete state transitions and continuous evolution.

Contents

[edit] Examples

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 (on/off); 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 controller, mobile robots, and processes from systems biology.

[edit] Definition

Informally, a hybrid automaton is a (possibly infinite) state machine augmented with differential equations. It is a standard model for describing a hybrid system. Several different but equivalent formal definitions exist.

[edit] 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 systems model checking. The HyTech 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.

[edit] References

  • Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine The algorithmic analysis of hybrid systems. Theoretical Computer Science, volume 138(1), pages 3--34,1995.
  • Nancy Lynch, Roberto Segala, Frits Vaandrager, Hybrid I/O Automata.Information and Computation, volume 185(1), pages 103-157, 2003.