MP2-2 3:40 Proceedings of the 2000 IEEE International Symposium on Computer-Aided Control System Design Anchorage, Alaska, USA September 25-27, 2000 Hybrid Automata: A Formal Paradigm for Heterogeneous Modeling' Karl Henrik Johansson, John Lygeros, Jun Zhang, and Shankar Sastry Department of Electrical Engineering and Computer Sciences . University of California, Berkeley, CA 94720-1770 { johans , lygeros ,zhangjun,sastry}@eecs .berkeley .edu Abstract A hybrid automaton is a model of a system with inter- acting continuous and discrete dynamics. It has been successfully employed in emerging applications on the border between computer science and control theory. In this paper, hybrid automata are formally introduced. Some results on existence and uniqueness of executions for hybrid automata are obtained. Continuous depen- dence on initial states are shown for a class of hybrid automata. Zeno hybrid automata, i.e., hybrid automata that exhibit infinitely many discrete transitions in finite time, are also discussed. 1 Introduction The importance of systems with interacting digital and analog computations is increasing dramatically. Areas such as aeronautics, automotive vehicles, bioengineer- ing, embedded software, process control, and trans- portation are growing tremendously [14, 2, 3, 7, 8, 161. There is a large number of new applications, where computers are coupled to physical environment. This has led to a need for better understanding of the be- havior of these hybrid systems with linked continuous- time and discrete-time dynamics, in order to guarantee design performance. Hybrid automata have proved to be an efficient way to model systems with both continuous and discrete dy- namics. Their rich structure allow them to accurately predict the behavior of quite complex systems. Based on computer science and control theory, tools are now evolving for analyzing and designing hybrid systems within the hybrid automata framework. The work pre- sented in the paper is part of this activity. 'This work was supported by ARO under the MUM grant DAAH04-96-1-0341, the Swedish Foundation for International Cooperation in Research and Higher Education, Telefonaktiebo- laget LM Ericsson's Foundation, ONR under grant N00014-97- 1-0946, and DARPA under contract F33615-984-3614. The main col1,ribution of the paper is to present some results on the fundamental properties of hybrid au- tomata. We investigate the existence and uniqueness of executions of hybrid automata. Although such re- sults form the foundation for analysis and design meth- ods, these problems have only recently been addressed [15, 91. Continuous dependence on initial conditions is another important issue in the analysis of hybrid au- tomata [4, 131. It is for instance often a desirable prop- erty in computer simulations. In the paper, we show a new result in this area. Zen0 hybrid systems are sys- tems that exhibit infinitely many discrete transitions in a finite time interval. This type of behavior does only occur in systems with interacting continuous and discrete dynamics. Physical systems are of course not Zeno, but a model of a physical system may however be Zen0 due to a too high level of abstraction. It is therefore important to characterize Zen0 hybrid au- tomata and in applicable cases modify the model to avoid Zenoness [5]. In the paper, we are able to com- pletely characterize the set of Zen0 states for a couple of quite broad classes of Zen0 hybrid automata. The outline of the paper is as follows. Section 2 intro- duces notation and the definitions of hybrid automata and executions. Some recent results on existence and uniqueness of executions for classes of hybrid automata are given in Section 3. A result on continuous depen- dence on initial conditions is presented in Section 4. Fi- nally, Zen0 hybrid automata are discussed in Section 5 and some conclusions are given in Section 6. 2 Hybrid Automata and Executions The following definitions are based on [lo, 5, 181. For a finite collection V of variables, let V denote the set of valuations of these variables. We use lower case letter to denote both a variable and its valuation. We refer to variables whose set of valuations is finite or countable as discrete and to variables whose set of valuations is a subset of a Euclidean space as continuous. For a set 0-7803-6566-6/00$1 O.ooo2OOO IEEE 123of continuous variables X with X = Rn for n 2 0, we assume that X is given the Euclidean metric topology, and o denote the Euclidean norm. For a set of disc bles Q, we assume that Q is given the dis- Crete topology (every subset is an open set), generated (q, 4') = 0 if q = q' and do(q, q') = 1 if e the valuations of the union Q U X by Q x X, which is given the product topology generated by the metric d((q,x), (q',x')) = do(q,q') + 112 - ~'11. We assume that a subset U of a topological space is given the induced topology, and we use to denote its closure, U" its interior, dU = \ U" its boundary, U' its complement, IUI its cardinality, and P(U) the set of all subsets of U. Definition 1 (Hybrid Automaton) A hybrid automaton H is a collection H = (Q, X, Init, f, Dom, Reset), where Q is the finite collection of discrete variables with values in Q; X is the finite collection of continuous variables with values in X = Rn ; Init C_ Q x X is the set of initial states; f : Q x X + TX is the vector field; Dom C Q x X is the domain of H; Reset : Q x X + P(Q x X) is the reset relation. We refer to (q,z) E Q x X as the state of H. We make the standing assumption that IQ1 < CO and that f is Lipschitz continuous in its second argument. A hybrid automaton can be represented by a directed graph (Q, E), with vertices Q and edges E = { (q, q') E Q x Q : 3z,z' E X, (q',d) E Reset(q,z)}. With each vertex q E Q, we associate a set of continuous initial states Init(q) = {x E X : (q,x) E Init}, a vector field f(q,-), and a set D(q) = {z E X : (q,x) E Dom}. With each edge e = (q,q') E E, we associate a guard G(e) = {x E X : 32' E X,(q',x') E Reset(q,z)}, and a reset map R(e,x) = {x' E X : (q',x') E Reset(q,z)}. Definition 2 (Hybrid Time Trajectory) A hybrid time trajectory T is a finite or infinite se- quence of intervals {Ii}go, such that Hybrid time trajectories can extend to infinity if T is an infinite sequence or if it is a finite sequence ending with an interval of the form [TN, CO). Since the