Hybrid automaton

Summary

In automata theory, a hybrid automaton (plural: hybrid automata or hybrid automatons) is a mathematical model for precisely describing 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 edit

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 edit

An Alur–Henzinger hybrid automaton   comprises the following components:[1]

  • 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 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  .

So this is a labeled multidigraph.

  • 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 edit

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

Decidable subclass of hybrid automata edit

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 machines 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 automata[2] 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,[3] one-dimensional piecewise-constant derivatives (PCD) systems,[4] priced timed automata,[5] and constant-rate multi-mode systems.[6]

See also edit

References edit

  1. ^ Henzinger, T.A. "The Theory of Hybrid Automata". Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS), pages 278-292, 1996.
  2. ^ Alur, R. and Dill, D. L. "A Theory of Timed Automata". Theoretical Computer Science (TCS), 126(2), pages 183-235, 1995.
  3. ^ Henzinger, Thomas A.; Kopke, Peter W.; Puri, Anuj; Varaiya, Pravin (1998-08-01). "What's Decidable about Hybrid Automata?". Journal of Computer and System Sciences. 57 (1): 94–124. doi:10.1006/jcss.1998.1581. hdl:1813/7198. ISSN 0022-0000.
  4. ^ Asarin, Eugene; Schneider, Gerardo; Yovine, Sergio (2001), "On the Decidability of the Reachability Problem for Planar Differential Inclusions", Hybrid Systems: Computation and Control, Springer Berlin Heidelberg, pp. 89–104, CiteSeerX 10.1.1.23.8172, doi:10.1007/3-540-45351-2_11, ISBN 9783540418665
  5. ^ Behrmann, Gerd; Larsen, Kim G.; Rasmussen, Jacob I. (2005), "Priced Timed Automata: Algorithms and Applications", Formal Methods for Components and Objects, Springer Berlin Heidelberg, pp. 162–182, CiteSeerX 10.1.1.106.7115, doi:10.1007/11561163_8, ISBN 9783540291312
  6. ^ Alur, Rajeev; Trivedi, Ashutosh; Wojtczak, Dominik (2012-04-17). Optimal scheduling for constant-rate multi-mode systems. ACM. pp. 75–84. CiteSeerX 10.1.1.299.946. doi:10.1145/2185632.2185647. ISBN 9781450312202. S2CID 14587340.

Further reading edit

  • 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.