In automata theory

Automata theory

In theoretical computer science, automata theory is the study of abstract machines and the computational problems that can be solved using these machines. These abstract machines are called automata...

, a hybrid automaton (plural: hybrid automata or hybrid automatons) is a mathematical model for precisely describing systems in which digital computational processes interact with analog physical processes. A hybrid automaton is a finite state machine

Finite state machine

A finite-state machine or finite-state automaton , or simply a state machine, is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states...

 with a finite set of continuous variables whose values are described by a set of ordinary differential equations. This combined specification of discrete and continuous behaviors enables dynamic systems that comprise both digital and analog components to be modeled and analyzed.

Examples

A simple example is a room-thermostat-heater system where the temperature of the room evolves according to laws of thermodynamics

Thermodynamics

Thermodynamics is a physical science that studies the effects on material bodies, and on radiation in regions of space, of transfer of heat and of work done on or by the bodies or radiation...

 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 control

Air traffic control

Air traffic control is a service provided by ground-based controllers who direct aircraft on the ground and in the air. The primary purpose of ATC systems worldwide is to separate aircraft to prevent collisions, to organize and expedite the flow of traffic, and to provide information and other...

 systems, mobile robots, and processes from systems biology

Systems biology

Systems biology is a term used to describe a number of trends in bioscience research, and a movement which draws on those trends. Proponents describe systems biology as a biology-based inter-disciplinary study field that focuses on complex interactions in biological systems, claiming that it uses...

.

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 directed multigraph . 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 condition init 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 systems model checking

Model checking

In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

. 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. Another formalism which is useful to model implementations of hybrid automaton is the lazy linear hybrid automaton

Lazy linear hybrid automaton

Lazy linear hybrid automata model the discrete time behavior of control systems containing finite-precision sensors and actuators interacting with their environment under bounded inertial delays. The model permits only linear flow constraints but the invariants and guards can be any computable...

.

Further Reading

• Rajeev Alur
  Rajeev Alur
  Rajeev Alur is a researcher in the field of formal methods for modeling and analyzing programs and systems, in particular model checking. His contributions include timed automation and temporal specifications based on languages of nested words and trees. He is Zisman Family professor of Computer...
  
  , 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
  Nancy Lynch
  Nancy Ann Lynch is a professor at the Massachusetts Institute of Technology. She is the NEC Professor of Software Science and Engineering in the EECS department and heads the Theory of Distributed Systems research group at MIT's Computer Science and Artificial Intelligence Laboratory.She is the...
  
  , Roberto Segala, Frits Vaandrager, Hybrid I/O Automata. Information and Computation, volume 185(1), pages 103–157, 2003.