Content deleted Content added
m compound modifier |
|||
| (56 intermediate revisions by 45 users not shown) | |||
Line 1:
In [[automata theory]], a '''hybrid automaton''' (plural: ''hybrid automata'' or ''hybrid automatons'') is a [[mathematical model]] for precisely describing [[hybrid system|hybrid systems]], for instance systems in which digital computational processes interact with analog physical processes. A hybrid automaton is a [[finite-state machine]] 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==
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 [http://www-cad.eecs.berkeley.edu/~tah/HyTech/ 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.▼
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 control]] systems, [[mobile robots]], and processes from [[systems biology]].
==Formal definition==
===References===▼
* A finite set <math>X = \{x_1, ..., x_n\}</math> of real-numbered variables. The number <math>n</math> is called the ''dimension'' of <math>H</math>. Let <math>\dot{X}</math> be the set <math>\{\dot{x}_1, . . . , \dot{x}_n\}</math> of dotted variables that represent first derivatives during continuous change, and let <math>X'</math> be the set <math>\{x'_1, ..., x'_n\}</math> of primed variables that represent values at the conclusion of discrete change.
*Nancy Lynch, Roberto Segala, Frits Vaandrager, ''Hybrid I/O Automata''.Information and Computation, volume 185(1), pages 103-157, 2003.▼
* A finite [[multidigraph]] <math>(V, E)</math>. The vertices in <math>V</math> are called ''control modes''. The edges in <math>E</math> are called ''control switches''.
* Three vertex labeling functions ''init'', ''inv'', and ''flow'' that assign to each control mode <math>v\in V</math> three predicates. Each initial condition ''init''<math>(v)</math> is a predicate whose free variables are from <math>X</math>. Each invariant condition ''inv''<math>(v)</math> is a predicate whose free variables are from <math>X</math>. Each flow condition ''flow''<math>(v)</math> is a predicate whose free variables are from <math>X\cup \dot{X}</math>.
So this is a [[labeled multidigraph]].
* An edge labeling function ''jump'' that assigns to each control switch <math>e\in E</math> a predicate. Each jump condition ''jump''<math>(e)</math> is a predicate whose free variables are from <math>X\cup X'</math>.
* A finite set <math>\Sigma</math> of events, and an edge labeling function ''event'': <math>E \rightarrow \Sigma</math> that assigns to each control switch an event.
==Related models==
▲Hybrid automata come in several flavors: The '''
==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]]s to three variables hybrid automata (two variables for storing counter values and one to restrict spending a unit-time per ___location) proves the undecidability of the reachability problem for hybrid automata. A sub-class of hybrid automata are [[timed automaton|timed automata]]<ref>Alur, R. and Dill, D. L. "A Theory of Timed Automata". Theoretical Computer Science (TCS), 126(2), pages 183-235, 1995.</ref> where all of the variables grow with uniform rate (i.e., all continuous variables have derivative 1). 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,<ref>{{Cite journal|date=1998-08-01|title=What's Decidable about Hybrid Automata?|journal=Journal of Computer and System Sciences|language=en|volume=57|issue=1|pages=94–124|doi=10.1006/jcss.1998.1581|issn=0022-0000|last1=Henzinger|first1=Thomas A.|last2=Kopke|first2=Peter W.|last3=Puri|first3=Anuj|last4=Varaiya|first4=Pravin|hdl=1813/7198|hdl-access=free}}</ref> one-dimensional piecewise-constant derivatives (PCD) systems,<ref>{{Citation|last1=Asarin|first1=Eugene|title=On the Decidability of the Reachability Problem for Planar Differential Inclusions|date=2001|work=Hybrid Systems: Computation and Control|pages=89–104|publisher=Springer Berlin Heidelberg|language=en|doi=10.1007/3-540-45351-2_11|isbn=9783540418665|last2=Schneider|first2=Gerardo|last3=Yovine|first3=Sergio|citeseerx=10.1.1.23.8172}}</ref> priced timed automata,<ref>{{Citation|last1=Behrmann|first1=Gerd|title=Priced Timed Automata: Algorithms and Applications|date=2005|work=Formal Methods for Components and Objects|pages=162–182|publisher=Springer Berlin Heidelberg|language=en|doi=10.1007/11561163_8|isbn=9783540291312|last2=Larsen|first2=Kim G.|last3=Rasmussen|first3=Jacob I.|citeseerx=10.1.1.106.7115}}</ref> and constant-rate multi-mode systems.<ref>{{Cite book|last1=Alur|first1=Rajeev|last2=Trivedi|first2=Ashutosh|last3=Wojtczak|first3=Dominik|date=2012-04-17|title=Optimal scheduling for constant-rate multi-mode systems|publisher=ACM|pages=75–84|doi=10.1145/2185632.2185647|isbn=9781450312202|citeseerx=10.1.1.299.946|s2cid=14587340 }}</ref>
== See also ==
*[[Timed automaton]] and [[signal automaton]], two kinds of hybrid automata
<references />
==Further reading==
*[[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
[[Category:Automata (computation)]]
[[Category:Differential equations]]
| |||