Lecture Notes on Hybrid Systems
John Lygeros
Department of Electrical and Computer Engineering
University of Patras
Rio, Patras, GR-26500, Greece
lygeros@ee.upatras.gr
ENSIETA
2-6/2/2004
Abstract
The aim of this course is to introduce some fundamental concepts from the area of hybrid systems,
that is dynamical systems that involve the interaction of continuous (real valued) states and discrete
(finite valued) states. Applications where these types of dynamics play a prominent role will be
highlighted. We will introduce general methods for investigating properties such as existence of
solutions, reachability and decidability of hybrid systems. The methods will be demonstrated on the
motivating applications. Students who successfully complete the course should be able to appreciate
the diversity of phenomena that arise in hybrid systems and how discrete “discrete” entities and
concepts such as automata, decidability and bisimulation can coexist with continuous entities and
concepts, such as differential equations.
Contents
1 Dynamical Systems: an Overview 1
1.1 Notation & Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Dynamical System Classification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3.1 Pendulum: A Nonlinear, Continuous Time System . . . . . . . . . . . . . . . 3
1.3.2 Logistic Map: A Nonlinear Discrete Time System . . . . . . . . . . . . . . . . 6
1.3.3 Manufacturing Machine: A Discrete System . . . . . . . . . . . . . . . . . . . 7
1.3.4 Thermostat: A Hybrid System . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.4 Bibliography and Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2 Review of Continuous Systems 11
2.1 State Space Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Existence and Uniqueness of Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.3 Continuity with Respect to Initial Condition and Simulation . . . . . . . . . . . . . 14
2.4 Bibliography and Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
3 Hybrid Automata & Executions 16
3.1 Examples of Hybrid Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.1.1 The Bouncing Ball . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.1.2 Gear Shift Control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.1.3 Computer-Controlled System . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3.1.4 Automated Highway System . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.2 Hybrid Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.2.1 Hybrid Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.2.2 Hybrid Time Sets & Executions . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.3 Bibliography and Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4 Existence of Executions 28
4.1 Modelling Issues . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
i
4.2 Two Fundamental Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4.3 Local Existence and Uniqueness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
4.4 Zeno Executions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4.5 Bibliography and Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
5 Analysis and Synthesis 37
5.1 Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
5.2 Deductive Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
5.3 Bibliography and Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6 Model Checking and Timed Automata 41
6.1 Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6.2 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
6.3 Timed Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
6.4 Bibliography and Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
7 Reachability with Inputs: A Viability Theory Perspective 53
7.1 Reachability with Inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
7.2 Impulse Differential Inclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
7.3 Viability and Invariance Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
7.4 Viability Conditions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
7.5 Invariance Conditions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
7.6 Viability Kernels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
7.7 Invariance Kernels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
7.8 The Bouncing Ball Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
7.9 Bibliography and Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
ii
List of Figures
1.1 The pendulum . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.2 Trajectory of the pendulum. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.3 The pendulum vector field. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 Phase plane plot of the trajectory of Figure 1.2. . . . . . . . . . . . . . . . . . . . . . 6
1.5 The logistic map. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.6 The directed graph of the manufacturing machine automaton. . . . . . . . . . . . . . 8
1.7 A trajectory of the thermostat system. . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.8 Directed graph notation for the thermostat system. . . . . . . . . . . . . . . . . . . . 9
3.1 Bouncing ball . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2 A hybrid system modelling a car with four gears. . . . . . . . . . . . . . . . . . . . . 18
3.3 The efficiency functions of the different gears. . . . . . . . . . . . . . . . . . . . . . . 18
3.4 Computer-controlled system. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.5 The AHS control hierarchy. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.6 The water tank system. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3.7 Graphical representation of the water tank hybrid automaton. . . . . . . . . . . . . . 23
3.8 A hybrid time set τ = {[τi, τi ]}3
i=0. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
3.9 τ ˆτ and τ ˜τ. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.10 Example of an execution of the water tank hybrid automaton. . . . . . . . . . . . . . 26
3.11 τA finite, τC and τD infinite, τE and τF Zeno. . . . . . . . . . . . . . . . . . . . . . . 27
4.1 Examples of blocking and non-determinism. . . . . . . . . . . . . . . . . . . . . . . . 31
4.2 Chattering system. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4.3 System with a smooth, non-analytic domain. . . . . . . . . . . . . . . . . . . . . . . 35
6.1 Finite state transition system. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
6.2 Example of a timed automaton. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
6.3 Region graph for the timed automaton of Figure 6.2. . . . . . . . . . . . . . . . . . . 50
7.1 K viable under H = (X, F, R, J) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
iii
7.2 K invariant under (X, F, R, J) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
7.3 Three possible evolutions for x0 ∈ ViabF (K ∩ I, R−1
(K)) ∪ (K ∩ R−1
(K)). . . . . . 63
iv
Chapter 1
Dynamical Systems: an Overview
1.1 Notation & Background
• Rn
denotes the n-dimensional Euclidean space. This is a finite dimensional vector space
(also known as a linear space). If n = 1, we will drop the superscript and write just R (the
set of real numbers or “the real line”). I will make no distinction between vectors and real
numbers in the notation (no arrows over the letters, bold fond, etc.). Both vectors and real
numbers will be denoted by lower case letters.
• x = x2
1 + x2
2 + . . . + x2
n denotes the standard (Euclidean) norm in Rn
.
• Z denotes the set of integers, . . . , −2, −1, 0, 1, 2, . . ..
• x ∈ A is a shorthand for “x belongs to a set A”, e.g. x ∈ Rn
means that x is an n-dimensional
vector.
• Given a set X, P(X) denotes the power set of X, i.e. the set of all subsets of X. In other
words, A ∈ P(X) means that A ⊆ X. By definition, X ∈ P(X) for all sets X.
• ∅ denotes the empty set (a set containing nothing). By definition ∅ ∈ P(X) for all sets X.
Exercise 1.1 Consider a set containing only 3 elements, say Q = {q1, q2, q3}. Write down all
the elements of P(Q). There should be 8 of them. In mathematics, the power set, P(X), of a
set X is sometimes denoted by 2X
. Can you guess the reason for this?
• f(·) : A → B is a shorthand for a function mapping every element x ∈ A to an element
f(x) ∈ B. For example the function sin(·) : R → R maps a real number x to its sine, sin(x).
• In logic
– ∀ is a shorthand for “for all”, as in “∀x ∈ R, x2
≥ 0”.
– ∃ is a shorthand for “there exists”, as in “∃x ∈ R such that sin(x) = 0”.
– ∧ is a shorthand for “and”, ∨ stands for “or”, and ¬ stands for “not”.
• Logic expressions can be used to define sets by enumerating properties of their elements. For
example, the following expression defines a subset of R2
{x ∈ R2
| (x2
1 + x2
2 = 1) ∧ (x1 ≥ 0) ∧ (x2 ≤ 0)},
namely the part of the unit circle that falls in the 4th
quadrant.
• ∞ denotes “infinity”.
1
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 2
• Given two real numbers a ≤ b,
[a, b] = {x ∈ R | a ≤ x ≤ b}
denotes the closed interval from a to b, while
[a, b) = {x ∈ R | a ≤ x < b}
denotes the right-open interval from a to b. Notice that if a = b, then [a, b] = [a, a] = {a},
whereas [a, b) = [a, a) = ∅. We also define [a, ∞) as the set of all real numbers greater than or
equal to a.
• Given two sets Q and X, Q × X denotes the product of the two sets. This is the set of all
pairs (q, x) with q ∈ Q and x ∈ X, i.e.
Q × X = {(q, x) | q ∈ Q and x ∈ X}
I will assume that people are somewhat familiar with the concepts of vector space, state space,
differential, etc. A brief review of these topics will be given in Chapter 2
Lecture notes will be self contained but, by necessity, terse. I recommend that students consult the
references to fully appreciate the subject. A number of exercises have been added throughout the
notes, to enhance the learning experience and highlight subtle points. They should all be easy (if
not trivial!) to solve if you understand the notes. You are not required to turn in solutions
for the exercises in the notes, they are there to help you understand the material, not to test
your understanding. You are of course welcome to discuss the solutions with the instructor.
1.2 Dynamical System Classification
Roughly speaking, a dynamical system describes the evolution of a state over time. To make
this notion more precise we need to specify what we mean by the terms “evolution”, “state” and
“time”.
Certain dynamical systems can also be influenced by external inputs, which may represent either
uncontrollable disturbances (e.g. wind affecting the motion of an aircraft) or control signals (e.g.
the commands of the pilot to the aircraft control surfaces and engines). Some dynamical systems
may also have outputs, which may represent either quantities that can be measured, or quantities
that need to be regulated. Dynamical systems with inputs and outputs are sometimes referred to
as control systems.
Based on the type of their state, dynamical systems can be classified into:
1. Continuous, if the state takes values in Euclidean space Rn
for some n ≥ 1. We will use
x ∈ Rn
to denote the state of a continuous dynamical system.
2. Discrete, if the state takes values in a countable or finite set {q1, q2, . . .}. We will use q to
denote the state of a discrete system. For example, a light switch is a dynamical system whose
state takes on two values, q ∈ {ON, OFF}. A computer is also a dynamical system whose
state takes on a finite (albeit very large) number of values.
3. Hybrid, if part of the state takes values in Rn
while another part takes values in a finite set.
For example, the closed loop system we obtain when we use a computer to control an inverted
pendulum is hybrid: part of the state (namely the state of the pendulum) is continuous, while
another part (namely the state of the computer) is discrete.
Based on the set of times over which the state evolves, dynamical systems can be classified as:
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 3
1. Continuous time, if the set of times is a subset of the real line. We will use t ∈ R to denote
continuous time. Typically, the evolution of the state of a continuous time system is described
by an ordinary differential equation (ODE). Think of the linear, continuous time system
in state space form
˙x = Ax.
2. Discrete time, if the set of times is a subset of the integers. We will use k ∈ Z to denote
discrete time. Typically, the evolution of the state of a discrete time system is described by a
difference equation. Think of the linear discrete time system in state space form
xk+1 = Axk.
3. Hybrid time, when the evolution is over continuous time but there are also discrete “instants”
where something “special” happens. More on this in Chapter 3.
Continuous state systems can be further classified according to the equations used to describe the
evolution of their state
1. Linear, if the evolution is governed by a linear differential equation (continuous time) or
difference equation (discrete time).
2. Nonlinear, if the evolution is governed by a nonlinear differential equation (continuous time)
or difference equation (discrete time).
Exercise 1.2 The linear vs nonlinear classification generally does not apply to discrete state or
hybrid systems. Why?
In this class we will start by giving some examples of the the following classes of systems:
1. Nonlinear (continuous state), continuous time systems.
2. Nonlinear, discrete time systems.
3. Discrete state, discrete time systems.
We will then concentrate on hybrid state, hybrid time systems and highlight the differences from
the other classes. Classes of systems that will not be treated at all include:
• Infinite dimensional continuous state systems described, for example, by partial differential
equations (PDE).
• Discrete state systems with an infinite number of states, e.g. Petri nets, push down automata,
Turing machines.
• Stochastic systems, i.e. systems with probabilistic dynamics.
1.3 Examples
1.3.1 Pendulum: A Nonlinear, Continuous Time System
Consider a pendulum hanging from a weight-less solid rod and moving under gravity (Figure 1.1).
Let θ denote the angle the pendulum makes with the downward vertical, l the length of the pendulum,
m its mass, and d the dissipation constant. The evolution of θ is governed by
ml¨θ + dl ˙θ + mg sin(θ) = 0
This is a nonlinear, second order, ordinary differential equation (ODE).
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 4
l
θ
mg
Figure 1.1: The pendulum
0 1 2 3 4 5 6 7 8 9 10
−2
−1.5
−1
−0.5
0
0.5
1
1.5
x2
x1
t
Figure 1.2: Trajectory of the pendulum.
Exercise 1.3 Derive this equation from Newton’s laws. Why is this ODE called nonlinear?
To determine how the pendulum is going to move, i.e. determine θ as a function of time, we would
like to find a solution to this ODE . Assuming that at time t = 0 the pendulum starts as some initial
position θ0 and with some initial velocity ˙θ0, “solving the ODE” means finding a function of time
θ(·) : R → R
such that
θ(0) = θ0
˙θ(0) = ˙θ0
ml¨θ(t) + dl ˙θ(t) + mg sin(θ(t)) = 0, ∀t ∈ R
Such a function is known as a trajectory (or solution) of the system. At this stage it is unclear
if one, none or multiple trajectories exist for this initial condition. Existence and uniqueness of
trajectories are both desirable properties for ODE that are used to model physical systems.
For nonlinear systems, even if a unique trajectory exists for the given initial condition, it is usually
difficult to construct explicitly. Frequently solutions of ODE can only be approximated by simulation.
Figure 1.2 shows a simulated trajectory of the pendulum for l = 1, m = 1, d = 1, g = 9.8,
θ(0) = 0.75 and ˙θ(0) = 0.
To simplify the notation we typically write dynamical system ODE in state space form
˙x = f(x)
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 5
−0.25 −0.2 −0.15 −0.1 −0.05 0 0.05 0.1 0.15 0.2 0.25
−0.6
−0.4
−0.2
0
0.2
0.4
0.6
θ
˙θ
Figure 1.3: The pendulum vector field.
where x is now a vector in Rn
for some appropriate n ≥ 1. The easiest way to do this for the
pendulum is to set
x =
x1
x2
=
θ
˙θ
which gives rise to the state space equations
˙x =
˙x1
˙x2
=
x2
−g
l sin(x1) − d
m x2
= f(x)
The vector
x ∈ R2
is called the state of the system. The size of the state vector (in this case n = 2) is called the
dimension of the system. Notice that the dimension is the same as the order of the original ODE.
The function
f(·) : R2
→ R2
which describes the dynamics is called a vector field, because is assigns a “velocity” vector to each
state vector. Figure 1.3 shows the vector field of the pendulum.
Exercise 1.4 Other choices are possible for the state vector. For example, for the pendulum one
can use x1 = θ3
+ ˙θ and x2 = ˙θ. What would the vector field be for this choice of state?
Solving the ODE for θ is equivalent to finding a function
x(·) : R → R2
such that
x(0) =
x1(0)
x2(0)
=
θ0
˙θ0
˙x(t) = f(x(t)), ∀t ∈ R.
For two dimensional systems like the pendulum it is very convenient to visualise the solutions by
phase plane plots. These are plots of x1(t) vs x2(t) parameterised by time (Figure 1.4).
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 6
−0.6 −0.4 −0.2 0 0.2 0.4 0.6 0.8
−2
−1.5
−1
−0.5
0
0.5
1
1.5
θ
˙θ
Figure 1.4: Phase plane plot of the trajectory of Figure 1.2.
0 0.1 0.2 0.3 0.4 0.5 0.6 0.7 0.8 0.9 1
0
0.1
0.2
0.3
0.4
0.5
0.6
0.7
0.8
0.9
1
f(x)
x
Figure 1.5: The logistic map.
1.3.2 Logistic Map: A Nonlinear Discrete Time System
The logistic map
xk+1 = axk(1 − xk) = f(xk) (1.1)
is a nonlinear, discrete time dynamical system that has been proposed as a model for the fluctuations
in the population of fruit flies in a closed container with constant food supply [78]. We assume that
the population is measured at discrete times (e.g. generations) and that it is large enough to be
assumed to be a continuous variable. In the terminology of the previous section, this is a one
dimensional system with state xk ∈ R, whose evolution is governed by the difference equation (1.1)
given above.
The shape of the function f (Figure 1.5) reflects the fact that when the population is small it tends
to increase due to abundance of food and living space, whereas when the population is large it tends
to decrease, due to competition for food and the increased likelihood of epidemics. Assume that
a ≤ 4 and that the initial population is such that 0 ≤ x0 ≤ 1.
Exercise 1.5 Show that under these assumptions 0 ≤ xk ≤ 1 for all k ∈ Z with k ≥ 0.
The behaviour of xk as a function of k depends on the value of a.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 7
1. If 0 ≤ a < 1, xk decays to 0 for all initial conditions x0 ∈ [0, 1]. This corresponds to a situation
where there is inadequate food supply to support the population.
2. If 1 ≤ a ≤ 3, xk tends to a steady state value. In this case the population eventually stabilises.
3. If 3 < a ≤ 1 +
√
6 = 3.449, xk tends to a 2-periodic state. This corresponds to the population
alternating between two values from one generation to the next.
As a increases further more and more complicated patterns are obtained: 4-periodic points, 3periodic
points, and even chaotic situations, where the trajectory of xk is a-periodic (i.e. never
meets itself).
1.3.3 Manufacturing Machine: A Discrete System
Consider a machine in a manufacturing plant that processes parts of type p one at a time. The
machine can be in one of three states: Idle (I), Working (W) or Down (D). The machine can
transition between the states depending on certain events. For example, if the machine is idle and
a part p arrives it will start working. While the machine is working it may break down. While the
machine is down it may be repaired, etc.
Abstractly, such a machine can be modelled as a dynamical system with a discrete state, q, taking
three values
q ∈ Q = {I, W, D}
The state “jumps” from one value to another whenever one of the events, σ occurs, where
σ ∈ Σ = {p, c, f, r}
(p for “part arrives”, c for “complete processing”, f for “failure” and r for “repair”). The state after
the event occurs is given by a transition relation
δ : Q × Σ → Q
Since both Q and Σ are finite sets, one can specify δ by enumeration.
δ(I, p) = W
δ(W, c) = I
δ(W, f) = D
δ(D, r) = I
δ is undefined for the rest of the combinations of q and σ. This reflects the fact that certain events
may be impossible in certain states. For example, it is impossible for the machine to start processing
a part while it is down, hence δ(D, p) is undefined.
Exercise 1.6 If the discrete state can take n values and there are m possible events, what is the
maximum number of lines one may have to write down to specify δ?
Such a dynamical system is called an automaton, or a finite state machine. Automata are special
cases of discrete event systems. Discrete event systems are dynamical systems whose state also
jumps depending on a finite set of events but can take on an infinite number of values. The dynamics
of a finite state machine can be represented compactly by a directed graph (Figure 1.6). This is
a graph whose nodes represent the possible values of the state (in this case I, W, D). The arcs of
the graph represent possible transitions between the state values and are labelled by the events.
Exercise 1.7 What is the relation between the number of arcs of the graph and the number of lines
one needs to write down in order to specify δ?
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 8
f
c
r
p
W D
I
Figure 1.6: The directed graph of the manufacturing machine automaton.
Assume that the machine starts in the idle state q0 = I. What are the sequences of events the
machine can experience? Clearly some sequences are possible while others are not. For example,
the sequence pcp is possible: the machine successfully processes one part and subsequently starts
processing a second one. The sequence ppc, on the other hand is not possible: the machine can not
start processing a second part before the previous one is complete. More generally, any sequence that
consists of an arbitrary number of pc’s (possibly followed by a single p) is an acceptable sequence.
In the discrete event literature this set of sequences is compactly denoted as
(pc)∗
(1 + p)
where ∗
denotes an arbitrary number (possibly zero) of pc’s, 1 denotes the empty sequence (no event
takes place), and + denotes “or”.
Likewise, pfr is a possible sequence of events (the machine starts processing a part, breaks down and
then gets repaired) while pfp is not (the machine can not start processing a part while it is down).
More generally, any sequence that consists of an arbitrary number of pfr’s (possibly followed by a
p or a pf) is an acceptable sequence.
Exercise 1.8 Write this set of sequences in the discrete event notation given above.
The set of all sequences that the automaton can experience is called the language of the automaton.
The above discussion suggests that the language of the machine automaton is
(pc + pfr)∗
(1 + p + pf)
It is important to understand the properties of these languages, for example to determine how to
schedule the work in a manufacturing plant.
1.3.4 Thermostat: A Hybrid System
Consider a room being heated by a radiator controlled by a thermostat. Assume that when the
radiator is off the temperature, x ∈ R, of the room decreases exponentially towards 0 degrees
according to the differential equation
˙x = −ax (1.2)
for some a > 0.
Exercise 1.9 Verify that the trajectories of (1.2) decrease to 0 exponentially.
When the thermostat turns the heater on the temperature increases exponentially towards 30 degrees,
according to the differential equation
˙x = −a(x − 30). (1.3)
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 9
x
22
21
20
19
18
t
Figure 1.7: A trajectory of the thermostat system.
OFF ON
˙x = −ax ˙x = −a(x − 30)
x ≥ 18 x ≤ 22
x ≤ 19
x ≥ 21
Figure 1.8: Directed graph notation for the thermostat system.
Exercise 1.10 Verify that the trajectories of (1.3) increase towards 30 exponentially.
Assume that the thermostat is trying to keep the temperature at around 20 degrees. To avoid
“chattering” (i.e. switching the radiator on an off all the time) the thermostat does not attempt
to turn the heater on until the temperature falls below 19 degrees. Due to some uncertainty in the
radiator dynamics, the temperature may fall further, to 18 degrees, before the room starts getting
heated. Likewise, the thermostat does not attempt to turn the heater on until the temperature
rises above 21 degrees. Due to some uncertainty in the radiator dynamics the temperature may rise
further, to 22 degrees, before the room starts to cool down. A trajectory of the thermostat system
is shown in Figure 1.7. Notice that in this case multiple trajectories may be obtained for the same
initial conditions, as for certain values of the temperature there is a choice between switching the
radiator on/off or not. Systems for which such a choice exists are known as non-deterministic.
Notice that this system has both a continuous and a discrete state. The continuous state is the
temperature in the room x ∈ R. The discrete state, q ∈ {ON, OFF} reflects whether the radiator
is on or off. The evolution of x is governed by a differential equation (as was the case with the
pendulum), while the evolution of q is through jumps (as was the case with the manufacturing
machine). The evolution of the two types of state is coupled. When q = ON, x rises according to
differential equation (1.3), while when q = OFF, x decays according to differential equation (1.2).
Likewise, q can not jump from ON to OFF unless x ≥ 21. q must jump from ON to OFF if x ≥ 22.
Etc.
It is very convenient to compactly describe such hybrid systems by mixing the differential equation
with the directed graph notation (Figure 1.8).
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 10
1.4 Bibliography and Further Reading
Continuous state systems and their properties have been studied extensively in mathematics engineering,
economics, biology, etc. The literature is vast and there are a number of excellent textbooks
available (see for example [100, 103, 51, 88]).
Discrete state systems have also been studied for many years, especially in computer science. Good
textbooks include [43, 58, 25].
By comparison, the study of hybrid systems is relatively recent. The few books that have appeared
on the subject to date [77, 98] have a research monograph “flavour” and address specific topics
and classes of systems. [98] contains a substantial textbook style overview. Another good source of
material are the special issues devoted by a number of journals on the topic of hybrid systems [85,
9, 91, 90, 84].
Chapter 2
Review of Continuous Systems
2.1 State Space Form
All continuous nonlinear systems considered in this class can be reduced to the standard state
space form. It is usual to denote
• the states of the system by xi ∈ R, i = 1, . . . , n,
• the inputs by uj ∈ R, j = 1, . . . , m, and
• the outputs by yk ∈ R, k = 1, . . . , p.
The number of states, n, is called the dimension (or order) of the system. The evolution of the
states, inputs and outputs is governed by a set of functions
fi : Rn
× Rm
× R → R, for i = 1, . . . , n
hj : Rn
× Rm
× R → R, for j = 1, . . . , p
Roughly speaking, at a given time t ∈ R and for given values of all the states and inputs these
functions determine in what direction the state will move, and what the output is going to be.
˙x1 = f1(x1, . . . , xn, u1, . . . , um, t)
...
˙xn = fn(x1, . . . , xn, u1, . . . , um, t)
y1 = h1(x1, . . . , xn, u1, . . . , um, t)
...
yp = hp(x1, . . . , xn, u1, . . . , um, t)
Exercise 2.1 What is the dimension of the pendulum example? What are the functions fi?
It is usually convenient to simplify the equations somewhat by introducing vector notation. Let
x =



x1
...
xn


 ∈ Rn
, u =



u1
...
um


 ∈ Rm
, y =



y1
...
yp


 ∈ Rp
,
11
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 12
and define
f : Rn
× Rm
× R → Rn
h : Rn
× Rm
× R → Rp
by
f(x, u, t) =



f1(x1, . . . , xn, u1, . . . , um, t)
...
fn(x1, . . . , xn, u1, . . . , um, t)


 , h(x, u, t) =



h1(x1, . . . , xn, u1, . . . , um, t)
...
hp(x1, . . . , xn, u1, . . . , um, t)


 .
Then the system equations simplify to
˙x = f(x, u, t)
y = h(x, u, t)
(2.1)
Equations (2.1) are known as the state space form of the system. The vector space Rn
in which
the state of the system takes values is known as the state space of the system. If the system is of
dimension 2, the state space is also referred to as the phase plane. The function f that determines
the direction in which the state will move is known as the vector field.
Notice that the differential equation for x is first order, i.e. involves ˙x but no higher derivatives of
x. Sometimes the system dynamics are given to us in the form of higher order differential equations,
i.e. equations involving a variable θ ∈ R and its derivatives with respect to time up to dr
θ
dtr for some
integer r ≥ 1. Such systems can be easily transformed to state space form by setting x1 = θ, x2 = ˙θ,
. . . , xr−1 = dr−1
θ
dtr−1 .
Exercise 2.2 Consider the system
dr
θ
dtr
+ g(θ,
dθ
dt
, . . . ,
dr−1
θ
dtr−1
) = 0
Write this system in state space form.
It may of course happen in certain examples that there are no inputs or outputs, or that there is no
explicit dependence of the dynamics on time. Systems of the form
˙x = f(x)
(i.e. without inputs or outputs and with no explicit dependence on time) are called autonomous
systems.
Exercise 2.3 Is the pendulum an autonomous system?
Exercise 2.4 Consider a non-autonomous system of the form ˙x = f(x, t), of dimension n. Show
that it can be transformed to an autonomous system of dimension n + 1. (Hint: append t to the
state).
2.2 Existence and Uniqueness of Solutions
Consider an autonomous dynamical system in state space form
˙x = f(x)
and assume that at time t = 0 the state is equal to x0, i.e.
x(0) = x0
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 13
We would like to “solve” the dynamics of the system to determine how the state will evolve in the
future (i.e. for t ≥ 0). More precisely, given some T > 0 we would like to determine a function
x(·) : [0, T ] → Rn
such that
x(0) = x0
˙x(t) = f(x(t)), ∀t ∈ [0, T ].
Such a function x(·) is called a trajectory (or solution) of the system. Notice that given a
candidate trajectory x(·) : [0, T ] → Rn
one needs to verify both the differential condition and the
initial condition to ensure that x(·) is indeed a solution of the differential equation.
Exercise 2.5 Assume instead of x(0) = x0 it is required that x(t0) = x0 for some t0 = 0. Show
how one can construct solutions to the system
x(t0) = x0, ˙x = f(x)
from solutions to
x(0) = x0, ˙x = f(x)
by appropriately redefining t. Could you do this with a non-autonomous system?
Without any additional information, it is unclear whether one can find a function x(·) solving the
differential equation. A number of things can go wrong.
Example (No solutions) Consider the one dimensional system
˙x = −sign(x), x(0) = 0
A solution to this differential equation does not exist for any T ≥ 0.
Exercise 2.6 Assume that x(0) = 1. Show that solutions to the system exist for all T ≤ 1 but not
for T > 1.
Incidentally, something similar would happen with the radiator system if the thermostat insisted on
switching the radiator on and off exactly at 20 degrees.
Example (Multiple Solutions) Consider the one dimensional system
˙x = 3x2/3
, x(0) = 0
All functions of the form
x(t) =
(t − a)3
t ≥ a
0 t ≤ a
for any a ≥ 0 are solutions of this differential equation.
Exercise 2.7 Verify this.
Notice that in this case the solution is not unique. In fact there are infinitely many solutions, one
for each a ≥ 0.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 14
Example (Finite Escape Time) Consider the one dimensional system
˙x = 1 + x2
, x(0) = 0
The function
x(t) = tan(t)
is a solution of this differential equation.
Exercise 2.8 Verify this. What happens at t = π/2?
Notice that the solution is defined for T < π/2 but not for T ≥ π/2.
To eliminate such pathological cases we need to impose some assumptions on f.
Definition 2.1 A function f : Rn
→ Rn
is called Lipschitz continuous if there exists λ > 0 such
that for all x, ˆx ∈ Rn
f(x) − f(ˆx) < λ x − ˆx
λ is known as the Lipschitz constant. A Lipschitz continuous function is continuous, but not necessarily
differentiable. All differentiable functions with bounded derivatives are Lipschitz continuous.
Exercise 2.9 Show that for x ∈ R the function f(x) = |x| that returns the absolute value of x is
Lipschitz continuous. What is the Lipschitz constant? Is f continuous? Is it differentiable?
Theorem 2.1 (Existence & Uniqueness of Solutions) If f is Lipschitz continuous, then the
differential equation
˙x = f(x)
x(0) = x0
has a unique solution x(·) : [0, T ] → Rn
for all T ≥ 0 and all x0 ∈ Rn
.
Exercise 2.10 Three examples of dynamical systems that do not have unique solutions were given
above. Why do these systems fail to meet the conditions of the theorem? (The details are not easy
to get right.)
This theorem allows us to check whether the differential equation models we develop make sense. It
also allows us to spot potential problems with proposed solutions. For example, uniqueness implies
that solutions can not cross.
Exercise 2.11 Why does uniqueness imply that trajectories can not cross? (Hint: what would
happen at the crossing point?).
2.3 Continuity with Respect to Initial Condition and Simu-
lation
Theorem 2.2 (Continuity with Initial State) Assume f is Lipschitz continuous with Lipschitz
constant λ. Let x(·) : [0, T ] → Rn
and ˆx(·) : [0, T ] → Rn
be solutions to ˙x = f(x) with x(0) = x0
and ˆx(0) = ˆx0 respectively. Then for all t ∈ [0, T ]
x(t) − ˆx(t) ≤ x0 − ˆx0 eλt
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 15
In other words, solutions that start close to one another remain close to one another.
This theorem provides another indication that dynamical systems with Lipschitz continuous vector
fields are well behaved. For example, it provides theoretical justification for simulation algorithms.
Most nonlinear differential equations are impossible to solve by hand. One can however approximate
the solution on a computer, using numerical algorithms for computing integrals (Euler, Runge-Kutta,
etc.). This is a process known as simulation.
Powerful computer packages, such as Matlab, make the simulation of most systems relatively straight
forward. For example, the code used to generate the pendulum trajectories is based on a Matlab
function
function [xprime] = pendulum(t,x)
xprime=[0; 0];
l = 1;
m=1;
d=1;
g=9.8;
xprime(1) = x(2);
xprime(2) = -sin(x(1))*g/l-x(2)*d/m;
The simulation code is then simply
>> x=[0.75 0];
>> [T,X]=ode45(’pendulum’, [0 10], x’);
>> plot(T,X);
>> grid;
The continuity property ensures that the numerical approximation to the solution computed by the
simulation algorithms and the actual solution remain close.
When one studies hybrid systems, many of these nice properties unfortunately vanish. As the
non-deterministic thermostat system suggests, existence and uniqueness of solutions are much more
difficult to guarantee. Continuity is usually impossible.
2.4 Bibliography and Further Reading
The material in this chapter is thoroughly covered in any good textbook on nonlinear dynamical
systems, see for example [100, 103, 51, 88].
Chapter 3
Hybrid Automata & Executions
3.1 Examples of Hybrid Systems
Roughly speaking, hybrid systems are dynamical systems that involve the interaction of different
types of dynamics. In this class we are interested in hybrid dynamics that arise out of the interaction
of continuous state dynamics and discrete state dynamics. Recall that a state variable is called
discrete if it takes on a finite (or countable) number of values and continuous if it takes values in
Euclidean space Rn
for some n ≥ 1. By their nature, discrete states can change value only through
a discrete “jump” (c.f. the machining example in Chapter 1). Continuous states can change values
either through a jump (c.f. the logistic map example in Chapter 1), or by “flowing” in continuous
time according to a differential equation (c.f. the pendulum example in Chapter 1). Hybrid systems
involve both these types of dynamics: discrete jumps and continuous flows. The analysis and design
of hybrid systems is in general more difficult than that of purely discrete or purely continuous
systems, because the discrete dynamics may affect the continuous evolution and vice versa.
Hybrid dynamics provide a convenient framework for modelling systems in a wide range of engineering
applications:
• In mechanical systems continuous motion may be interrupted by collisions.
• In electrical circuits continuous phenomena such as the charging of capacitors, etc. are
interrupted by switches opening and closing, or diodes going on or off.
• In chemical process control the continuous evolution of chemical reactions is controlled by
valves and pumps.
• In embedded computation systems a digital computer interacts with a mostly analogue
environment.
In all these systems it is convenient (and usually fairly accurate) to model the “discrete” components
(switches, valves, computers, etc.) as introducing instantaneous changes in the “continuous”
components (charging of capacitors, chemical reactions, etc.).
We start our study of hybrid systems by providing a number of examples of hybrid behaviour.
16
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 17
(x1 ≤ 0) ∧ (x2 ≤ 0) x2 := −cx2
˙x1 = x2
˙x2 = −g
x1 ≥ 0
x1 ≥ 0
Fly
Figure 3.1: Bouncing ball
3.1.1 The Bouncing Ball
A model for a bouncing ball can be represented as a simple hybrid system (Figure 3.1) with single
discrete state and a continuous state of dimension two
x =
x1
x2
,
where x1 denotes the vertical position of the ball and x2 its vertical velocity.
The continuous motion of the ball is governed by Newton’s laws of motion. This is indicated by the
differential equation that appears in the vertex (box), where g denotes the gravitational acceleration.
This differential equation is only valid as long as x1 ≥ 0, i.e., as long as the ball is above the ground.
This is indicated by the logical expression x1 ≥ 0 that appears in the vertex below the differential
equation.
The ball bounces when x1 = 0 and x2 ≤ 0. This is indicated by the logical expression that appears
near the beginning of the edge (arrow). At each bounce, the ball loses a fraction of its energy. This
is indicated by the equation x2 := −cx2 (with c ∈ [0, 1]) that appears near the end of the edge. This
is an assignment statement, which means that after the bounce the speed of the ball will be c times
the speed of the ball before the bounce, and in the opposite direction.
Exercise 3.1 Show that energy is preserved during continuous evolution. What fraction of the
energy of the ball is lost at each bounce? What is the time interval that elapses between two
bounces as a function of the energy of the ball?
Starting at an initial state with x1 ≥ 0 (as indicated by the logical condition next to the arrow
pointing to the vertex), the continuous state flows according to the differential equation as long
as the condition x1 ≥ 0 is fulfilled. When x1 = 0 and x2 ≤ 0, a discrete transition takes place
and the continuous state is reset to x2 := −cx2 (x1 remains constant). Subsequently, the state
resumes flowing according to the vector field, and so on. Such a trajectory is called an execution
(and sometimes a run or a solution) of the hybrid system.
3.1.2 Gear Shift Control
The gear shift example describes a control design problem where both the continuous and the discrete
controls need to be determined. Figure 3.2 shows a model of a car with a gear box having four gears.
The longitudinal position of the car along the road is denoted by x1 and its velocity by x2 (lateral
dynamics are ignored). The model has two control signals: the gear denoted gear ∈ {1, . . ., 4} and
the throttle position denoted u ∈ [umin, umax]. Gear shifting is necessary because little power can
be generated by the engine at very low or very high engine speed. The function αi represents the
efficiency of gear i. Typical shapes of the functions αi are shown in Figure 3.3.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 18
gear = 1 gear = 2
gear = 2
gear = 3
gear = 3 gear = 4
˙x1 = x2
˙x2 = α1(x2)u
gear = 1
˙x1 = x2
˙x2 = α2(x2)u
gear = 2
˙x1 = x2
˙x2 = α1(x2)u
gear = 3
˙x1 = x2
˙x2 = α1(x2)u
gear = 4
Figure 3.2: A hybrid system modelling a car with four gears.
a1(x2) a2(x2) a3(x2)
a4(x2)
x2
Figure 3.3: The efficiency functions of the different gears.
Exercise 3.2 How many real valued continuous states does this model have? How many discrete
states?
Several interesting control problems can be posed for this simple car model. For example, what is
the optimal control strategy to drive from (a, 0) to (b, 0) in minimum time? The problem is not
trivial if we include the reasonable assumption that each gear shift takes a certain amount of time.
The optimal controller, which can be modelled as a hybrid system, may be derived using the theory
of optimal control of hybrid systems.
3.1.3 Computer-Controlled System
Hybrid systems are natural models for computer-controlled systems (Figure 3.4), since they involve
a physical process (which often can be modelled as continuous-time system) and a computer (which
is fundamentally a finite state machine). The classical approach to computer-controlled systems has
been using sampled-data theory, where it is assumed that measurements and control actions are
taken at a fixed sampling rate. Such a scheme is easily encoded using a hybrid model. The hybrid
model also captures a more general formulation, where measurements are taken based on computer
interrupts. This is sometimes closer to real-time implementations, for example, in embedded control
systems.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 19
Plant
Computer
A/D D/A
Figure 3.4: Computer-controlled system.
3.1.4 Automated Highway System
Highway congestion is an increasing problem, especially in and around urban areas. One of the
promising solutions considered for this problem is traffic automation, either partial or full. The
use of an automated system that performs some or all of the tasks of the driver may reduce or
eliminate human errors and hence improve safety. Moreover, as the automatic controller can react
to disturbances faster than a human driver, automation may also decrease the average inter-vehicle
spacing and hence increase throughput and reduce congestion and delays.
The design of an Automated Highway System (AHS) is an extremely challenging control problem,
and a number of alternatives have been proposed for addressing it. One of the most forward-looking
AHS designs involves a fully automated highway system that supports platooning of vehicles. The
platooning concept [99] assumes that traffic on the highway is organised in groups of tightly spaced
vehicles (platoons). The first vehicle of a platoon is called the leader, while the remaining vehicles
are called followers. The platooning structure achieves a balance between safety and throughput:
it is assumed that the system is safe even if in emergency situations (for example, as a result of a
failure) collisions do occur, as long as the relative velocity at impact is low. Of course no collisions
should take place during normal operation. This gives rise to two safe spacing policies. The obvious
one is that of the leaders, who are assumed to maintain a large inter-platoon spacing (of the order
of 30-60 meters). The idea is that the leader has enough time to stop without colliding with the last
vehicle of the platoon ahead. The more unintuitive spacing policy is that of the followers, who are
assumed to maintain tight intra-platoon spacing (of the order of 1-5 meters). In case of emergency,
collisions among the followers of a platoon may take place, but, because of the tight spacing, they
are expected to be at low relative velocities. Recent theoretical, computational and experimental
studies have shown that an AHS that supports platooning is not only technologically feasible but,
if designed properly, may lead to an improvement of both the safety and the throughput of the
highway system, under normal operation.
Implementation of the platooning concept requires automatic vehicle control, since human drivers
are not fast and reliable enough to produce the necessary inputs. To manage the complexity of the
design process a hierarchical controller is used. The controller is organised in four layers (Figure 3.5).
The top two layers, called network and link, reside on the roadside and are primarily concerned with
throughput maximisation, while the bottom two, called coordination and regulation, reside on the
vehicles and are primarily concerned with safety. The physical layer is not part of the controller. It
contains the “plant”, i.e. the vehicles and highway, with their sensors, actuators and communication
equipment.
The network layer is responsible for the flow of traffic on the entire highway system, for example,
several highways around an urban area. Its task is to prevent congestion and maximise throughput
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 20
Link Layer
(Flow)
Network Layer
(Routing)
Coordination Layer
(Communication)
Regulation Layer
(Control)
Physical Layer
(Vehicles)
On−Board
Roadside
Continuous
Discrete
Figure 3.5: The AHS control hierarchy.
by dynamically routing traffic. The link layer coordinates the operation of sections (links) of the
highway (for example the highway segment between two exits). Its primary concern is to maximise
the throughput of the link. With these criteria in mind, it calculates an optimum platoon size and
an optimum velocity and decides which lanes the vehicles should follow. It also monitors incidents
and diverts traffic away from them, in an attempt to minimise their impact on traffic flow.
The coordination layer coordinates the operation of neighbouring platoons by choosing manoeuvres
that the platoons need to carry out. For normal operation, these manoeuvres are join to join
two platoons into one, split to break up one platoon into two, lane change, entry and exit. The
coordination layer is primarily a discrete controller. It uses communication protocols, in the form
of finite state machines, to coordinate the execution of these manoeuvres between neighbouring
vehicles.
The regulation layer receives the coordination layer commands and readings from the vehicle sensors
and generates throttle, steering and braking commands for the vehicle actuators. For this purpose
it utilises a number of continuous time feedback control laws that use the readings provided by the
sensors to calculate the actuator inputs required for a particular manoeuvre. In addition to the
control laws needed for the manoeuvres, the regulation layer makes use of two default controllers,
one for leader and one for follower operation.
The interaction between the coordination layer (which is primarily discrete) and the regulation layer
(which is primarily continuous) gives rise to interesting hybrid dynamics. To ensure the safety of
the AHS, one needs to verify that the closed loop hybrid system does not enter a bad region of its
state space (e.g. does not allow any two vehicles to collide at high relative velocity). This issue can
be addressed by posing the problem as a game between the control applied by one vehicle and the
disturbance generated by neighbouring vehicles. It can be shown that information available through
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 21
discrete coordination can be used together with appropriate continuous controllers to ensure the
safety of the closed loop hybrid system.
3.2 Hybrid Automata
To model all these diverse phenomena one needs a modelling language that is
• descriptive, to allow one to capture different types of continuous and discrete dynamics, be
capable of modelling different ways in which discrete evolution affects and is affected by continuous
evolution, allow non-deterministic models (e.g. the thermostat) to capture uncertainty,
etc.
• composable, to allow one to build large models by composing models of simple components
(e.g. for the AHS application).
• abstractable, to allow one to refine design problems for composite models down to design
problems for individual components and, conversely, compose results about the performance
of individual components to study the performance for the overall system.
Modelling languages that possess at least some subset of these properties have been developed in the
hybrid systems literature. Different languages place more emphasis on different aspects, depending
on the applications and problems they are designed to address. In this class we will concentrate
on one such language, called hybrid automata. The hybrid automata we will study are fairly rich
(in terms of descriptive power), but are autonomous, i.e. have no inputs and outputs. They are
therefore unsuitable for studying composition and abstraction properties.
3.2.1 Hybrid Automata
A hybrid automaton is a dynamical system that describes the evolution in time of the values of a
set of discrete and continuous state variables.
Definition 3.1 (Hybrid Automaton) A hybrid automaton H is a collection H = (Q, X, f, Init,
D, E, G, R), where
• Q = {q1, q2, . . .} is a set of discrete states;
• X = Rn
is a set of continuous states;
• f(·, ·) : Q × X → Rn
is a vector field;
• Init ⊆ Q × X is a set of initial states;
• Dom(·) : Q → P(X) is a domain;
• E ⊆ Q × Q is a set of edges;
• G(·) : E → P(X) is a guard condition;
• R(·, ·) : E × X → P(X) is a reset map.
Recall that P(X) denotes the power set (set of all subsets) of X. The notation of Definition 3.1
suggests, for example, that the function Dom assigns a set of continuous states Dom(q) ⊆ Rn
to to
each discrete state q ∈ Q. We refer to (q, x) ∈ Q × X as the state of H.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 22
w
x1
x2
r1
r2
v1 v2
Figure 3.6: The water tank system.
Hybrid automata define possible evolutions for their state. Roughly speaking, starting from an
initial value (q0, x0) ∈ Init, the continuous state x flows according to the differential equation
˙x = f(q0, x),
x(0) = x0,
while the discrete state q remains constant
q(t) = q0.
Continuous evolution can go on as long as x remains in Dom(q0). If at some point the continuous
state x reaches the guard G(q0, q1) ⊆ Rn
of some edge (q0, q1) ∈ E, the discrete state may change
value to q1. At the same time the continuous state gets reset to some value in R(q0, q1, x) ⊆ Rn
.
After this discrete transition, continuous evolution resumes and the whole process is repeated.
To simplify the discussion, we assume from now on that the number of discrete states is finite, and
that for all q ∈ Q, the vector field f(q, ·) is Lipschitz continuous. Recall that this ensures that the
solutions of the differential equation ˙x = f(q, x) are well defined (Chapter 2). Finally, we assume
that for all e ∈ E, G(e) = ∅, and for all x ∈ G(e), R(e, x) = ∅. This assumption eliminates some
pathological cases and in fact be imposed without loss of generality.
As we saw in Chapter 1 and in the examples discussed above, it is often convenient to visualise
hybrid automata as directed graphs (Q, E) with vertices Q and edges E. With each vertex q ∈ Q,
we associate a set of initial states {x ∈ X | (q, x) ∈ Init}, a vector field f(q, ·) : Rn
→ Rn
and a
domain Dom(q) ⊆ Rn
. An edge (q, q ) ∈ E starts at q ∈ Q and ends at q ∈ Q. With each edge
(q, q ) ∈ E, we associate a guard G(q, q ) ⊆ Rn
and a reset function R(q, q , ·) : Rn
→ P(Rn
).
Example (Water Tank System) The two tank system, shown in Figure 3.6, consists of two tanks
containing water. Both tanks are leaking at a constant rate. Water is added to the system at a
constant rate through a hose, which at any point in time is dedicated to either one tank or the other.
It is assumed that the hose can switch between the tanks instantaneously.
For i = 1, 2, let xi denote the volume of water in Tank i and vi > 0 denote the constant flow of
water out of Tank i. Let w denote the constant flow of water into the system. The objective is to
keep the water volumes above r1 and r2, respectively, assuming that the water volumes are above r1
and r2 initially. This is to be achieved by a controller that switches the inflow to Tank 1 whenever
x1 ≤ r1 and to Tank 2 whenever x2 ≤ r2.
It is straight forward to define a hybrid automaton, to describe this process:
• Q = {q1, q2} (two discrete states, inflow going left and inflow going right);
• X = R2
(two continuous states, the level of water in the two tanks);
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 23
q1 q2
x2 ≤ r2
x1 ≤ r1
x1 ≥ r1 ∧ x2 ≥ r2 x1 ≥ r1 ∧ x2 ≥ r2
x := x
x := x
˙x1 = w − v1
˙x2 = −v2
x2 ≥ r2
˙x1 = −v1
˙x2 = w − v2
x1 ≥ r1
Figure 3.7: Graphical representation of the water tank hybrid automaton.
• (when the inflow is going to the tank on the right, the water level in the left tank goes down
while the water level in right tank goes up, and vice verse)
f(q1, x) =
w − v1
−v2
, and f(q2, x) =
−v1
w − v2
;
• Init = {q1, q2} × {x ∈ R2
| x1 ≥ r1 ∧ x2 ≥ r2} (start with both water levels above the low level
marks r1 and r2);
• Dom(q1) = {x ∈ R2
| x2 ≥ r2} and Dom(q2) = {x ∈ R2
| x1 ≥ r1} (put water in the current
tank as long as the level in the other tank is above the low level mark);
• E = {(q1, q2), (q2, q1)} (possible to switch inflow from left to right and vice versa);
• G(q1, q2) = {x ∈ R2
| x2 ≤ r2} and G(q2, q1) = {x ∈ R2
| x1 ≤ r1} (switch the inflow to the
other tanks as soon as the water there reaches the low level mark);
• R(q1, q2, x) = R(q2, q1, x) = {x} (the continuous state does not change as a result of switching
the inflow).
The directed graph corresponding to this hybrid automaton is shown in Figure 3.7.
The directed graphs contain exactly the same information as Definition 3.1. They can therefore be
treated as informal definitions of hybrid automata. It is common to remove the assignment x := x
from an edge of the graph when the continuous state does not change as a result of the discrete
transition corresponding to that edge.
3.2.2 Hybrid Time Sets & Executions
Hybrid automata involve both continuous “flow” determined by differential equations and discrete
“jumps” determined by a directed graph (like an automaton). To characterise the evolution of
the state of a hybrid automaton one has to think of a set of times that contains both continuous
intervals (over which continuous evolution takes place) and distinguished discrete points in time,
when discrete transitions happen. Such a set of times is called a hybrid time set.
Definition 3.2 (Hybrid Time Set) A hybrid time set is a sequence of intervals τ = {I0, I1, . . . , IN } =
{Ii}N
i=0, finite or infinite (i.e. N = ∞ is allowed) such that
• Ii = [τi, τi ] for all i < N;
• if N < ∞ then either IN = [τN , τN ] or IN = [τN , τN ); and
• τi ≤ τi = τi+1 for all i.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 24
0
1
2
3
i
tτ0 τ0
τ1 τ1
τ2 = τ2
τ3 τ3
t1 t2
t3 t4
t5
t6
Figure 3.8: A hybrid time set τ = {[τi, τi ]}3
i=0.
An example of a hybrid time set is given in Figure 3.8. Notice that the right endpoint, τi, of the
interval Ii coincides with the left endpoint, τi+1 of the interval Ii+1 (c.f. the time instants labelled
t2 and t3 in Figure 3.8). The interpretation is that these are the times at which discrete transitions
of the hybrid system take place. τi corresponds to the time instant just before a discrete transition,
whereas τi+1 corresponds to the time instant just after the discrete transition. Discrete transitions
are assumed to be instantaneous, therefore τi = τi+1. The advantage of this convention is that it
allows one to model situations where multiple discrete transitions take place one after the other
at the same time instant, in which case τi−1 = τi = τi = τi+1 (c.f. the interval I2 = [τ2, τ2] in
Figure 3.8).
Despite its somewhat complicated nature, a hybrid time set, τ, is a rather well behaved mathematical
object. For example, there is a natural way in which the elements of the hybrid time set can be
ordered. For t1 ∈ [τi, τi ] ∈ τ and t2 ∈ [τj, τj] ∈ τ we say that t1 precedes t2 (denoted by t1 t2) if
t1 < t2 (i.e. if the real number t1 is less that the real number t2) or if i < j (i.e. if t1 belongs to
an earlier interval than t2). In Figure 3.8, we have t1 t2 t3 t4 t5 t6. In general, given
any two distinct time instants, t1 and t2, belonging to some τ we have that either t1 t2 or t2 t2
(c.f. given any two distinct real numbers x and y, either x < y or y < x). Using mathematical
terminology, one would say that each hybrid time set τ is linearly ordered by the relation .
Given two hybrid time sets τ and ˆτ there is also a natural way to define if one is “shorter” than the
other (τ is called a prefix of ˆτ if it is “shorter”). More formally, we say that τ = {Ii}N
i=0 is a prefix of
ˆτ = {ˆIi}M
i=0 (and write τ ˆτ) if either they are identical, or τ is a finite sequence, N ≤ M (notice
that M can be infinite), Ii = ˆIi for all i = 0, . . . , N − 1, and IN ⊆ ˆIN . We say that τ is a strict
prefix of ˆτ (and write τ ˆτ) if τ ˆτ and τ = ˆτ. In Figure 3.9, τ is a strict prefix of both ˆτ and ˜τ,
but ˆτ is not a prefix of ˜τ and ˜τ is not a prefix of ˆτ. Notice that given τ and ˆτ we may have neither
ˆτ τ nor τ ˆτ (c.f. given two sets of real numbers A ⊆ R and B ⊆ R it is possible to have neither
A ⊆ B nor B ⊆ A). Using mathematical terminology, one would say that the set of all hybrid time
sets is partially ordered by the relation .
Hybrid time sets will be used to define the time horizon over which the states of hybrid systems
evolve. What does it mean for the state to “evolve” over a hybrid time set? For continuous systems
with state x ∈ Rn
such an evolution was a function, x(·) : [0, T ] → Rn
, mapping a time interval [0, T ]
to the set Rn
where the state lives (see Chapter 2). For discrete systems (like the manufacturing
machine example of Chapter 1) whose state takes values in a finite set q ∈ {q1, . . . , qn} such an
evolution was a sequence of states. For hybrid systems, where the state has both a continuous
component x ∈ Rn
and a discrete component q ∈ {q1, . . . , qn} we need to come up with a mixture
of these two notions.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 25
0
1
0
1
0
1
1
2
1
2
1
2
i i i
τ ˆτ˜τ
Figure 3.9: τ ˆτ and τ ˜τ.
Definition 3.3 (Hybrid Trajectory) A hybrid trajectory is a triple (τ, q, x) consisting of a hybrid
time set τ = {Ii}N
0 and two sequences of functions q = {qi(·)}N
0 and x = {xi(·)}N
0 with qi(·) : Ii → Q
and x(·) : Ii → Rn
.
An execution of an autonomous hybrid automaton is a hybrid trajectory, (τ, q, x) of its state variables.
The elements listed in Definition 3.1 impose restrictions on the types of hybrid trajectories that the
hybrid automaton finds “acceptable”.
Definition 3.4 (Execution) An execution of a hybrid automaton H is a hybrid trajectory, (τ, q, x),
which satisfies the following conditions:
• Initial condition: (q0(0), x0(0)) ∈ Init.
• Discrete evolution: for all i, (qi(τi ), qi+1(τi+1)) ∈ E, xi(τi ) ∈ G(qi(τi ), qi+1(τi+1)), and
xi+1(τi+1) ∈ R(qi(τi ), qi+1(τi+1), xi(τi )).
• Continuous evolution: for all i,
1. qi(·) : Ii → Q is constant over t ∈ Ii, i.e. qi(t) = qi(τi) for all t ∈ Ii;
2. xi(·) : Ii → X is the solution to the differential equation
dxi
dt
= f(qi(t), xi(t))
over Ii starting at xi(τi); and,
3. for all t ∈ [τi, τi ), xi(t) ∈ Dom(qi(t)).
Definition 3.4 specifies which of the hybrid trajectories are executions of H and which are not by
imposing a number of restrictions. The first restriction dictates that the executions should start at an
acceptable initial state in Init. For simplicity, we will use (q0, x0) = (q0(τ0), x0(τ0)) ∈ Init to denote
the initial state of an execution (τ, q, x). As for continuous systems, we can assume that τ0 = 0
without loss of generality. The second restriction determines when discrete transitions can take place
and what the state after discrete transitions can be. The requirements relate the state before the
discrete transition (qi(τi ), xi(τi )) to the state after the discrete transition (qi+1(τi+1), xi+1(τi+1)):
they should be such that (qi(τi ), qi+1(τi+1)) is an edge of the graph, xi(τi ) belongs to the guard of
this edge and xi+1(τi+1) belongs the the reset map of this edge. In this context, it is convenient to
think of the guard G(e) as enabling a discrete transition e ∈ E: the execution may take a discrete
transition e ∈ E from a state x as long as x ∈ G(e). The third restriction determines what happens
along continuous evolution, and when continuous evolution must give way to a discrete transition.
The first part dictates that along continuous evolution the discrete state remains constant. The
second part requires that along continuous evolution the continuous state flows according to the
differential equation ˙x = f(q, x). Notice that the differential equation depends on the discrete state
we are currently in (which is constant along continuous evolution). The third part requires that
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 26
0 0.5 1 1.5 2 2.5 3 3.5
−0.2
0
0.2
0.4
0.6
0.8
1
0 0.5 1 1.5 2 2.5 3 3.5
0.5
1.5
2.5
x2
x1
q1
q2
Figure 3.10: Example of an execution of the water tank hybrid automaton.
along continuous evolution the state must remain in the domain, Dom(q), of the discrete state. In
this context, it is convenient to think of Dom(q) as forcing discrete transitions: the execution must
take a transition if the state is about to leave the domain.
Example (Water Tank (cont.)) Figure 3.10 shows an execution of the water tank automaton.
The hybrid time set τ of the execution consists of three intervals, τ = {[0, 2], [2, 3], [3, 3.5]}. The
evolution of the discrete state is shown in the upper plot, and the evolution of the continuous state
is shown in the lower plot. The values chosen for the constants are r1 = r2 = 0, v1 = v2 = 1/2 and
w = 3/4. The initial state is q = q1, x1 = 0, x2 = 1.
A convenient interpretation is that the hybrid automaton accepts (as opposed to generates) executions.
This perspective allows one to consider, for example, hybrid automata that accept multiple
executions for some initial states, a property that can prove very useful when modelling uncertain
system (as illustrated by the thermostat example of Chapter 1).
Definition 3.5 (Classification of executions) An execution (τ, q, x) is called:
• Finite, if τ is a finite sequence and the last interval in τ is closed.
• Infinite, if τ is an infinite sequence, or if the sum of the time intervals in τ is infinite, i.e.
N
i=0
(τi − τi) = ∞.
• Zeno, if it is infinite but
∞
i=0(τi − τi) < ∞.
• Maximal if it is not a strict prefix of any other execution of H.
Figure 3.11 shows examples of hybrid time sets of finite, infinite and Zeno executions.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 27
i
0
0 0 0
1 1 1
1
i i
0
22
1
2
1
0
i i i
τA τB τC
τD τE τF
Figure 3.11: τA finite, τC and τD infinite, τE and τF Zeno.
Exercise 3.3 Show that an execution is Zeno if and only if it takes an infinite number of discrete
transitions in a finite amount of time. Does an execution definer over the hybrid time set τB of
Figure 3.11 belong to any of the classes of Definition 3.5?
3.3 Bibliography and Further Reading
Hybrid systems arise naturally in a number of engineering applications. In addition to the applications
mentioned above, the hybrid paradigm has also been used successfully to address problems in
air traffic control [95], automotive control [15], bioengineering [23], chemical process control [57, 33],
highway systems [99, 44] and manufacturing [83].
The formal definition of hybrid automata is based on a fairly standard class of autonomous hybrid
systems. The notation used here comes from [64, 47]. This class of systems has been studied
extensively in the literature in a number of variations, for a number of purposes, and by a number
of authors. Special cases of the class of systems considered here include switched systems [82],
complementarity systems [97], mixed logic dynamic systems [39], and piecewise linear systems [49]
(the autonomous versions of these, to be more precise). The hybrid automata considered here are a
special case of the hybrid automata of [5] and the impulse differential inclusions of [14] (discussed
in Chapter 7 of these notes), both of which allow differential inclusions to model the continuous
dynamics. They are a special case of the General Hybrid Dynamical Systems of [21], which allow
the continuous state to take values in manifolds (different ones for each discrete state). They are also
a special case of hybrid input/output automata of [68], which, among other things, allow infinitedimensional
continuous state.
Chapter 4
Existence of Executions
4.1 Modelling Issues
Powerful modelling languages, such as hybrid automata, allow one to model a very wide variety
of physical phenomena, but also make it possible to produce models that are unreasonable, either
physically or mathematically. A common danger in hybrid modelling is lack of existence of solutions.
In most of the hybrid languages one can easily construct models that admit no solutions for certain
initial states. Such systems are known as blocking hybrid systems. This is an undesirable property
when modelling physical systems, since it suggests that the mathematical model provides an incomplete
picture of the physical reality: the evolution of the physical system is likely to continue despite
the fact that the evolution of the mathematical model is undefined.
Even if a hybrid system accepts executions for all initial states, it does not necessarily accept
executions with infinite execution times. For example, the executions of hybrid models can take an
infinite number of discrete transitions in finite time. Such executions are known as Zeno executions.
One can argue that physical systems do not exhibit Zeno behaviour. However, modelling abstraction
can often lead to Zeno models of physical systems. Since abstraction is crucial for handling complex
systems, understanding when it leads to Zeno hybrid systems is important.
Another issue that arises in hybrid modelling is lack of uniqueness of solutions. Hybrid systems
that accept multiple executions for a single initial state are known as non-deterministic. It is often
desirable to retain some level of non-determinism in a hybrid model, since it can be used to model
uncertainty (recall the thermostat example of Chapter 1). This, however, requires additional care
when designing controllers for such systems, or when developing arguments about their performance.
A common practice in continuous dynamical systems is to base proofs on arguments about the
solution of the system. This is motivated by the fact that, under fairly general assumptions (Lipschitz
continuity, recall Theorem 2.1), continuous dynamical system have unique solutions. This proof
technique is inadequate for non-deterministic systems. Instead one needs to develop arguments that
hold for all solutions of the system.
Finally, hybrid systems are especially challenging from the point of view of simulation. The problems
faced by the developers of simulation algorithms are intimately related to the modelling problems
discussed so far.
• Existence: simulation algorithms may run into trouble if the simulated model has no solutions.
Incorporating tests for existence in the simulation packages can alleviate this problem. More
challenging is the case of Zeno executions. In this case, unless special care is taken, the
simulation may grind to a halt, or produce spurious results.
• Uniqueness: Non-determinism introduces further complications from the point of view of sim-
28
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 29
ulation. Here the simulation algorithm may be called upon to decide between different alternatives.
When a choice between continuous evolution and discrete transition is possible, a
common approach is to take transitions the moment they are enabled (as-soon-as semantics).
Probabilistic methods have also been proposed for dealing with non-determinism in the context
of simulation.
• Discontinuity: Lack of continuity of the solution with respect to initial conditions, an inherent
characteristic of hybrid systems, can also lead to problems, both theoretical and practical. The
most common problem is event detection (guard crossing).
• Composability: When simulating large scale systems (e.g. the Automated Highway System
of Chapter 3), one would like to be able to build up the simulation by composing different
components (e.g. models for the motion of each vehicle). It may also be desirable to add
components to the simulation on-line (e.g. to model vehicles joining the highway), eliminate
components (e.g. to model vehicles leaving the highway), or redefine the interactions between
components (e.g. to model vehicles changing lanes). Object oriented modelling languages have
been developed to address these needs.
4.2 Two Fundamental Concepts
Reachability is a fundamental concept in the study of hybrid systems (and dynamical systems in
general). Roughly speaking, a state, (ˆq, ˆx) ∈ Q × X of a hybrid automaton H is called reachable
if the hybrid automaton can find its way to (ˆq, ˆx) while moving along one of its executions. The
importance of the concept of reachability is difficult to overstate. In the next section we will show
how reachability plays a central role in the derivation of existence and uniqueness conditions for
executions. Reachability will also turn out to be a key concept in the study of safety properties for
hybrid systems.
More formally,
Definition 4.1 (Reachable State) A state (ˆq, ˆx) ∈ Q × X of a hybrid automaton H is called
reachable if there exists a finite execution (τ, q, x) ending in (ˆq, ˆx), i.e. τ = {[τi, τi ]}N
0 , N < ∞, and
(qN (τN ), xN (τN )) = (ˆq, ˆx).
We will use Reach ⊆ Q × X to denote the set of all states reachable by H. Clearly, Init ⊆ Reach.
Exercise 4.1 Why are all initial states reachable?
Another important concept in the study of existence of executions for hybrid automata is the set of
states from which continuous evolution is impossible. We will call these states transition states. For
(ˆq, ˆx) ∈ Q × X and some > 0, consider the solution, x(·) : [0, ) → Rn
of the differential equation
dx
dt
= f(ˆq, x) with x(0) = ˆx. (4.1)
Notice that, under the assumption that f is Lipschitz continuous in x, the solution to equation (4.1)
exists and is unique (Theorem 2.1). The states, Trans ⊆ Q × X, from which continuous evolution
is impossible are
Trans = {(ˆq, ˆx) ∈ Q × X | ∀ > 0 ∃t ∈ [0, ) such that (ˆq, x(t)) ∈ Dom(ˆq)} .
In words, Trans is the set of states for which continuous evolution along the differential equation
forces the system to exit the domain instantaneously.
The exact characterisation of the set Trans may be quite involved. Clearly, continuous evolution
is impossible for all states outside the domain (refer to Definition 3.4). Therefore, for each discrete
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 30
state q ∈ Q, states in the complement of the domain of q (i.e. the set of all x outside Dom(q),
denoted by Dom(q)c
) must belong to Trans. Mathematically this can be written as
q∈Q
{q} × Dom(q)c
⊆ Trans
If Dom(q) is a closed set (i.e. it contains its boundary), then Trans may also contain pieces of the
boundary of the domain. In the examples considered in this class, it is usually straight forward to
figure out what these parts are going to be.
Example (Water Tank (continued)) Consider again the water tank automaton, and assume
that
0 < v1, v2 < w.
We will show how to compute the sets Reach and Trans for this system.
First of all Reach must contain all initial states. Therefore
Reach ⊇ {q1, q2} × {x ∈ R2
| (x1 ≥ r1) ∧ (x2 ≥ r2)} (4.2)
Can it contain any other states? It turns out that it can not. To see why, we will show using
induction that the state remains in the set Init.
Consider an arbitrary initial state (ˆq, ˆx) ∈ Init and an arbitrary execution (τ, q, x) starting at (ˆq, ˆx).
The fact that (ˆq, ˆx) ∈ Init provides the base case for the induction argument. Assume that for some
i, (qi(τi), xi(τi)) ∈ Init, and consider the case where qi(τi) = q1 (the case qi(τi) = q2 is similar). If
τi > τi, then continuous evolution takes place from (qi(τi), xi(τi)). Along this evolution, the first
component of the continuous state increases (because qi(τi) = q1, therefore ˙x1 = w−v1 and v1 < w).
The second component of the continuous state, on the other hand, decreases, but remains above r2.
This is because, by the definition of an execution,
xi(t) ∈ Dom(q1) = {x ∈ R2
| x2 ≥ r2}
for all t ∈ [τi, τi ]. Therefore, (qi(t), xi(t)) remains in Init along continuous evolution.
If τi = ∞, or if [τi, τi] is the last interval in τ we are done! Otherwise, a discrete transition takes
place from (qi(τi ), xi(τi )). But the reset relation, R, leaves x unaffected, therefore,
(qi+1(τi+1), xi+1(τi+1)) ∈ Init
The last statement is true even if τi = τi .
Summarising, if (qi(τi), xi(τi)) ∈ Init, then (qi(t), xi(t)) ∈ Init for all t ∈ [τi, τi]. Moreover,
(qi+1(τi+1), xi+1(τi+1)) ∈ Init. Therefore, by induction on i, (qi(t), xi(t)) ∈ Init for all i and all
t and
Reach ⊆ {q1, q2} × {x ∈ R2
| (x1 ≥ r1) ∧ (x2 ≥ r2)} (4.3)
Equations (4.2) and (4.3) together imply that
Reach = {q1, q2} × {x ∈ R2
| (x1 ≥ r1) ∧ (x2 ≥ r2)}
To establish the set Trans for the water tank system, notice that continuous evolution is impossible
if q = q1 and x2 < r2 (the inflow will get immediately switched to tank 2) or if q = q2 and x1 < r1.
Therefore,
Trans ⊇ {q1} × {x ∈ R2
| x2 < r2} ∪ {q2} × {x ∈ R2
| x1 < r1}
On the other hand, continuous evolution is possible if q = q1 and x2 > r2, or if q = q2 and x1 > r1.
Therefore
Trans ⊆ {q1} × {x ∈ R2
| x2 ≤ r2} ∪ {q2} × {x ∈ R2
| x1 ≤ r1}
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 31
q q
x ≤ −2
x ≤ −3
x :∈ (−∞, 0]
x :∈ (−∞, 0]
˙x = 1
x ≤ 0
˙x = −1
x ≤ 0
Figure 4.1: Examples of blocking and non-determinism.
How about if q = q1 and x2 = r2? If continuous evolution was to take place from this state, x2 would
immediately go below r2. This is because q = q1 implies that ˙x2 = −v2 < 0 (recall that v2 > 0).
This, however, would imply that the state would leave the domain Dom(q1), which is impossible
along continuous evolution. Therefore, continuous evolution is also impossible from states where
q = q1 and x2 = r2 (and, by a symmetric argument, states where q = q2 and x1 = r1). Overall,
Trans = {q1} × {x ∈ R2
| x2 ≤ r2} ∪ {q2} × {x ∈ R2
| x1 ≤ r1} .
4.3 Local Existence and Uniqueness
Next, we turn our attention to questions of existence of executions. We give some conditions under
which infinite executions exist for all initial states, and conditions under which these executions are
unique.
Definition 4.2 (Non-Blocking and Deterministic) A hybrid automaton H is called non-blocking
if for all initial states (ˆq, ˆx) ∈ Init there exists an infinite execution starting at (ˆq, ˆx). It is called
deterministic if for all initial states (ˆq, ˆx) ∈ Init there exists at most one maximal execution starting
at (ˆq, ˆx).
Roughly speaking, the non-blocking property implies that infinite executions exist for all initial
states, while the deterministic property implies that the infinite executions (if they exist) are unique.
As we have seen, continuous dynamical systems described by differential equations have both these
properties if the vector field f is assumed to be Lipschitz continuous (Theorem 2.1). In hybrid
systems, however, more things can go wrong.
Consider, for example, the hybrid automaton of Figure 4.1. Let (ˆq, ˆx) denote the initial state, and
notice that ˆq = q. If ˆx = −3, executions starting at (ˆq, ˆx) can either flow along the vector field ˙x = 1,
or jump back to q reseting x anywhere in (−∞, 0], or jump to q leaving x unchanged. If ˆx = −2
executions starting at (ˆq, ˆx) can either flow along the vector field, or jump to q . If ˆx = −1 executions
stating at (ˆq, ˆx) can only flow along the vector field. Finally, if ˆx = 0 there are no executions starting
at (ˆq, ˆx), other than the trivial execution defined over [τ0, τ0] with τ0 = τ0. Therefore, the hybrid
automaton of Figure 4.1 accepts no infinite executions for some initial states and multiple infinite
executions for others.
Intuitively, a hybrid automaton is non-blocking if for all reachable states for which continuous
evolution is impossible a discrete transition is possible. This fact is stated more formally in the
following lemma.
Lemma 4.1 A hybrid automaton, H, is non-blocking if for all (ˆq, ˆx) ∈ Reach ∩ Trans, there exists
ˆq ∈ Q such that (ˆq, ˆq ) ∈ E and ˆx ∈ G(ˆq, ˆq ). If H is deterministic, then it is non-blocking if and
only if this condition holds.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 32
Proof: Consider an initial state (q0, x0) ∈ Init and assume, for the sake of contradiction, that there
does not exist an infinite execution starting at (q0, x0). Let χ = (τ, q, x) denote a maximal execution
starting at (q0, x0), and note that τ is a finite sequence.
First consider the case τ = {[τi, τi ]}N−1
i=0 [τN , τN ) and let (qN , xN ) = limt→τN
(qN (t), xN (t)). Note
that, by the definition of execution and a standard existence argument for continuous dynamical
systems, the limit exists and χ can be extended to χ = (τ, q, x) with τ = {[τi, τi ]}N
i=0, qN (τN ) = qN ,
and xN (τN ) = xN . This contradicts the assumption that χ is maximal.
Now consider the case τ = {[τi, τi ]}N
i=0, and let (qN , xN ) = (qN (τN ), xN (τN )). Clearly, (qN , xN ) ∈
Reach. If (qN , xN ) ∈ Trans, then there exists > 0 such that χ can be extended to χ = (τ, q, x)
with τ = {[τi, τi ]}N−1
i=0 [τN , τN + ), by continuous evolution. If, on the other hand (qN , xN ) ∈
Trans, then by assumption there exists (q , x ) ∈ Q × X such that (qN , q ) ∈ E, xN ∈ G(qN , q )
and x ∈ R(qN , q , xN ). Therefore, χ can be extended to χ = (τ, q, x) with τ = {[τi, τi ]}N+1
i=0 ,
τN+1 = τN+1 = τN , qN+1(τN+1) = q , xN+1(τN+1) = x by a discrete transition. In both cases the
assumption that χ is maximal is contradicted.
This argument also establishes the “if” of the second part. For the “only if”, consider a deterministic
hybrid automaton that violates the conditions, i.e., there exists (q , x ) ∈ Reach such that (q , x ) ∈
Trans, but there is no q ∈ Q with (q , q ) ∈ E and x ∈ G(q , q ). Since (q , x ) ∈ Reach, there exists
(q0, x0) ∈ Init and a finite execution, χ = (τ, q, x) starting at (q0, x0) such that τ = {[τi, τi ]}N
i=0 and
(q , x ) = (qN (τN ), xN (τN )).
We first show that χ is maximal. Assume first that there exists χ = (τ, q, x) with τ = {[τi, τi]}N−1
i=0
[τN , τN + ) for some > 0. This would violate the assumption that (q , x ) ∈ Trans. Next assume
that there exists χ = (τ, q, x) with τ = τ[τN+1, τN+1] with τN+1 = τN . This requires that the
execution can be extended beyond (q , x ) by a discrete transition, i.e., there exists (q , x ) ∈ Q × X
such that (q , q ) ∈ E, x ∈ G(q , q ) and x ∈ R(q , q , x ). This would contradict our original
assumptions. Overall, χ is maximal.
Now assume, for the sake of contradiction that H is non-blocking. Then, there exists an infinite
(and therefore maximal) χ starting at (q0, x0). But χ = χ (as the former is finite and the latter
infinite). This contradicts the assumption that H is deterministic.
Intuitively, a hybrid automaton may be non-deterministic if either there is a choice between continuous
evolution and discrete transition, or if a discrete transition can lead to multiple destinations
(recall that continuous evolution is unique by Theorem 2.1). More specifically, the following lemma
states that a hybrid automaton is deterministic if and only if (1) whenever a discrete transition is
possible continuous evolution is impossible, and (2) discrete transitions have unique destinations.
Lemma 4.2 A hybrid automaton, H, is deterministic if and only if for all (ˆq, ˆx) ∈ Reach
1. if ˆx ∈ G(ˆq, ˆq ) for some (ˆq, ˆq ) ∈ E, then (ˆq, ˆx) ∈ Trans;
2. if (ˆq, ˆq ) ∈ E and (ˆq, ˆq ) ∈ E with ˆq = ˆq then ˆx ∈ G(ˆq, ˆq ) ∩ G(ˆq, ˆq ); and,
3. if (ˆq, ˆq ) ∈ E and x ∈ G(ˆq, ˆq ) then R(ˆq, ˆq , ˆx) = {ˆx }, i.e. the set contains a single element,
ˆx .
Proof: For the “if” part, assume, for the sake of contradiction, that there exists an initial state
(q0, x0) ∈ Init and two maximal executions χ = (τ, q, x) and χ = (τ, q, x) starting at (q0, x0) with
χ = χ. Let ¯χ = (¯τ, ¯q, ¯x) denote the maximal common prefix of χ and χ. Such a prefix exists
as the executions start at the same initial state. Moreover, ¯χ is not infinite, as χ = χ. As in
the proof of Lemma 4.1, ¯τ can be assumed to be of the form ¯τ = {[¯τi, ¯τi]}N
i=0. Let (qN , xN ) =
(qN (¯τN ), xN (¯τN )) = (qN (¯τN ), xN (¯τN )). Clearly, (qN , xN ) ∈ Reach. We distinguish the following
four cases:
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 33
Case 1: ¯τN ∈ {τi } and ¯τN ∈ {τi}, i.e., ¯τN is not a time when a discrete transition takes place in
either χ or χ. Then, by the definition of execution and a standard existence and uniqueness argument
for continuous dynamical systems, there exists > 0 such that the prefixes of χ and χ are defined
over {[¯τi, ¯τi ]}N−1
i=0 [¯τN , ¯τN + ) and are identical. This contradicts the fact that ¯χ is maximal.
Case 2: ¯τN ∈ {τi } and ¯τN ∈ {τi}, i.e., ¯τN is a time when a discrete transition takes place in χ but not
in χ. The fact that a discrete transition takes place from (qN , xN ) in χ indicates that there exists q ∈
Q such that (qN , q ) ∈ E and xN ∈ G(qN , q ). The fact that no discrete transition takes place from
(qN , xN ) in χ indicates that there exists > 0 such that χ is defined over {[¯τi, ¯τi ]}N−1
i=0 [¯τN , ¯τN + ).
A necessary condition for this is that (qN , xN ) ∈ Trans. This contradicts condition 1 of the lemma.
Case 3: ¯τN ∈ {τi } and ¯τN ∈ {τi}, symmetric to Case 2.
Case 4: ¯τN ∈ {τi } and ¯τN ∈ {τi}, i.e., ¯τN is a time when a discrete transition takes place in both χ
and χ. The fact that a discrete transition takes place from (qN , xN ) in both χ and χ indicates that
there exist (q , x ) and (q , x ) such that (qN , q ) ∈ E, (qN , q ) ∈ E, xN ∈ G(qN , q ), xN ∈ G(qN , q ),
x ∈ R(qN , q , xN ), and x ∈ R(qN , q , xN ). Note that by condition 2 of the lemma, q = q , hence,
by condition 3, x = x . Therefore, the prefixes of χ and χ are defined over {[¯τi, ¯τi ]}N
i=0[¯τN+1, ¯τN+1],
with ¯τN+1 = ¯τN+1 = ¯τN , and are identical. This contradicts the fact that ¯χ is maximal and
concludes the proof of the “if” part.
For the “only if” part, assume that there exists (q , x ) ∈ Reach such that at least one of the conditions
of the lemma is violated. Since (q , x ) ∈ Reach, there exists (q0, x0) ∈ Init and a finite execution,
χ = (τ, q, x) starting at (q0, x0) such that τ = {[τi, τi ]}N
i=0 and (q , x ) = (qN (τN ), xN (τN )).
If condition 1 is violated, then there exist χ and ˜χ with τ = {[τi, τi ]}N−1
i=0 [τN , τN + ), > 0, and
˜τ = τ[τN+1, τN+1], τN+1 = τN , such that χ χ and χ ˜χ. If condition 2 is violated, there exist
χ and ˜χ with τ = ˜τ = τ[τN+1, τN+1], τN+1 = τN+1 = τN , and qN+1(τN+1) = ˜qN (τN+1), such that
χ χ, χ ˜χ. Finally, if condition 3 is violated, then there exist χ and ˜χ with τ = ˜τ = τ[τN+1, τN+1],
τN+1 = τN+1 = τN , and xN+1(τN+1) = ˜xN+1(τN+1), such that χ χ, χ ˜χ. In all three cases,
let χ and ˜χ denote maximal executions of which χ and ˜χ are prefixes, respectively. Since χ = ˜χ, it
follows that χ = ˜χ. Therefore, there are at least two maximal executions starting at (q0, x0) and
thus H is non-deterministic.
The following theorem is a direct consequence of Lemmas 4.1 and 4.2.
Theorem 4.1 (Existence and Uniqueness) A hybrid automaton H accepts a unique infinite execution
for each initial state if it satisfies all the conditions of Lemmas 4.1 and 4.2.
Important Note: The conditions of the lemmas involve the set of reachable states, Reach. This
is needed only to make the conditions necessary. If all we are interested in is establishing that a
hybrid automaton accepts an infinite executions for all initial states, or that infinite executions are
unique, it suffices to show that the conditions of the lemmas hold for all states (as opposed to all
reachable states). This can make our life considerably easier, since calculating the set of reachable
states is sometimes hard.
Example (Water Tank (continued)) Consider again the water tank automaton with 0 < v1, v2 <
w. Recall that
Reach = {(q, x) ∈ Q × R2
| x1 ≥ r1 ∧ x2 ≥ r2},
Trans = {q1} × {x ∈ R2
| x2 ≤ r2} ∪ {q2} × {x ∈ R2
| x1 ≤ r1}.
Therefore,
Reach ∩ Trans ={q1} × {x ∈ R2
| x1 ≥ r1 ∧ x2 = r2}∪
{q2} × {x ∈ R2
| x2 ≥ r2 ∧ x1 = r1}.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 34
Consider an arbitrary state (ˆq, ˆx) ∈ Reach ∩ Trans (in fact the argument holds for any state
(ˆq, ˆx) ∈ Trans, see “important note” above). Notice that, if ˆq = q1, then
ˆx ∈ {x ∈ R2
| (x1 ≥ r1) ∧ (x2 = r2)} ⊆ G(q1, q2).
Likewise, if q = q2, then x ∈ G(q1, q2). Therefore, the condition of Lemma 4.1 is satisfied, and the
water tank system is non-blocking.
Next, consider an arbitrary reachable state (ˆq, ˆx) ∈ Reach (in fact the argument holds for any state
(ˆq, ˆx) ∈ Q × X). Assume that ˆq = q1 (a similar argument holds if ˆq = q2).
1. If ˆx ∈ G(q1, q2) = {x ∈ R2
| x2 ≤ r2}, then x2 ≤ r2. Therefore (ˆq, ˆx) ∈ Trans.
2. Only one discrete transition is possible from q1 (namely (q1, q2) ∈ E).
3. R(q1, q2, ˆx) = {ˆx} contains one element.
Therefore, the conditions of Lemma 4.2 are also satisfied. By Theorem 4.1, the water tank automaton
accepts a unique infinite execution for each initial state.
4.4 Zeno Executions
The conditions of Theorem 4.1 ensure that a hybrid automaton accepts infinite executions for all
initial states. They do not, however, ensure that the automaton accepts executions defined over
arbitrarily long time horizons. The Lipschitz assumption on f eliminates the possibility of escape to
infinity in finite time along continuous evolution (c.f. finite escape example in Chapter 2). However,
the infinite executions may be such that the state takes an infinite number of discrete transitions in
finite time. Executions with this property are known as Zeno executions.
The name “Zeno” comes from the ancient Greek philosopher, Zeno of Elea. Born around 490BC,
Zeno was a philosopher and one of the founders of the Eleatic school. He was a student of Parmenides,
whose teachings rejected the ideas of plurality and transition as illusions generated by our senses.
The main contribution of Zeno was a series of paradoxes designed to support the view of his mentor
by showing that accepting plurality and motion leads to logical contradictions. One of the better
known ones is the race of Achilles and the turtle.
Achilles, a renowned runner, was challenged by the turtle to a race. Being a fair sportsman,
Achilles decided to give the turtle a 100 meter head-start. To overtake the turtle,
Achilles will have to first cover half the distance separating them, i.e. 50 meters. To cover
the remaining 50 meters, he will first have to cover half that distance, i.e. 25 meters,
and so on. There are an infinite number of such segments and to cover each one of them
Achilles needs a non zero amount of time. Therefore, Achilles will never overtake the
turtle.
This paradox may seem simple minded, but it was not until the beginning of the 20th
century that
it was resolved satisfactorily by mathematicians and philosophers. And it was not until the end of
the 20th
century that it turned out to be a practical problem, in the area of hybrid systems.
The Zeno phenomenon is notoriously difficult to characterise and eliminate in hybrid systems. In
this class we will not examine the properties of Zeno executions in detail. We will only give some
examples of hybrid automata that admit Zeno behaviour.
Example (Chattering System) Consider the hybrid automaton of Figure 4.2. It is easy to show
that this hybrid automaton accepts a unique infinite execution for all initial states. However, all
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 35
q1 q2
x ≥ 0
x ≤ 0
x :∈ (−∞, 0] x :∈ [0, ∞)
˙x = 1
x ≤ 0
˙x = −1
x ≥ 0
x
t
Figure 4.2: Chattering system.
q1 q2
ρ(x) ≥ 0
ρ(x) ≤ 0
x :∈ (−∞, 0)
˙x = 1
ρ(x) ≤ 0
˙x = 1
ρ(x) ≥ 0
ρ(x)
x
Figure 4.3: System with a smooth, non-analytic domain.
infinite executions are Zeno. An execution starting in x0 at time τ0 reaches x = 0 in finite time
τ0 = τ0 + |x0| and takes an infinite number of transitions from then on, without time progressing
further.
This is a phenomenon known in continuous dynamical system as chattering. A bit of thought in
fact reveals that this system is the same as the example used to demonstrate absence of solutions
in Chapter 2. In the control literature the “Zenoness” of such chattering systems is sometimes
eliminated by allowing weaker solution concepts, such as sliding solutions (also known as Filippov
solutions). A more thorough treatment of this topic can be found in [34, 96].
Example (Non-analytic Domain) Consider the hybrid automaton of Figure 4.3. Assume that
the function ρ : R → R that determines the boundary of the domain is of the form
ρ(x) =
sin 1
x2 exp − 1
x2 if x = 0
0 if x = 0
It is easy to check that the automaton is non-blocking and deterministic.
For any > 0, ρ has an infinite number of zero crossings in the interval (− , 0]. Therefore, the
execution of the hybrid automaton with initial state (q1, x0) will take an infinite number of discrete
transitions before time τ0 + |x0| (notice that x0 < 0).
Example (Water Tank (continued)) We have already shown that the water tank hybrid automaton
accepts a unique infinite execution for each initial state if 0 < v1, v2 < w. If in addition the
inflow is less than the sum of the outflows (w < v1 + v2), then all infinite executions are Zeno. It is
easy to show that the execution starting at time τ0 takes an infinite number of transitions by time
τ0 +
x1(τ0) + x2(τ0) − r1 − r2
v1 + v2 − w
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 36
4.5 Bibliography and Further Reading
The simulation of hybrid systems presents special challenges, that need particular attention. Nowadays
general purpose simulation packages such as Matlab and Simulink can deal adequately with
most complications (this was not always the case!) Specialised packages have also been developed
that allow accurate simulation of hybrid systems (at least to the extent that this is possible in theory).
For references see [8, 76, 75, 7]. See also [31] for a compositional language for hybrid system
simulation.
The fundamental properties of existence and uniqueness of solutions, continuity with respect to
initial conditions, etc. naturally attracted the attention of researchers in hybrid systems from fairly
early on. The majority of the work in this area concentrated on developing conditions for wellposedness
(existence and uniqueness of solutions) for special classes of hybrid systems: piecewise
linear systems [46, 56], complementarity systems [97, 37], mixed logic dynamical systems [39], etc.
The discussion in these notes is based on [64, 63, 47].
Continuity of the solutions with respect to initial conditions and parameters has also been studied,
but somewhat less extensively. Motivated by questions of simulation, Tavernini [93] established a
class of hybrid systems that have the property of continuous dependence of solutions for almost
every initial condition. More recently, an approach to the study of continuous dependence on initial
conditions based on the Skorohod topology was proposed [24]. The Skorohod topology, used in
stochastic processes for the space of cadlag functions [18], is mathematically appealing, but tends to
be cumbersome to work with in practice. [64] presents a more practical (but still limited) approach
to the question of continuity.
Zeno executions are treated in [3, 17, 4] from a computer science perspective and [47, 48, 38, 92, 107]
from a control theory perspective. [47, 74] attempt to define extensions of Zeno execution beyond
the Zeno time, motivated by the classical definition of “sliding” flows for discontinuous vector fields.
Chapter 5
Analysis and Synthesis
5.1 Specifications
The reason why we are interested in modelling hybrid systems is that we would like to be able to
analyse the resulting models, and infer some properties of the real system from them. If control
inputs are available, we would also like to be able to design controllers such that the closed loop
hybrid system satisfies certain desirable properties.
Given a hybrid automaton modelling a physical system and some desirable property that we would
like this system to possess (specification), we would like to be able answer the following two
questions:
1. Verification: does the hybrid automaton meet the specification (satisfy the desirable prop-
erty).
2. Synthesis: if there are some design choices to be made (e.g. the system has control inputs
and a controller needs to be designed) can the design be done in such a way that the resulting
system meets the specification.
For real systems, verification and synthesis are usually followed by a process of validation: the
theoretical hybrid design is implemented on a prototype of the real system and tests are performed
to determine whether it meets the specification. It is not uncommon for a design to fail the validation
test, due to factors that were omitted in the hybrid automaton model. The design then needs to be
tuned further and the process of synthesis-verification-validation needs to be repeated.
What kinds of specifications may one want to impose on a hybrid system? A common
specification is stability: one would like to determine whether a hybrid system is stable or asymptotically
stable. If control inputs are available, the problem becomes one of stabilisation: Can one
choose a controller such that the closed loop system is stable or asymptotically stable? Just as
for purely continuous systems, Lyapunov methods are very useful in this case. Both the stability
definitions and Lyapunov theorems need to be appropriately modified to account for the presence
of discrete states. This topic will not be addressed further in this class. For more details, interested
students may want to refer to [30].
In this class we will concentrate primarily on properties that can be encoded as sets of hybrid
trajectories. Recall that a hybrid trajectory (Definition 3.3) is a triple, (τ, q, x) consisting of a
hybrid time set τ and two sequences of functions, q and x mapping each interval of τ to the discrete
states Q and the continuous states Rn
respectively. A specification can be encoded as a set of
desirable hybrid trajectories, H. A hybrid automaton is then said to meet the specification if all
the executions of the hybrid automaton belong to this set H. (Recall that the executions of a
37
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 38
hybrid automaton are also hybrid trajectories, in particular the ones that meet the conditions of
Definition 3.4).
What kind of properties can be encoded like this? The most common are properties that
have to do with reachability. For example, the property
“The state (q, x) always remains in a set of states F ⊆ Q × X”
is one such property, and so is the dual property
“The state (q, x) eventually reaches a set of states F ⊆ Q × X”
The first property is known as a safety property, because the set F can be used to encode “good”
or “safe” states. For example, when analysing the behaviour of two cars following one another on
an automated highway, F can be the set of states for which the two cars have not collided (i.e. the
spacing between them is greater than zero); we would like to ensure that the cars always remain in
the set F (i.e. do not collide). Using notation from Temporal Logic this safety property can be
written as
((q, x) ∈ F)
stands for “always”; the way to read the above formula is “always (q, x) is in F”.
The second property (“The state (q, x) eventually reaches F”) is known as a liveness property.
It reflects the fact that something good should eventually happen to our system. For example, cars
on an automated highway not only want to avoid collisions with other cars, but also want to reach
their destination. In the temporal logic notation this property can be written as
♦((q, x) ∈ F)
♦ stands for “eventually”; the way to read the above formula is “eventually (q, x) is in F”.
Using concepts like these one can encode arbitrarily complex properties. For example the property
♦((q, x) ∈ F)
stands for “always, eventually (q, x) is in F”, or in other words, the state visits the set F “infinitely
often”. Another example is
♦ ((q, x) ∈ F)
which stands for “eventually always (q, x) is in F”, or in other words, (q, x) reaches F at some point
and stays there for ever after. And so on.
How can one check that a hybrid automaton meets such a specification? Roughly speaking
there are three different approaches to this problem:
1. Model Checking: For certain classes of hybrid systems the process can be carried out completely
automatically. The system and the specification are encoded in an appropriate programming
language, and given to a computer to analyse. After a few minutes/hours/days/weeks
the computer either runs out of memory, or comes back with an answer: “The system satisfies
the specification”, or “The system does not satisfy the specification”. In the latter case the
computer also generates an execution of the hybrid automaton that fails to meet the specification;
such an execution is known as a witness. The witness is useful for redesigning the
system. The basics of this approach will be given in Chapter 6.
2. Deductive: Induction arguments, progress variables, etc. are used to develop a proof that the
system meets the specification. Most of the work in structuring the proof has to be done my
hand. Computational theorem proving tools may then be used to check the individual steps
of the proof. The basics of this approach will be the topic of the rest of this handout.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 39
3. Optimal Control and Viability Theory: Reachability problems can also be encoded in
an optimal control or viability theory setting. The optimal control approach requires some
rather advanced machinery from optimal control theory and will not be covered in this class.
The viability theory approach will be introduced in Chapter 7. Most of the work with these
approaches has to be done analytically (by hand!) Because optimal control problems are
notoriously difficult to solve analytically one often has to resort to numerical tools (PDE
solvers, etc.) to approximate the solution.
5.2 Deductive Methods
In the rest of this chapter we will introduce some basic principles of deductive analysis, motivated
by the reachability problem. First of all notice that
Proposition 5.1 A hybrid automaton H satisfies a specification ((q, x) ∈ F) if and only if
Reach ⊆ F.
Exercise 5.1 Prove Proposition 5.1.
Deductive arguments aim to establish bounds on Reach through invariant sets. The definition
of “invariant set” for hybrid automata is a direct generalisation of the definition for continuous
dynamical systems: a set of states is called invariant if all executions of the hybrid automaton
starting in that set remain in that set for ever. More formally,
Definition 5.1 (Invariant Set) A set of states, M ⊆ Q × X, of a hybrid automaton, H, is called
invariant if for all (ˆq, ˆx) ∈ M, all executions (τ, q, x) starting at (ˆq, ˆx), all Ii ∈ τ and all t ∈ Ii we
have that (qi(t), xi(t)) ∈ M.
In the above statement “execution (τ, q, x) starting at (ˆq, ˆx)” refers to a hybrid trajectory with
(q0(τ0), x0(τ0)) = (ˆq, ˆx) that satisfies the discrete and continuous evolution conditions of Definition
3.4, but not necessarily the initial condition (i.e. we allow (ˆq, ˆx) ∈ Init in Definition 5.1).
Students are asked to forgive this slight abuse of the terminology.
The following fact is a direct consequence of the definition.
Proposition 5.2 Consider a hybrid automaton H.
1. The union and intersection of two invariant sets of H are also invariant sets of H.
2. If M is an invariant set and Init ⊆ M, then Reach ⊆ M.
Exercise 5.2 Prove Proposition 5.2.
The two parts of the proposition can be used together to provide progressively tighter bounds on
Reach, by figuring out invariant sets that contain Init and then taking their intersection. Given a
specification of the form ((q, x) ∈ F), the idea is to find an invariant set that contains Init (and
hence Reach) and is contained in F, i.e.
Init ⊆ M ⊆ F.
How does one prove that a set is invariant? Usually by induction. Assume we suspect that a certain
set of states, M ⊆ Q×Rn
, may be invariant. First of all we may want to check that the initial states
are contained in the set M (otherwise M may turn out to be useless for proving safety properties).
Then we check that if continuous evolution starts from a state in M then it remains in M throughout.
In other words, we check that for all T ≥ 0, if
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 40
• (ˆq, ˆx) ∈ M, and
• x : [0, T ] → Rn
is the solution to dx
dt = f(ˆq, x) starting at x(0) = ˆx, and
• x(t) ∈ Dom(ˆq) for all t ∈ [0, T ),
then
• (ˆq, x(t)) ∈ M for all t ∈ [0, T ]
Exercise 5.3 Show that it is sufficient that (ˆq, x(T )) ∈ M (i.e. we do not need to check (ˆq, x(t)) ∈ M
at intermediate times). This is not difficult, but requires a bit of thought.
Finally, we check that if a discrete transition is possible from somewhere in M, then the state after
the discrete transition is also in M. In other words, if
• (ˆq, ˆx) ∈ M, and
• (ˆq, ˆq ) ∈ E, and
• ˆx ∈ G(ˆq, ˆq )
then
• R(ˆq, ˆq , ˆx) ⊆ M
We have actually seen this procedure in practice already: these were the steps we followed to
determine the set of states reachable by the water tank system.
5.3 Bibliography and Further Reading
Of the analysis questions listed in this chapter, the one that has arguably attracted the most attention
if the question of stability of equilibria and invariant sets. Most of the work in this area has
concentrated on extensions of Lyapunov’s Direct Method to the hybrid domain [106, 20, 79]. The
work of [50] provided effective computational tools, based on Linear Matrix Inequalities, for applying
these results to a class of piecewise linear systems. [64] discuss extensions of LaSalle’s Method and
Lyapunov’s Indirect Method to the hybrid domain. Related to the latter is also the work of [45, 105],
where a direct study of the stability of piecewise linear systems is developed. For an excellent
overview of the literature in this area the reader is referred to [30].
The corresponding synthesis problem of stabilisation has been somewhat less extensively studied.
Much of the work in this area deals with switched systems (usually linear and/or planar). The
proposed stabilisation schemes typically involve selecting appropriate times for switching between a
set of given systems [82, 102, 60, 59, 105]. In some cases this approach has been extended to robust
stabilisation schemes for systems that involve certain types of uncertainty [89, 45].
Temporal logic is widely used in computer to encode properties given as sets of trajectories (safety
properties, etc.) as well as dynamics for discrete systems. A very thorough treatment can be found
in [70, 71].
Deductive methods are commonly used with discrete systems; see [70, 71, 67] for an overview. One
way of formally extending deductive arguments to the hybrid domain is presented in [22, 68, 72];
the approach of [22, 68] has been applied to a number of examples, primarily to establish the safety
of transportation systems [40, 101, 32, 65, 62, 61].
Deductive arguments can be automated (at least partly) using theorem provers. One tool that
provides computational support for deductive arguments for hybrid systems is STeP [73].
Chapter 6
Model Checking and Timed
Automata
Finite state systems are relatively easy to work with because one can investigate their properties
by systematically exploring their states. For example, one can decide if a finite state system will
eventually visit a particular set of states by following the system trajectories one by one. This is
tedious to do by hand, but is easy to implement on a computer. Moreover, the process is guaranteed
to terminate: since the number of states is finite, sooner or later we will find ourselves visiting the
same states over and over again. At this point either the desired set has already been reached, or,
if not, it will never be reached.
With hybrid systems it is in general impossible to do this. Because the number of states is infinite,
it is impossible to enumerate them and try to explore them one by one. However, there are hybrid
systems for which one can find a finite state system which is, in some sense, equivalent to the hybrid
system. This is usually done by partitioning the state space into a finite number of sets with the
property that any two states in a give set exhibit similar behaviour. Then, to decide whether the
hybrid system has certain properties, one has to work with the finite sets of the partition, as opposed
to the infinite states of the original hybrid system. Moreover, the generation and analysis of the
finite partition can be carried out automatically by a computer.
The process of automatically analysing the properties of systems by exploring their state space
is known as model checking. In this handout we discuss some fundamental ideas behind model
checking, and introduce a class of hybrid systems, known as timed automata, that are amenable to
this approach. As with deductive methods the discussion will be motivated by safety (reachability)
analysis. Because of the complexity of the material we will not develop the results in their full
beauty and generality. A good starting point for a deeper study is [5].
6.1 Transition Systems
We first introduce a very general class of dynamical systems, known as transition systems, on which
the above questions can be formulated.
Definition 6.1 (Transition System) A transition system, T = (S, δ, S0, SF ) consists of
• A set of states S (finite or infinite);
• A transition relation δ : S → P(S);
• A set of initial states S0 ⊆ S;
41
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 42
q0
q1 q2
q3 q4 q5 q6
Figure 6.1: Finite state transition system.
• A set of final states SF ⊆ S.
The set of final states is included because we are interested in reachability type specifications. We
will use it to encode desired final states, sets of states in which we want to stay, etc.
A trajectory of a transition system is finite or infinite sequence of states {si}N
i=0 such that
1. s0 ∈ S0; and,
2. si+1 ∈ δ(si) for all i = 0, 1, . . . , N − 1.
Example (Finite State Transition System) A transition system with finite states is shown in
Figure 6.1. The formal definition of the system is
1. S = {q0, . . . , q6};
2. δ(q0) = {q0, q1, q2}, δ(q1) = {q0, q3, q4}, δ(q2) = {q0, q5, q6}, δ(q3) = δ(q4) = δ(q5) = δ(q6) = ∅;
3. S0 = {q0} (denoted by an arrow pointing to q0);
4. SF = {q3, q6} (denoted by a double circle).
Example (Transition System of a Hybrid Automaton) Hybrid automata can be transformed
into transition systems by abstracting away time. Consider a hybrid automaton H =
(Q, X, Init, f, Dom, E, G, R) together with a distinguished “final” set of states F ⊆ Q × X. We
will define a transition system for the hybrid automaton. Start with
• S = Q × X, i.e. s = (q, x)
• S0 = Init
• SF = F.
The transition relation δ can be defined in many parts: a discrete transition relation δe : S → P(S)
for each edge e ∈ E of the graph and a continuous transition relation δC : S → P(S) to model the
passage of time. For each e = (q, q ) ∈ E define
δe(ˆq, ˆx) =
{q } × R(e, ˆx) if (ˆq = q) and (ˆx ∈ G(e))
∅ if (ˆq = q) or (x ∈ G(e))
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 43
For the continuous transition relation let
δC(ˆq, ˆx) = {(ˆq , ˆx ) ∈ Q × X | [ˆq = ˆq] ∧ [∃T ≥ 0, (x(T ) = ˆx ) ∧ (∀t ∈ [0, T ], x(t) ∈ Dom(ˆq))]}
where x(·) denotes the solution of the differential equation
˙x = f(ˆq, x) starting at x(0) = ˆx
The overall transition relation is then
δ(s) = δC(s) ∪
e∈E
δe(s)
In words, a transition from s ∈ S to s ∈ S is possible in the transition system if either a discrete
transition e ∈ E of the hybrid system will bring s to s , or s can flow continuously to s after some
time. Notice that in the last statement time has been abstracted away. We do not care how long it
takes to get from s to s , we only care whether it is possible to get there eventually. The transition
system captures the sequence of “events” that the hybrid system may experience, but not the timing
of these events.
Transition systems are designed to allow one to answer reachability (and other) questions algorithmically.
For example, say we would like to answer the question
“Does there exist a trajectory of T such that si ∈ SF for some i?”
If this is the case we say that SF is reachable. We can approach this question using the predecessor
operator
Pre : P(S) → P(S)
which for each set of states ˆS ⊆ S is defined as
Pre( ˆS) = {s ∈ S | ∃ˆs ∈ ˆS with ˆs ∈ δ(s)}
The operator Pre takes a set of states, ˆS, and returns the states that can reach ˆS in one transition.
The following algorithm can then be used to determine if SF is reachable.
Algorithm 1 (Backwards Reachability)
initialisation: W0 = SF , i = 0
repeat
if Wi ∩ S0 = ∅
return “SF reachable”
end if
Wi+1 = Pre(Wi) ∪ Wi
i = i + 1
until Wi = Wi−1
return “SF not reachable”
Using an induction argument it is easy to show that if the algorithm terminates (i.e. at some point
it returns “SF reachable” or “SF not reachable”) then it produces the right answer.
Exercise 6.1 Show this.
Exercise 6.2 Define an appropriate operator Post : P(S) → P(S) that for each set of states ˆS ⊆ S
returns the set of states that can be reached from ˆS in one transition. Hence develop a forward
reachability algorithm.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 44
This algorithm is written in what is known as pseudo-code. It is conceptually useful, but is still
a long way from being implementable on a computer. To effectively implement the algorithm one
needs to figure out a way to explain to the computer how to
1. store sets of states,
2. compute the Pre of a set of states,
3. take the union and intersection of sets of states,
4. check whether a set of states is empty, and
5. check whether two sets of states are equal.
If the number of states S is finite all of these are relatively easy to do by enumerating the states.
None of these steps are completely straight forward, however, if the state has real valued components
(as is the case with hybrid systems).
Even if one was able to perform all of these operations using a computer program, it is still unclear
whether the program would always produce an answer to the reachability question. The above
algorithm may come up with the answer “SF reachable”, the answer “SF not reachable”, but it may
also come up with no answer at all. This will be the case if new states get added to Wi each time we
go around the repeat-until loop (hence Wi+1 = Wi) but none of these states belongs to S0 (hence
Wi+1 ∩ S0 = ∅).
Example (Non-Terminating System) Consider the transition system T = (S, δ, S0, SF ) with
S = R,
δ(x) = 2x
S0 = {−1}, SF = {1}. The Backwards Reachability algorithm produces the following sequence of
sets:
W0 = {1}, W1 = {1,
1
2
}, . . . , Wi = {1,
1
2
, . . . ,
1
2
i
}, . . .
Notice that Wi+1 contains one more element that Wi, therefore we will never have Wi = Wi+1.
Moreover, −1 will never be in Wi, therefore Wi ∩ S0 = ∅. Hence the algorithm will not terminate.
With finite state systems termination is not a problem: the set Wi will sooner or later stop growing.
Example (Finite State Transition System (cont.)) When applied to the finite state system
of Figure 6.1 the Backwards Reachability Algorithm produces the following sequence of sets:
W0 = {q3, q6}, W1 = {q1, q2, q3, q6}, W2 = {q0, q1, q2, q3, q6}
Notice that W2 ∩ S0 = {q0} = ∅. Therefore, after two steps the algorithm terminates with the
answer “SF reachable”.
Exercise 6.3 Assume the set S is finite and contains M states. Give an upper bound on the number
of times the algorithm will have to perform the “repeat-until” loop.
6.2 Bisimulation
Since finite state systems are so much easier to work with, we are going to try to turn our infinite
state systems into finite state ones, by grouping together states that have “similar” behaviour. Such
a grouping of states is called a partition of the state space. A partition is a collection of sets of
states, {Si}i∈I, with Si ⊆ S, such that
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 45
1. Any two sets, Si and Sj, in the partition are disjoint, i.e. Si ∩Sj = ∅ for all i, j ∈ I with i = j.
(A family of sets with this property is called mutually disjoint).
2. The union of all sets in the partition is the entire state space, i.e.
i∈I
Si = S
(A family of sets with this property is said to cover the state space).
The index set, I, of the partition may be either finite or infinite. If I is a finite set (e.g. I =
{1, 2, . . ., M} for M < ∞) then we say that the partition {Si}i∈I is a finite partition.
Example (Finite State Transition System (cont.)) The collection of sets
{q0}, {q1, q2}, {q3, q6}, {q4, q5}
is a partition of the state space S of the finite system of Figure 6.1. The collection
{q0}, {q1, q3, q4}, {q2, q5, q6}
is also a partition. However, the collection
{q1, q3, q4}, {q2, q5, q6}
is not a partition, and neither is
{q0, q1, q3, q4}, {q0, q2, q5, q6}
Given a transition system, T = (S, δ, S0, SF ) and a partition of the state space {Si}i∈I we can define
a transition system whose states are the elements of the partition Si ⊆ S, rather than individual
states s ∈ S. This transition system ˆT = ( ˆS, ˆδ, ˆS0, ˆSF ) is defined as
• ˆS = {Si}i∈I, i.e. the states are the sets of the partition;
• ˆδ allows a transition from one set in the partition (say Si) to another (say Sj) if and only if
δ allows a transition from some state in Si (say s ∈ Si) to some state in Sj (say s ∈ Sj). In
mathematical notation,
ˆδ(Si) = {Sj | ∃s ∈ Si, ∃s ∈ Sj such that s ∈ δ(s)}
• A set in the partition (say Si) is in the initial set of ˆT (i.e. Si ∈ ˆS0) if and only if some element
of Si (say s ∈ Si) is an initial state of the original transition system (i.e. s ∈ S0).
• A set in the partition (say Si) is a final set of ˆT (i.e. Si ∈ ˆSF ) if and only if some element of
Si (say s ∈ Si) is a final state of the original transition system (i.e. s ∈ SF ).
Exercise 6.4 Show that the above definitions are equivalent to ˆδ(Si) = {Sj | δ(Si) ∩ Sj = ∅},
Si ∈ ˆS0 ⇔ Si ∩ S0 = ∅, Si ∈ ˆSF ⇔ Si ∩ SF = ∅. You need to define δ(Si) appropriately, but
otherwise this is a tautology.
The transition system generated by the partition is known as the quotient transition system. Notice
that if the partition is finite, then the quotient transition system ˆT is a finite state system and
therefore can be easily analysed.
Using this method we can in principle construct finite state systems out of any transition system.
The problem is that for most partitions the properties of the quotient transition system do not allow
us to draw any useful conclusions about the properties of the original system. However, there is
a special type of partition for which the quotient system ˆT is in a sense equivalent to the original
transition system, T . This type of partition is known as a bisimulation.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 46
Definition 6.2 (Bisimulation) A bisimulation of a transition system T = (S, δ, S0, SF ) is a partition
{Si}i∈I of the state space S of T such that
1. S0 is a union of elements of the partition,
2. SF is a union of elements of the partition,
3. if one state (say s) in some set of the partition (say Si) can transition to another set in the
partition (say Sj), then all other states, ˆs in Si must be able to transition to some state in Sj.
More formally, for all i, j ∈ I and for all states s, ˆs ∈ Si, if δ(s) ∩ Sj = ∅, then δ(ˆs) ∩ Sj = ∅.
Exercise 6.5 Show that a partition {Si}i∈I is a bisimulation if and only if conditions 1 and 2 above
hold and 3 is replaced by “for all i, Pre(Si) is a union of elements of {Si}i∈I”.
Example (Finite Transition System (cont.)) The partition
{q0}, {q1, q2}, {q3, q6}, {q4, q5}
is a bisimulation of the finite system of Figure 6.1. Let us test this:
1. S0 = {q0} which is an element of the partition;
2. SF = {q3, q6} which is also an element of the partition;
3. Let us study the third condition for the set {q1, q2}. From q1 one can jump to the following
sets in the partition
{q0}, {q3, q6}, {q4, q5}
From q2 one can jump to exactly the same sets in the partition. Therefore the third condition
is satisfied for set {q1, q2}. It is also easy to check this condition for the remaining sets (for
the set {q0} the third condition is trivially satisfied).
The partition
{q0}, {q1, q3, q4}, {q2, q5, q6}
on the other hand, is not a bisimulation. For example, SF is not a union of elements of the
partition. Also, from q1 one can transition to q0, whereas from q3 and q4 (the other elements of the
set {q1, q3, q4}) one cannot transition to q0.
Bisimulations are important because of the following property.
Theorem 6.1 Let {Si}i∈I be a bisimulation of a transition system, T , and let ˆT be the quotient
transition system. SF is reachable by T if and only if ˆSF is reachable by ˆT.
(NB. This is a simplified version of a much deeper theorem. In fact bisimulations preserve not only
reachability properties, but any kind of property that can be written as a formula in a temporal
logic known as the Computation Tree Logic (CTL).)
This is a very important and useful result. For finite state systems its implications are mostly in
terms of computational efficiency. If we can find a bisimulation of the finite state system (like we
did in the finite state example discussed above) we can study reachability in the quotient system
instead of the original system. The advantage is that the quotient system will in general be much
smaller that the original system. In the above example, the quotient system had 4 states whereas
the original system had 7.
The implications are much more profound for infinite state systems. Even when the original transition
system has an infinite number of states, sometimes we may be able to find a bisimulation that
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 47
consists of a finite number of sets. Then we will be able to answer reachability questions for the
infinite state system by studying an equivalent finite state system. Since finite state systems are so
much easier to work with this could be a very big advantage. A class of hybrid systems for which
we can always find finite bisimulations will be introduced in the next section.
The following algorithm can be used to find a bisimulation of a transition system T = (S, δ, S0, SF ).
Algorithm 2 (Bisimulation)
initialisation: P = {S0, SF , S \ (S0 ∪ SF )}
while there exists Si, Sj ∈ P such that Si ∩ Pre(Sj) = ∅ and Si ∩ Pre(Sj) = Si do
Si = Si ∩ Pre(Sj)
Si = Si \ Pre(Sj)
P = (P \ Si) ∪ {Si, Si }
end while
return P
The symbol \ in the algorithm stands for set difference: Si \ Pre(Sj) is the set that contains all
elements of Si that are not elements of Pre(Sj), in other words
Si \ Pre(Sj) = {s ∈ S | (s ∈ Si) ∧ (s ∈ Pre(Sj))}
The algorithm maintains a partition of the state space, denoted by P, which gets refined progressively
so that it looks more and more like a bisimulation. The definition of the bisimulation suggests that
if P is to be a bisimulation then it must at least allow us to “distinguish” the initial and final states.
We therefore start with a partition that contains three sets: S0, SF and everything else S \(S0 ∪SF ),
i.e.
P = {S0, SF , S \ (S0 ∪ SF )}
At each step of the algorithm, we examine the sets of the candidate partition. Assume we can find
two sets Si, Sj ∈ P such that Pre(Sj) contains some elements of Si (i.e. Si ∩Pre(Sj) = ∅) but not all
of them (i.e. Si ⊆ Pre(Sj), or, equivalently, Si ∩ Pre(Sj) = Si). Then some states s ∈ Si may find
themselves in Sj after one transition (namely those with s ∈ Si ∩ Pre(Sj)), while others cannot do
the same (namely those with s ∈ Si \ Pre(Sj)). This is not allowed if P is to be a bisimulation. We
therefore replace Si by two sets: the states in Si that can transition to Sj (Si = Si ∩ Pre(Sj)) and
the states in Si that cannot transition to Sj (Si = Si \ Pre(Sj)). Notice that after the replacement
P has one more set than it did before. The process is repeated until for all sets Si, Sj ∈ P either
Si ∩ Pre(Sj) = ∅ or Si ∩ Pre(Sj) = Si. The resulting collection of sets, P is a bisimulation. In fact:
Theorem 6.2 If the Bisimulation Algorithm terminates it will produce the coarsest bisimulation of
the transition system (i.e. the bisimulation containing the smallest number of sets).
For finite state systems this algorithm is easy to implement (by enumerating the states) and will
always terminate.
Example (Finite State Transition System (cont.)) Let us apply the bisimulation algorithm
to the finite system of Figure 6.1. Initially
P = {S0, SF , S \ (S0 ∪ SF )} = {{q0}, {q3, q6}, {q1, q2, q4, q5}}
Notice that Pre({q3, q6}) = {q1, q2}. This is not an element of the partition P. It intersects
{q1, q2, q4, q5} but is not equal to it. We therefore split {q1, q2, q4, q5} into two sets
{q1, q2, q4, q5} ∩ Pre({q3, q6}) = {q1, q2}
and
{q1, q2, q4, q5} \ Pre({q3, q6}) = {q4, q5}
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 48
After one iteration of the algorithm the partition becomes
P = {{q0}, {q3, q6}, {q1, q2}, {q4, q5}}
It is easy to check that this is a bisimulation. Clearly S0 and SF are elements of the partition.
Moreover,
Pre({q0}) = {q0, q1, q2}
which is a union of elements of the partition, and so on.
The problem with using the bisimulation algorithm on finite state systems is that it may be more
work to find a bisimulation than to investigate the reachability of the original system. Sometimes
bisimulations can be computed by “inspection”, by taking advantage of symmetries of the transition
structure. In the above example, we can immediately see that the left sub-tree is a mirror image of
the right sub-tree. This should make us suspect that there is a bisimulation lurking somewhere in
the system. There is an entire community in computer science that develops methods for detecting
and exploiting such symmetries.
When we try to apply the bisimulation algorithm to infinite state systems we face the same problems
we did with the Backward Reachability algorithm: how to store sets of states in the computer, how
to compute Pre, etc. Moreover, even in cases where we can do all these, the algorithm may never
terminate. The reason is that not all infinite state transition systems have finite bisimulations. In
the next section we will introduce a class of (infinite state) hybrid systems for which we can not
only implement the above algorithm in a computer, but also ensure that it will terminate in a finite
number of steps.
6.3 Timed Automata
Timed automata are a class of hybrid systems that involve particularly simple continuous dynamics:
all differential equations are of the form ˙x = 1 and all the domains, guards, etc. involve comparison
of the real valued states with constants (x = 1, x < 2, x ≥ 0, etc.). Clearly timed automata are
somewhat limited when it comes to modelling physical systems. They are very good however for
encoding timing constraints (“event A must take place at least 2 seconds after event B and not
more than 5 seconds before event C”, etc.). For some applications, such as multimedia, Internet
and audio protocol verification, etc. this type of description is sufficient for both the dynamics of
the system and the properties that we want the system to satisfy. We conclude this chapter with a
brief discussion of the properties of timed automata. Because complicated mathematical notation
is necessary to formally introduce the topic we will give a rather informal exposition. Students
interested in the details are referred to the (rather technical but classic) paper [2].
Consider x ∈ Rn
. A subset of Rn
set is called rectangular if it can be written as a finite boolean
combination of constraints of the form xi ≤ a, xi < b, xi = c, xi ≥ d, and xi > e, where a, b, c, d, e
are rational numbers. Roughly speaking, rectangular sets are “rectangles” in Rn
whose sides are
aligned with the axes, or unions of such rectangles. For example, in R2
the set
(x1 ≥ 0) ∧ (x1 ≤ 2) ∧ (x2 ≥ 1) ∧ (x2 ≤ 2)
is rectangular, and so is the set
((x1 ≥ 0) ∧ (x2 = 0)) ∨ ((x1 = 0) ∧ (x2 ≥ 0))
The empty set is also a rectangular set (e.g. ∅ = (x1 ≥ 1) ∧ (x1 ≤ 0)). However the set
{x ∈ R2
| x1 = 2x2}
is not rectangular.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 49
q1 q2
x2 > 2
x1 > 4
x1 := 3 ∧ x2 := 0
x1 := 0
x1 = x2 = 0
˙x1 = 1
˙x2 = 1
x2 ≤ 3
˙x1 = 1
˙x2 = 1
x1 ≤ 5
Figure 6.2: Example of a timed automaton.
Exercise 6.6 Draw these sets in R2
. You should immediately be able to see why rectangular sets
are called rectangular.
Notice that rectangular sets are easy to encode in a computer. Instead of storing the set itself (which
is impossible since the set is infinite) we can store and manipulate the list of constraints used to
generate the set (which is finite).
Roughly speaking, a timed automaton is a hybrid automaton which
• involves differential equations of the form ˙xi = 1. Continuous variables governed by this
differential equation are known as clocks.
• the sets involved in the definition of the initial states, guards and domain are rectangular sets
• the reset is either a rectangular set, or may leave certain states unchanged.
Example (Timed Automaton) An example of a timed automaton is given in Figure 6.2. We
have
• Q = {q1, q2};
• X = R2
;
• f(q1, x) = f(q1, x) =
1
1
;
• Init = {(q1, (0, 0))};
• Dom(q1) = {x ∈ R2
| x2 ≤ 3}, Dom(q2) = {x ∈ R2
| x1 ≤ 5};
• E = {(q1, q2), (q2, q1)};
• G(q1, q2) = {x ∈ R2
| x2 > 2}, G(q2, q1) = {x ∈ R2
| x1 > 4};
• R(q1, q2, x) = {(3, 0)}, R(q2, q1, x) = {(0, x2)}
Exercise 6.7 Is this timed automaton non-blocking? Is it deterministic?
Notice that in the timed automaton of the example all the constants that appear in the definition
are non-negative integers. It turns out that we can in general assume that this is the case: given
any timed automaton whose definition involves rational and/or negative constants we can define
an equivalent timed automaton whose definition involves only non-negative integers. This is done
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 50
x1
x2
1
1
2
2
3
3
4 5
Figure 6.3: Region graph for the timed automaton of Figure 6.2.
by “scaling” (multiplying by an appropriate integer) and “shifting” (adding an appropriate integer)
some of the states.
We can turn timed automata into transition systems by “abstracting away” time, just like we did
for general hybrid systems above. It turns out that the transition system corresponding to a timed
automaton always has a finite bisimulation. One standard bisimulation that works for all timed
automata is the region graph. The region graph for the timed automaton of Figure 6.2 is shown in
Figure 6.3.
We will briefly describe the way the region graph is constructed. Assume that all the constants
that appear in the definition of the timed automaton are non-negative integers (this can be done
without loss of generality as noted above). As usual, let us label the continuous variables (clocks) as
x1, . . . , xn. Let Ci be the largest constant with which xi is compared in any of the sets used in the
definition of the timed automaton (initial sets, guards, etc.). In the example C1 = 5 and C2 = 3. If
all we know about the timed automaton is these bounds Ci, xi could be compared with any integer
M with 0 ≤ M ≤ Ci in some guard, reset or initial condition set. Therefore, the discrete transitions
of the timed automaton may be able to “distinguish” states with xi < M from states with xi = M
and from states with xi > M, for all 0 ≤ M ≤ Ci. Distinguish means, for example, that a discrete
transition may be possible from a state with xi < M but not from a state with xi > M (because
the guard contains the condition xi < M). Because these sets may be distinguished by the discrete
transitions we add them to our candidate bisimulation. In the example this gives rise to the sets
for x1 : x1 ∈ (0, 1), x1 ∈ (1, 2), x1 ∈ (2, 3), x1 ∈ (3, 4), x1 ∈ (4, 5), x1 ∈ (5, ∞)
x1 = 0, x1 = 1, x1 = 2, x1 = 3, x1 = 4, x1 = 5,
for x2: x2 ∈ (0, 1), x2 ∈ (1, 2), x2 ∈ (2, 3), x2 ∈ (3, ∞)
x2 = 0, x2 = 1, x2 = 2, x2 = 3.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 51
The product of all these sets, i.e. the sets
{x ∈ R2
| x1 ∈ (0, 1) ∧ x2 ∈ (0, 1)}
{x ∈ R2
| x1 ∈ (0, 1) ∧ x2 = 1}
{x ∈ R2
| x1 = 1 ∧ x2 ∈ (0, 1)}
{x ∈ R2
| x1 = 1 ∧ x2 = 1}
{x ∈ R2
| x1 ∈ (1, 2) ∧ x2 ∈ (3∞)}, etc.
define all the sets in R2
that the discrete dynamics (initial states, guards, domain and reset relations)
can distinguish. Notice that in the continuous state space R2
these product sets are open squares
(squares without their boundary), open horizontal and vertical line segments (line segments without
their end points), points on the integer grid and open, unbounded rectangles (when some xi > Ci).
Since ˙x1 = ˙x2 = 1, time flow makes the continuous state move diagonally up along 45◦
lines. By
allowing time to flow the timed automaton may therefore distinguish points below the diagonal of
each square, points above the diagonal and points on the diagonal. For example, points above the
diagonal of the square
{x ∈ R2
| x1 ∈ (0, 1) ∧ x2 ∈ (0, 1)}
will leave the square through the line
{x ∈ R2
| x1 ∈ (0, 1) ∧ x2 = 1}
points below the diagonal will leave the square through the line
{x ∈ R2
| x1 = 1 ∧ x2 ∈ (0, 1)}
while points on the diagonal will leave the square through the point
{x ∈ R2
| x1 = 1 ∧ x2 = 1}
This leads us to split each open square in three: two open triangles and an open diagonal line
segment.
It can in fact be shown that this is enough to generate a bisimulation.
Theorem 6.3 The region graph is a finite bisimulation of the timed automaton.
It should be stressed that the region graph is not necessarily the coarsest bisimulation. One may be
able to find bisimulations with fewer sets; the elements of these bisimulation will be unions of sets of
the region graph. It is generally considered bad form to try to construct the entire region graph to
investigate properties of a timed automaton. Usually, one either uses the bisimulation algorithm to
construct a coarse bisimulation, or uses the reachability algorithm directly to investigate reachability.
The point of Theorem 6.3 is that it guarantees that there is at least one finite bisimulation for each
timed automaton, which in turn guarantees that the Bisimulation and Reachability algorithms can
be implemented and will terminate.
A counting exercise reveals that the total number of regions in the region graph is of the order of
n! 2n
n
i=1
(2Ci + 2)
(! denotes factorial.) Even for relatively small n this is a very large number! (! denotes exclamation
point) What is worse, the number grows very quickly (exponentially) as n increases. (In addition
to n! and 2n
, there is another hidden exponential in this formula. Because on a computer numbers
are stored in binary, Ci is exponential in the number of bits used to store it).
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 52
This is bad news. It implies that a relatively simple timed automaton can give rise to a region
graph with a very large number of sets, which will be a nightmare to analyse. It turns out that
this is a general property of timed automata and has nothing to do with the way the region graph
was constructed. Because timed automata have finite bisimulations, we know that they can be
automatically analysed by a computer. However, in the worst case, the number of operations that
the computer will have to perform to analyse the system will be exponential in the size of the
problem (e.g. the length of the input file we need to define our timed automaton for the computer).
This is irrespective of how well we write the programme. In computational complexity terminology,
model checking for timed automata turns out to be PSPACE Complete.
A second bit of bad news about the model checking method is that it does not work for more
complicated systems. For example, one can show that simple variants of timed automata do not
have finite bisimulations. This is the case for example if we allow ˙xi = ci for some constant ci = 1
(skewed clocks, leading to multi-rate automata), or allow comparisons between clocks (terms of the
form xi ≤ xj), or reseting one clock to another (xi := xj). In computer theory terminology, the
reachability question for such systems is undecidable, i.e. there does not exist an algorithm that will
answer the question in finite time.
6.4 Bibliography and Further Reading
Timed automata were the first class of hybrid systems that were shown to be amenable to model
checking methods [2]. Since then a number of other classes of hybrid systems with this property have
been established: classes of multi-rate automata [1], classes of systems with continuous dynamics
governed by constant differential inclusions [41] and classes of systems with continuous dynamics
governed by linear differential equations [55]. It has also been shown that a very wide class of hybrid
systems can be approximated arbitrarily closely by such “decidable” hybrid systems [86] (albeit at
the cost of exponential computational complexity). For an excellent overview of the developments
in this area see [5].
In the case of hybrid control systems, related methods have been developed for automatically synthesising
controllers to satisfy specifications (e.g. given in temporal logic) whenever possible [69, 104, 11].
Based on the theoretical results, computational tools been developed to automatically perform verification
or synthesis tasks [42, 6, 29, 16].
Chapter 7
Reachability with Inputs: A
Viability Theory Perspective
7.1 Reachability with Inputs
In addition to discrete and continuous state variables, many hybrid systems also contain input
variables U, possibly divided into discrete (UD) and continuous (UC). Depending on the application,
inputs may influence
1. Continuous evolution, through the vector field
f(·, ·, ·) : Q × X × U → Rn
.
2. When discrete transitions take place, through the domain
Dom(·) : Q → 2X×U
.
3. The destination of discrete transitions, through the reset map
R(·, ·, ·) : E × X × U → 2X
.
One can pause a number of interesting problems for hybrid systems with inputs, that make no
sense for autonomous hybrid systems. For example, one can study stabilisation, optimal control,
reachability specifications, etc. As before we will restrict our attention to reachability specifications.
Depending on what the inputs are supposed to represent, reachability questions for hybrid systems
with inputs can take a number of forms:
1. Viability. Roughly speaking, this involves answering the question “Does there exist a choice
for the inputs u such that the executions of the hybrid system remain in a given set?”. In this
case one can think of the inputs as controls, that can be used to steer the executions of the
system.
2. Invariance. This involves answering the question “Do the executions of the system remain
in a given set for all choices of u?”. In this case one can think of the inputs as uncontrollable
disturbances that can steer the system outside the desired set.
3. Gaming. In this case some of the input variables play the role of controls, while others play
the role of disturbances. The relevant question in this case is “Does there exist a choice for the
controls, such that despite the action of the disturbances the execution of the system remain
is a given set?”
53
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 54
Working with hybrid systems with inputs is considerably more complicated. Even defining the precise
semantics of an execution of the system is far from straight forward. Additional complications arise
when one considers gaming problems, since one has to introduce assumptions about information
exchange among the players, appropriate notions of strategy, etc. Here we will restrict our attention
to a special case of the general problem for which precise mathematical answers can be formulated
for these questions. In particular, we will study questions of viability and invariance for a class of
hybrid systems known as impulse differential inclusions. The proofs are rather technical and are
included in the notes only for the sake of completeness. For more details please refer to [14].
7.2 Impulse Differential Inclusions
Definition 7.1 (Impulse Differential Inclusion) An impulse differential inclusion is a collection
H = (X, F, R, J), consisting of a finite dimensional vector space X, a set valued map F : X →
2X
, regarded as a differential inclusion ˙x ∈ F(x), a set valued map R : X → 2X
, regarded as a reset
map, and a set J ⊆ X, regarded as a forced transition set.
We call x ∈ X the state of the impulse differential inclusion. Subsequently, I = X \ J will be used
to denote the complement of J. Comparing Definition 7.1 with Definition 3.1, we see that the set I
plays a similar role for the impulse differential inclusion that Dom played for hybrid automata. The
differential inclusion, F(·), plays a similar role to the vector field, f(·, ·). Finally, the domain of the
reset map R plays the same role as the guards G of a hybrid automaton, and the image of the reset
map R plays the same role as the reset relation (also denoted by R) of the hybrid automaton. Note
that the initial states are not explicitly mentioned, and that there are no discrete states. Discrete
states, q, can be introduced into the model, by embedding them in R (e.q., q = 1, 2, 3, . . .) and
introducing a trivial differential inclusion ˙q ∈ {0} to capture their continuous evolution. This is
somewhat cumbersome to do, so we will state the results without this additional complication.
Impulse differential inclusions are extensions of differential inclusions and discrete time systems over
finite dimensional vector spaces. A differential inclusion,
˙x ∈ F(x),
over a finite dimensional vector space X can be thought of as an impulse differential inclusion,
(X, F, R, J), with R(x) = ∅ for all x ∈ X and J = ∅. Likewise, a discrete time system,
xk+1 ∈ R(xk),
can be thought of as an impulse differential inclusion, H = (X, F, R, J), with F(x) = {0} for all
x ∈ X and J = X. In the control literature, differential inclusions and discrete time systems are
frequently used to model continuous and discrete control systems. The continuous control system
˙x = f(x, u), u ∈ U(x)
with x ∈ Rn
, u ∈ Rm
, f : Rn
× Rm
→ Rn
and U : Rn
→ 2Rm
can be though of as a differential
inclusion
˙x ∈ F(x) = {f(x, u) | u ∈ U(x)}.
Likewise, the discrete time control system
xk+1 = r(xk, uk), uk ∈ U(xk)
with xk ∈ Rn
, uk ∈ Rm
, r : Rn
× Rm
→ Rn
and U : Rn
→ 2Rm
can be though of as
xk+1 ∈ R(xk) = {r(xk, u) | u ∈ U(xk)}.
Therefore, impulse differential inclusions can be thought of as hybrid control systems, with controls
both on the continuous evolutions and on the discrete transitions.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 55
Impulse differential inclusions can be used to describe hybrid phenomena. As for the executions of
a hybrid automaton, the state of an impulse differential inclusion evolves over hybrid time sets.
Definition 7.2 (Run of an Impulse Differential Inclusion) a run of an impulse differential
inclusion, H = (X, F, R, J), is a hybrid trajectory, (τ, x), consisting of a hybrid time set τ = {Ii}N
i=0
and a sequence of maps x = {xi}N
i=0, xi(·) : Ii → X, that satisfies:
• Discrete Evolution: for all i, xi+1(τi+1) ∈ R(xi(τi ))
• Continuous Evolution: if τi < τi , xi(·) is a solution to the differential inclusion ˙x ∈ F(x) over
the interval [τi, τi ] starting at xi(τi), with xi(t) ∈ J for all t ∈ [τi, τi [.
Recall that a solution to the differential inclusion ˙x ∈ F(x) over an interval [0, T ] starting at x0 ∈ X
is an absolutely continuous function x : [0, T ] → X, such that x(0) = x0 and almost everywhere
˙x(t) ∈ F(x(t)). As for hybrid automata, runs of impulse differential inclusions can be classified into
finite, infinite, Zeno, etc. (cf. Definition 3.5).
Definition 7.2 dictates that, along a run the state can evolve continuously according to the differential
inclusion ˙x ∈ F(x) until the set J is reached. Moreover, whenever R(x) = ∅, a discrete transition
from state x to some state in R(x) may take place. In other words R enables discrete transitions
(transitions may happen when R(x) = ∅ but do not have to), while J forces discrete transitions
(transitions must happen when x ∈ J).
Notice that if at a state x ∈ X a transition must happen (x ∈ J) but is not able to (R(x) = ∅)
the system blocks, in the sense that there does not exist a run of the impulse differential inclusion
starting at x (other than the trivial run ([0, 0], x)). This is similar to the blocking situations (lack
of runs) that we encountered for hybrid automata. To prevent such behaviour we introduce the
following assumption.
Assumption 7.1 An impulse differential inclusion (X, F, R, J) is said to satisfy Assumption 7.1 if
J ⊆ R−1
(X) and, if J is open (hence I = X \J is closed), F(x)∩TI (x) = ∅, for all x ∈ I \R−1
(X).
As an example, consider again the bouncing ball system. The vertical motion of the ball can be
captured by an impulse differential inclusion, HB = (XB, FB, RB, JB) with two state variables, the
height of the ball, x1 and its velocity in the vertical direction, x2. Therefore, XB = R2
and
FB(x1, x2) =(x2, −g)
RB(x1, x2) =
(x1, −cx2) if x1 ≤ 0 and x2 ≤ 0
∅ otherwise
JB ={x ∈ XB | x1 ≤ 0 and x2 ≤ 0},
where g represents the acceleration due to gravity and c2
∈ [0, 1] the fraction of energy lost with
each bounce.
7.3 Viability and Invariance Definitions
For impulse differential inclusions, reachability questions can be characterised by viability con-
straints.
Definition 7.3 (Viable Run) a run, (τ, x) of an impulse differential inclusion, H = (X, F, R, J),
is called viable in a set K ⊆ X if x(t) ∈ K for all Ii ∈ τ and all t ∈ Ii.
Notice that the definition of a viable run requires the state to remain in the set K throughout, along
continuous evolution up until and including the state before discrete transitions, as well as after
discrete transitions. Based on the notion of a viable run, one can define two different classes of sets.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 56
Definition 7.4 (Viable and Invariant Set) A set K ⊆ X is called viable under an impulse differential
inclusion, H = (X, F, R, J), if for all x0 ∈ K there exists an infinite run starting at x0 that
is viable in K. K is called invariant under the impulse differential inclusion, if for all x0 ∈ K all
runs starting at x0 are viable in K.
In the cases where an impulse differential inclusion fails to satisfy a given viability or invariance
requirement, one would like to establish sets of initial conditions (if any) for which the requirement
will be satisfied. This notion can be characterised in terms of viability and invariance kernels.
Definition 7.5 (Viability and Invariance Kernel) The viability kernel, ViabH(K) of a set K ⊆
X under an impulse differential inclusion H = (X, F, R, J) is the set of states x0 ∈ X for which there
exists an infinite run viable in K. The invariance kernel, InvH(K) of K ⊆ X under H = (X, F, R, J)
is the set of states x0 ∈ X for which all runs are viable in K.
Notice that by definition ViabH(K) ⊆ K and InvH(K) ⊆ K, but in general the two sets are
incomparable.
To state viability and invariance results for impulse differential inclusions we need to introduce some
technical definitions from set valued analysis. For more details see [12, 13].
For a set valued map R : X → 2Y
and a set K ⊆ Y we use R−1
(K) to denote the inverse image of
K under R and R 1
(K) to denote the extended core of K under R, defined by
R−1
(K) = {x ∈ X | R(x) ∩ K = ∅}, and
R 1
(K) = {x ∈ X | R(x) ⊆ K} ∪ {x ∈ X | R(x) = ∅}.
Notice that R−1
(Y ) is the set of x ∈ X such that R(x) = ∅. We call the set R−1
(Y ) the domain of
R and the set {(x, y) ∈ X × Y | y ∈ R(x)} the graph of R.
A set valued map R : X → 2X
is called upper semicontinuous at x ∈ X if for every > 0 there
exists δ > 0 such that
∀ x ∈ B(x, δ), R(x ) ⊆ B(R(x), ).
R is called lower semicontinuous at x ∈ X if for all x ∈ R(x) and for all sequences xn converging
to x, there exists a sequence xn ∈ R(xn) converging to x . R is called upper semicontinuous
(respectively lower semicontinuous) if it is upper semicontinuous (respectively lower semicontinuous)
at all x ∈ X. It should be noted that, unlike single valued functions, these two notions of continuity
are not equivalent for set valued maps. It can be shown that if R is upper semicontinuous with closed
domain and K ⊆ X is a closed set, then R−1
(K) is closed, whereas if R is lower semicontinuous and
U ⊆ X is an open set, then R−1
(U) is open. Notice that the last statement also implies that if R is
lower semicontinuous and K ⊆ X is closed, R 1
(K) is closed, since R 1
(K) = X \ R−1
(X \ K).
For a closed subset, K ⊆ X, of a finite dimensional vector space, and a point x ∈ K, we use TK(x)
to denote the contingent cone to K at x, i.e. the set of v ∈ X such that there exists a sequence of
real numbers hn > 0 converging to 0 and a sequence of vn ∈ X converging to v satisfying
∀ n ≥ 0, x + hnvn ∈ K.
Notice that, if x is in the interior of K, TK(x) = X.
Subsequently we will be dealing with differential inclusions of the form ˙x ∈ F(x), where F : X → 2X
.
To ensure existence of solutions we will need to impose some standard regularity assumptions on the
map F, for example require F to be Marchaud and/or Lipschitz. We say that a map F : X → 2X
is Marchaud if and only if
1. the graph and the domain of F are nonempty and closed;
2. for all x ∈ X, F(x) is convex, compact and nonempty; and,
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 57
3. the growth of F is linear, that is there exists c > 0 such that for all x ∈ X
sup{ v | v ∈ F(x)} ≤ c( x + 1).
We say F is Lipschitz if and only if there exists a constant λ > 0 (known as the Lipschitz constant)
such that for all x, x ∈ X
F(x) ⊆ F(x ) + λ x − x B(0, 1).
7.4 Viability Conditions
The viability conditions for impulse differential inclusions involve the notion of “viability with target”.
Viability with target provides conditions under which solutions of ˙x ∈ F(x) that remain in a
set K until they reach a target set C exist.
Lemma 7.1 Consider a Marchaud map F : X → 2X
and two closed sets K ⊆ X and C ⊆ X. For
all x0 ∈ K, there exists a solution of ˙x ∈ F(x) starting at x0 which is either
1. defined over [0, ∞[ with x(t) ∈ K for all t ≥ 0, or
2. defined over [0, T ] for some T ≥ 0, with x(T ) ∈ C and x(t) ∈ K for all t ∈ [0, T ],
if and only if for all x ∈ K \ C, F(x) ∩ TK(x) = ∅.
Proof:
Necessity: Consider x0 ∈ K\C and x(·) a trajectory starting from x0 which stays in K on some
interval [0, σ] (and which does not reach C in this time interval). By application of Proposition 3.4.1
of [12], we obtain
F(x0) ∩ TK(x0) = ∅.
Sufficiency: Let x0 ∈ K\C. Because C is closed, some r > 0 exists such that B(x0, r) ∩ C = ∅. In
the set BK(x0, r) := K ∩ B(x0, r), one can imitate the proof of Proposition 3.4.2 of [12] and obtain
the existence of T > 0 and of a solution to ˙x ∈ F(x) starting at x0 which remains in BK(x0, r) on
[0, T ].
Using an argument (Zorn’s Lemma) classical in differential equation theory, it is possible to extend
x(·) to a maximal trajectory - again denoted x(·) - on some [0, ˜T] viable in K and such that C ∩
[0, ˆT) = ∅. Either ˆT = +∞ and the proof is complete, or ˆT < +∞ and then x( ˆT) ∈ C (if not one
could extend a little the trajectory to a viable one, this would be a contradiction with the maximality
of x(·)).
The conditions characterising viable sets depend on whether the set J is open or closed. In the case
where J is closed we have the following.
Theorem 7.1 (Viability Conditions, J Closed) Consider an impulse differential inclusion H =
(X, F, R, J) such that F is Marchaud, R is upper semicontinuous with closed domain and J is closed.
A closed set K ⊆ X is viable under H if and only if
1. K ∩ J ⊆ R−1
(K), and
2. ∀ x ∈ K\R−1
(K), F(x) ∩ TK(x) = ∅
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 58
In words, the conditions of the theorem require that for any state x ∈ K, whenever a discrete
transition has to take place (x ∈ K ∩ J), a transition back into K is possible (R(x) ∩ K = ∅), and
whenever a discrete transition to another point in K is not possible (R(x) ∩ K = ∅) continuous
evolution that remains in K has to be possible (encoded by the local viability condition F(x) ∩
TK(x) = ∅). Proof: Notice that, since R is upper semicontinuous with closed domain and K is
closed, R−1
(K) is also closed.
Necessity: Assume that K is viable under (X, F, R, J) and consider an arbitrary x0 ∈ K. To show
the first condition is necessary assume x0 ∈ K ∩ J. Then continuous evolution is impossible at x0.
Assume, for the sake of contradiction, that x0 ∈ R−1
(K). Then either R(x) = ∅ (in which case the
system blocks and no infinite runs start at x0) or all runs starting at x0 leave K through a discrete
transition to some x1 ∈ R(x0). In either case, the assumption that K is viable is contradicted. To
show the second condition is necessary, assume x0 ∈ K \ R−1
(K). Since an infinite run viable in
K starts at x0, there exists a solution to the differential inclusion ˙x ∈ F(x) starting at x0 which is
either
1. defined on [0, ∞[ with x(t) ∈ K \ J for all t ≥ 0; or,
2. defined on [0, t ] with x(t ) ∈ R−1
(K) and x(t) ∈ K \ J for all t ∈ [0, t [.
This implies, in particular, that there is a solution to the differential inclusion ˙x ∈ F(x) starting at
x0 which is either
1. defined on [0, ∞[ with x(t) ∈ K for all t ≥ 0; or,
2. defined on [0, t ] with x(t ) ∈ R−1
(K) and x(t) ∈ K for all t ∈ [0, t ].
By the necessary part of Lemma 7.1, this implies that for all x0 ∈ K \ R−1
(K), F(x) ∩ TK(x) = ∅.
Sufficiency: Assume the conditions of the theorem are satisfied and consider an arbitrary x0 ∈ K. We
construct an infinite run of (X, F, R, J) starting at x0 and viable in K by induction. We distinguish
two cases, x0 ∈ K \ R−1
(K) and x0 ∈ K ∩ R−1
(K). In the first case, by the sufficient part of
Lemma 7.1, there exists a solution to the differential inclusion ˙x ∈ F(x) starting at x0 which is
either
1. defined on [0, ∞[ with x(t) ∈ K for all t ≥ 0; or,
2. defined on [0, t ] with x(t ) ∈ R−1
(K) and x(t) ∈ K for all t ∈ [0, t ].
Notice that, since by the first assumption of the theorem, K ∩ J ⊆ R−1
(K) there must also be a
solution to the differential inclusion ˙x ∈ F(x) starting at x0 which is either
1. defined on [0, ∞[ with x(t) ∈ K \ J for all t ≥ 0; or,
2. defined on [0, t ] with x(t ) ∈ R−1
(K) and x(t) ∈ K \ J for all t ∈ [0, t [
(i.e. either the solution stays in K forever and never reaches J, or the solution stays in K and
reaches R−1
(K) by the time it reaches J). In the former case, consider the infinite run ([0, ∞[, x);
this is clearly a run of (X, F, R, J), viable in K. In the latter case, let τ0 = 0, τ0 = t , and τ1 = τ0.
Since x(τ0) ∈ R−1
(K), x(τ1) can be chosen such that x(τ1) ∈ K. Notice that this argument also
covers the case where x0 ∈ K ∩ R−1
(K), with x(τ0) playing the role of x0. An infinite run viable in
K can now be constructed inductively, by substituting x0 by x(τ1) and repeating the process.
Similar conditions characterise viability when the set J is open, or, in other words, the set I = X \J
is closed.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 59
R−1(K)
F (x)
F (x)
F (x)
F (x)
TK(x)
TK(x)
TK(x)
TK(x)
X
J
K
Figure 7.1: K viable under H = (X, F, R, J)
Theorem 7.2 (Viability Conditions, J Open) Consider an impulse differential inclusion H =
(X, F, R, J) such that F is Marchaud, R is upper semicontinuous with closed domain and J is open.
A closed set K ⊆ X is viable under H if and only if
1. K ∩ J ⊆ R−1
(K), and
2. ∀ x ∈ (K ∩ I)\R−1
(K), F(x) ∩ TK∩I(x) = ∅
Figure 7.1 suggests how the conditions of Theorems 7.1 and 7.2 can be interpreted pictorially.
Notice that Assumption 7.1 does not need to be added explicitly to Theorems 7.1 and 7.2, since the
part of it that is essential to guarantee the existence of a run viable in K is implied by the conditions
of the theorems. Conditions that guarantee the existence of runs for impulse differential inclusions
can be deduced as a corollary of Theorems 7.1 and 7.2.
Corollary 7.1 Consider an impulse differential inclusion H = (X, F, R, J) such that F is Marchaud,
and R is upper semicontinuous with closed domain and J is either open or closed. Every
finite run of H can be extended to an infinite run if and only if H satisfies Assumption 7.1.
7.5 Invariance Conditions
The conditions for invariance make use of the notion of “invariance with target” for continuous
differential inclusions. Invariance with target involves conditions ensuring that all solutions of ˙x ∈
F(x) remain in a set K until they reach a target set, C.
Lemma 7.2 Consider a Marchaud and Lipschitz map F : X → 2X
and two closed sets K and C.
All solutions of ˙x ∈ F(x) starting at some x0 ∈ K are either
1. defined over [0, ∞[ with x(t) ∈ K for all t ≥ 0, or
2. defined over [0, T ] with x(T ) ∈ C and x(t) ∈ K for all t ∈ [0, T ],
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 60
if and only if for all x ∈ K \ C, F(x) ⊆ TK(x).
Proof:
Necessity: Assume that all solutions starting in K stay in K until they reach C. Consider x0 ∈ K \C
and v0 ∈ F(x0). Then (see for example [12] Corollary 5.3.2) there exists a trajectory x(·) of ˙x ∈ F(x)
starting at x0 such that d
dt x(0) = v0. Since x is a solution to ˙x ∈ F(x) it remains in K until it reaches
C. But x0 ∈ K \C and C is closed, therefore, there exists α > 0 such that x(t) ∈ K for all t ∈ [0, α].
Since x is absolutely continuous, for all t ∈ [0, α[ where d
dt x(t) is defined, d
dt x(t) ∈ TK(x(t)) (see for
example [12]). In particular, for t = 0, v0 = d
dt x(0) ∈ TK(x0). Hence, for all x0 ∈ K \ C and for all
v0 ∈ F(x0), v0 ∈ TK(x0), or, in other words, F(x0) ⊆ TK(x0).
Sufficiency: Let λ be the Lipschitz constant of F. Consider x0 ∈ K and a solution x(·) of ˙x ∈ F(x)
starting at x0, and show that x remains in K until it reaches C. If x0 ∈ C then there is nothing to
prove. If x0 ∈ K \ C consider
θ = sup{t | ∀ t ∈ [0, t[, x(t ) ∈ K \ C}.
If θ = ∞ or x(θ) ∈ C we are done. We show that x(θ) ∈ K \ C leads to a contradiction. Indeed,
consider α > 0 such that B(x(θ), α) ∩ C = ∅ (which exists since x(θ) ∈ C and C is closed), and
θ > θ, such that for all t ∈ [θ, θ ], x(t) ∈ B(x(θ), α) (which exists since x is continuous). For
t ∈ [θ, θ ], let ΠK(x(t)) denote a point of B(x(θ), α) ∩ K such that
d(x(t), K) = d(x(t), ΠK (x(t)))
(a projection of x(t) onto K). Then (see for example [12], Lemma 5.1.2) for almost every t ∈ [θ, θ ],
d
dt
d(x(t), K) ≤d
d
dt
x(t), TK (ΠK(x(t)))
≤d
d
dt
x(t), F(ΠK (x(t)))
≤d
d
dt
x(t), F(x(t)) + λd(x(t), ΠK (x(t)))
≤0 + d(x(t), K)
since x is a solution to ˙x ∈ F(x) and by definition of Π. By the Gronwall lemma, d(x(t), K) = 0 for
all t ∈ [θ, θ ], which contradicts the definition of θ. Summarising, if F(x) ⊆ TK(x) for all x ∈ K \ C,
then all solutions starting in K either stay for ever in K \ C or reach C before they leave K.
Lemma 7.2 allows us to prove the following invariance theorem for impulse differential inclusions.
Theorem 7.3 (Invariance Conditions) Consider an impulse differential inclusion H = (X, F, R, J)
such that F is Marchaud and Lipschitz and J is closed. A closed set K ⊆ X is invariant under H
if and only if
1. R(K) ⊆ K, and
2. ∀ x ∈ K \ J, F(x) ⊆ TK(x).
In words, the conditions of the theorem require that for all x ∈ K, if a discrete transition is possible
(x ∈ R−1
(X)), then all states after the transition are also in K (R(x) ⊆ K), whereas if continuous
evolution is possible (x ∈ J) then all possible solutions of the differential inclusion ˙x ∈ F(x) remain
in K (characterised here by the invariance condition F(x) ⊆ TK(x)). Figure 7.2 suggests how the
conditions of Theorem 7.3 can be interpreted pictorially.
Proof:
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 61
R−1(X)
R (K) ∩ R−1(X)
F (x)
F (x)
F (x)
F (x)
X
J
K
Figure 7.2: K invariant under (X, F, R, J)
Necessity: Assume that K is invariant under (X, F, R, J). If the first condition is violated, then
there exists x0 ∈ K and x1 ∈ R(x0) with x1 ∈ K. Therefore, there exists a run starting at x0
that leaves K through a discrete transition to some x1 and the assumption that K is invariant is
contradicted. To show the second condition is necessary, notice that since all runs of (X, F, R, J)
starting in K are viable in K, then all solutions to ˙x ∈ F(x) starting in K are either
1. defined on [0, ∞[ with x(t) ∈ K \ J for all t ≥ 0; or,
2. defined on [0, t ] with x(t ) ∈ J and x(t) ∈ K for all t ∈ [0, t ].
Otherwise, there would exist a solution of ˙x ∈ F(x) which leaves K before reaching J. This solution
would be a run of (X, F, R, J) that is not viable in K, which would contradict the assumption
that K is invariant. By the necessary part of Lemma 7.2, 1 and 2 imply that for all x0 ∈ K \ J,
F(x) ⊆ TK(x).
Sufficiency: Assume the conditions of the theorem are satisfied and consider an arbitrary x0 ∈ K and
an arbitrary run, (τ, x), of (X, F, R, J) starting at x0. Notice that x(τ0) = x0 ∈ K by assumption.
Assume x(τi) ∈ K and show x(t) ∈ K until τi+1; the claim then follows by induction. If t = τi we
are done. If τi t τi, then x(τi) ∈ K \ J since continuous evolution is possible from x(τi). By the
second condition of the theorem and the sufficient part of Lemma 7.2, all solutions to the differential
inclusion ˙x ∈ F(x) starting at x(τi) are either
1. defined on [0, ∞[ with x(t) ∈ K for all t ≥ 0; or,
2. defined on [0, t ] with x(t ) ∈ J and x(t) ∈ K for all t ∈ [0, t ].
In the first case, the run is viable in K and we are done. In the second case, τi t and therefore
for all t ∈ [τi, τi ], x(t) ∈ K. If x(τi ) ∈ R−1
(K), x(τi+1) ∈ R(x(τi)) ⊆ K by the first condition of the
theorem. If, on the other hand, x(τi ) ∈ J, but R(x(τi )) = ∅, then the execution blocks at τi, and
therefore is viable in K.
Notice that no assumptions need to be imposed on R. Strictly speaking, Theorem 7.3 remains true
even without Assumption 7.1; if the impulse differential inclusion has no runs for certain initial
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 62
conditions in K, then, vacuously, all runs that start at these initial conditions are viable in K. In
practice, it may be prudent to impose Assumption 7.1, to ensure the results are meaningful.
7.6 Viability Kernels
If K is not viable under an impulse differential inclusion H, one would like to characterise the
largest subset of K which is viable under H. This set turns out to be the viability kernel of K under
the impulse differential inclusion. The viability kernel of an impulse differential inclusion can be
characterised in terms of the notion of the viability kernel with target for a continuous differential
inclusion. For a differential inclusion ˙x ∈ F(x), the viability kernel of a set K with target C,
ViabF (K, C), is defined as the set of states for which there exists a solution to the differential
inclusion that remains in K either forever, or until it reaches C.
Lemma 7.3 Consider a Marchaud map F : X → 2X
and two closed subsets of X, K and C.
ViabF (K, C) is the largest closed subset of K satisfying the conditions of Lemma 7.1.
Proof: Let D ⊆ K a closed set satisfying assumptions of Lemma 7.1. Clearly D ⊆ ViabF (K, C).
We claim that ViabF (K, C) is closed. Consider a sequence xn ∈ ViabF (K, C) converging to some
x ∈ X. Since K is closed, x ∈ K. We show that x ∈ ViabF (K, C). If x ∈ C, the proof is done.
Else, there exists an r > 0 with K ∩ B(x, r) = ∅. For n large enough xn ∈ B(x, r
2 ). For any such n,
consider xn(·) a solution to the differential inclusion starting from xn, viable in K until it reaches
C. Such a solution exists, since xn ∈ ViabF (K, C).
The graph of the solution map of the differential inclusion restricted to the compact set
{x} ∪ {xn, n > 0}.
is compact (Theorem 3.5.2 in [12]). Hence, there exists a subsequence to xn(·) - again denoted
xn(·) - converging to a solution x(·) of the differential inclusion starting at x uniformly on compact
intervals.
Let σ > 0 such that x[0, σ) ∩ C = ∅. Such a σ exists since x ∈ C, C is closed, and x(·) is continuous.
Fix 0 ≤ t < σ. For n large enough, xn[0, t]∩C = ∅ because C is closed and xn(·) converges uniformly
to x(·) on [0, t]. Since xn[0, t] is contained in K so is x[0, t]. Because σ and t are arbitrary, we can
deduce that x(·) is viable in K until it reaches C. So x ∈ ViabF (K, C), and therefore ViabF (K, C)
is closed.
It remains to prove that ViabF (K, C) satisfies conditions of Lemma 7.1 (i.e., that it is itself viable
with target C). Let x0 ∈ ViabF (K, C). By the very definition of the viability kernel some trajectory
x(·) starting from x exists which is viable in K until it reaches C. Suppose by contradiction that
some s > 0 exists such x(s) /∈ ViabF (K, C) and x[0, s] ∩ C = ∅. Then any trajectory starting from
x(s) leaves K before reaching C. But t → x(s + t) is such a trajectory which is viable in K until it
reaches C, a contradiction.
Exercise 7.1 Show that K ∩ C ⊆ ViabF (K, C) ⊆ K.
Using this notion, one can give an alternative characterisation of the sets that are viable under an
impulse differential inclusion, as fixed points of an appropriate operator. For an impulse differential
inclusion H = (X, F, R, J), consider the operator Pre∃
H : 2X
→ 2X
defined by
Pre∃
H(K) = ViabF (K ∩ I, R−1
(K)) ∪ (K ∩ R−1
(K))
Recall that I = X \ J.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 63
x0
R−1(X) R−1(K)
Case 1
Case 2
Case 3
K
X
I
Figure 7.3: Three possible evolutions for x0 ∈ ViabF (K ∩ I, R−1
(K)) ∪ (K ∩ R−1
(K)).
Lemma 7.4 Consider an impulse differential inclusion H = (X, F, R, J) such that F is Marchaud,
R is upper semicontinuous with closed domain, and J is open. A closed set K ⊆ X is viable under
H if and only if it is a fixed point of the operator Pre∃
H.
Proof:
Necessity: We first show that for every closed set K viable under H = (X, F, R, J), Pre∃
H(K) = K.
Pre∃
H(K) is clearly a subset of K, since ViabF (K ∩ I, R−1
(K)) ⊆ K ∩ I ⊆ K. Conversely, consider
an arbitrary x0 ∈ K. Assume, for the sake of contradiction, that x0 ∈ ViabF (K ∩ I, R−1
(K)) ∪
(K ∩ R−1
(K)). Consider an arbitrary infinite run (τ, x) viable in K and starting at x0. Then
x(τ0) ∈ R−1
(K) and x(τ0) ∈ ViabF (K ∩ I, R−1
(K)). If τ0 = τ0, x starts by a discrete transition
to some x(τ1) ∈ R(x(τ0)). Since x(τ0) ∈ R−1
(K), x(τ1) ∈ K, which contradicts the assumption
that (τ, x) is viable in K. If τ0 < τ0, then (τ, x) starts by continuous evolution. Since x0 = x(τ0) ∈
ViabF (K ∩ I, R−1
(K)), the run either
1. leaves K (at time t τ0) before it reaches R−1
(K), or
2. leaves I (at time τ0) before it reaches R−1
(K), or
3. takes a transition from some x(τ0) ∈ K ∩ I \ R−1
(K)
(see Figure 7.3). The first case contradicts the assumption that (τ, x) is viable in K. In the remaining
cases, x(τ0) ∈ R−1
(K) and since x(τ1) ∈ R(x(τ0)), we have x(τ1) ∈ K. This also contradicts the
assumption that (τ, x) is viable in K.
Sufficiency: Next, we show that every closed set K such that K = Pre∃
H(K) is viable. Consider an
arbitrary x0 ∈ K; we construct by induction an infinite run, (τ, x) that starts at x0 and is viable in
K. By assumption x0 = x(τ0) ∈ K. Assume that we have constructed a run viable in K defined
over a finite sequence [τ0, τ0], [τ1, τ1], . . . , [τi, τi]. Since K is a fixed point of Pre∃
H and the run is
viable in K, x(τi) ∈ ViabF (K ∩ I, R−1
(K)) ∪ (K ∩ R−1
(K)). If x(τi) ∈ K ∩ R−1
(K), let τi = τi and
chose x(τi+1) ∈ R(x(τi )) ∩ K. If x(τi) ∈ ViabF (K ∩ I, R−1
(K)), then there exists a solution to the
differential inclusion ˙x ∈ F(x) which is either:
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 64
1. defined over [0, ∞[ with x(t) ∈ K ∩ I for all t ≥ 0; or,
2. defined over [0, t ] with x(t ) ∈ R−1
(K) and x(t) ∈ K ∩ I for all t ∈ [0, t ].
In the former case, set τi = ∞ and the construction of the infinite run is complete. In the latter
case, let τi = τi + t and choose x(τi+1) ∈ R(x(τi )) ∩ K. The claim follows by induction.
Theorem 7.4 (Viability Kernel) Consider an impulse differential inclusion H = (X, F, R, J)
such that F is Marchaud, R is upper semicontinuous with closed domain and compact images, and
J is open. The viability kernel of a closed set K ⊆ X under H is the largest closed subset of K
viable under H, that is, the largest closed fixed point of Pre∃
H contained in K.
Proof: The proof makes use of the sequence of sets {Ki} constructed by the Viability Kernel
Approximation algorithm, that is the sequence K0 = K, Ki+1 = Pre∃
H(Ki). Let
K∞ =
∞
i=0
Ki.
The proof proceeds in a sequence of steps. We show that:
1. For every viable set L ⊆ K, L ⊆ ViabH(K).
2. K∞ is closed.
3. ViabH(K) ⊆ K∞.
4. K∞ ⊆ ViabH(K).
5. ViabH(K) is viable.
Step 1: Every set L ⊆ K which viable under H = (X, F, R, J) must be contained in ViabH(K),
since for all x0 ∈ L there exists an infinite run starting at x0 that stays in L, and therefore in K.
Step 2: Since ViabF (Ki ∩ I, R−1
(Ki)) ⊆ Ki ∩ I ⊆ Ki, Ki+1 ⊆ Ki for all i. Since K is closed,
K0 is closed. Moreover, if Ki is closed, then R−1
(Ki) is closed (since R is upper semicontinuous
with closed domain), and ViabF (Ki ∩ I, R−1
(Ki)) is closed (by Lemma 7.3, since I and R−1
(Ki)
are closed), and, therefore, Ki+1 is closed. By induction, Ki form a sequence of nested closed sets,
and therefore K∞ is closed (possibly the empty set).
Step 3: Consider a point x0 ∈ ViabH(K) and show that x0 ∈ K∞. Assume, for the sake of
contradiction, that x0 ∈ K∞. Then there exists N ≥ 0 such that x0 ∈ KN . If N = 0, then
x0 ∈ K0 = K, therefore all runs starting at x0 that are not viable in K (trivially). This contradicts
the assumption that x0 ∈ ViabH(K). If N > 0, we show that for all infinite runs (τ, x) starting
at x0 (which exist since x0 ∈ ViabH(K)), there exists a t τ1 such that1
x(t) ∈ KN−1. The
claim then follows by induction. Indeed, since x0 ∈ KN we must have have x0 ∈ ViabF (KN−1 ∩
I, R−1
(KN−1))∪(KN−1 ∩R−1
(KN−1)). If τ0 < τ0, then (τ, x) starts by continuous evolution. Since
x0 = x(τ0) ∈ ViabF (KN−1 ∩ I, R−1
(KN−1)), then all solutions to ˙x ∈ F(x) either
1. leave KN−1 (at some t τ0) before they reach R−1
(KN−1), or
2. leave I (at time τ0) before they reach R−1
(KN−1), or
3. take a transition from some x(τ0) ∈ (KN−1 ∩ I) \ R−1
(KN−1).
1If τ = [τ0, ∞), t τ1 is replaced by t τ0 = ∞.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 65
(refer to Figure 7.3). In the first case we are done. In the remaining cases, x(τ0) ∈ R−1
(KN−1) and
since x(τ1) ∈ R(x(τ0)), we have x(τ1) ∈ KN−1. The last argument also subsumes the case τ0 = τ0,
since x0 ∈ KN−1 ∩ R−1
(KN−1).
Step 4: Consider an arbitrary x0 ∈ K∞. To show that x0 ∈ ViabH(K), we construct an infinite run
(τ, x) ∈ R∞
H (x0) viable in K. More specifically, since x0 ∈ Kk for all k, there exists a sequence of
runs (τ(k)
, x(k)
) ∈ RH (x0), which remain in K for at least k jumps. We will show that the sequence
(τ(k)
, x(k)
) has a cluster point (¯τ, ¯x) ∈ R∞
H (x0), which is an infinite run of (X, F, R, J), starting at
x0, viable in K.
Let [τ
(k)
i , τ
(k)
i ] (or [τ
(k)
i , τ
(k)
i [ if i is the last interval) denote the sequence of intervals τ(k)
. Recall
that, without loss of generality, we can assume that τ
(k)
0 = 0 for all k. Let ¯τ0 = 0 and define
¯τ0 = lim inf
k→∞
τ
(k)
0 .
Then there exists a subsequence of τ
(k)
0 , denoted by τ
σ(k)
0 , such that
lim
k→∞
τ
σ(k)
0 = ¯τ0.
We distinguish three cases:
1. ¯τ0 = +∞;
2. ¯τ0 ∈]0, +∞[; and,
3. ¯τ0 = 0.
Case 1 will lead to a run (¯τ, ¯x) ∈ R∞
H (x0) that is viable in K and makes no jumps. Case 2 will lead
to a run (¯τ, ¯x) ∈ R∞
H (x0) that is viable in K, whose first jump comes after an interval of continuous
evolution. Finally, Case 3 will lead a run (¯τ, ¯x) ∈ R∞
H (x0) viable in K, that takes its first jump
immediately.
Case 1: Consider a sequence yσ(k)
(·) of solutions to the differential inclusion
˙x ∈ F(x), x(0) = x0, (7.1)
that coincide with xσ(k)
on [0, τ
σ(k)
0 [. Because the set of solutions of (7.1) is compact (see Theorem
3.5.2 of [12]), there exists a subsequence yφ(k)
(·) of the sequence yσ(k)
(·) that converges to a solution
¯y(·) of (7.1). Moreover, since limk→∞ τ
σ(k)
0 = +∞, the sequence yφ(k)
(·) (and hence the sequence
xφ(k)
(·)) converges to ¯y(·) uniformly over [0, T ], for all T > 0.
Now, (τφ(k)
, xφ(k)
) is a run of (X, F, R, J) viable in K for at least k jumps. Therefore, xφ(k)
(t) ∈ K∩I
for all t ∈ [0, τ
φ(k)
0 [, and hence, for sufficiently large k, xφ(k)
(t) ∈ K ∩ I for all t ∈ [0, T ]. Since
K ∩ I is closed, ¯y(t) ∈ K ∩ I for all t ∈ [0, T ]. Since T is arbitrary, ([0, ∞[, ¯y) is an infinite run of
(X, F, R, J) (with no jumps) starting at x0 and viable in K. The proof is complete.
Case 2: We can restrict attention to k ≥ 1. As for case 1, define the sequence yσ(k)
(·) of solutions of
(7.1) that coincide with xσ(k)
on [0, τ
σ(k)
0 [ and the subsequence yφ(k)
(·) converging (uniformly over
compact intervals) to a solution ¯y(·) of (7.1). As before, (τφ(k)
, xφ(k)
) is a run of (X, F, R, J) viable
in K for at least k > 0 jumps. Therefore, xφ(k)
(t) ∈ K ∩I for all t ∈ [0, τ
φ(k)
0 [. Since K ∩I is closed,
¯y(t) ∈ K ∩ I for all t ∈ [0, ¯τ0]. Therefore, ([¯τ0, ¯τ0], ¯y) is a finite run of (X, F, R, J) (with no jumps)
starting at x0 and viable in K.
Since yφ(k)
(·) converges to ¯y(·) and τ
φ(k)
0 converges to ¯τ0, xφ(k)
(τ
φ(k)
0 ) converges to ¯y(¯τ0). Recall that
(τφ(k)
, xφ(k)
) is a run of (X, F, R, J) viable in K for at least k > 0 jumps, therefore xφ(k)
(τ
φ(k)
1 ) ∈
R(xφ(k)
(τ
φ(k)
0 )) ∩ K. Since R is upper semicontinuous with closed domain and compact images,
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 66
there exists a subsequence of xφ(k)
(τ
φ(k)
1 ) converging to some point ¯y1 ∈ R(¯y(¯τ0)) ∩ K. Therefore,
([0, ¯τ0][¯τ1, ¯τ1], ¯y) with ¯τ1 = ¯τ1 = ¯τ0 and ¯y(¯τ1) = ¯y1 defined as above is a finite run of (X, F, R, J)
(with one jump) starting at x0 and viable in K.
Case 3: The second part of the argument for Case 2 shows that, since xφ(k)
(τ
σ(k)
0 ) converge to x0,
there exists ¯y1 ∈ R(x0) ∩ K. Therefore, ([0, ¯τ0][¯τ1, ¯τ1], ¯y) with ¯τ0 = ¯τ1 = ¯τ1 = 0, ¯y(τ0) = x0 and
¯y(¯τ1) = ¯y1 is a finite run of (X, F, R, J) (with one instantaneous jump) starting at x0 and viable in
K.
To complete the proof for Cases 2 and 3, we repeat the argument starting at ¯y(¯τ1) (discarding the
initial part of the sequences accordingly). We generate ¯τ1 = lim infk→∞ τ
(k)
1 and construct a run
of (X, F, R, J) viable in K, defined either over [0, ¯τ0][¯τ1, ¯τ1[ (if ¯τ1 = +∞, in which case the proof
is complete) or over [0, ¯τ0][¯τ1, ¯τ1][¯τ2, ¯τ2] with ¯τ2 = ¯τ2 = ¯τ1 (if ¯τ1 is finite). The claim follows by
induction.
Step 5: Finally, we show ViabH(K) is viable by showing that it is a fixed point of Pre∃
H. Recall that
Pre∃
H(ViabH(K)) ⊆ ViabH(K). Consider an arbitrary x0 ∈ ViabH(K) and assume, for the sake of
contradiction, that x0 ∈ Pre∃
H(ViabH(K)). Consider an arbitrary infinite run (τ, x) viable in K and
starting at x0 (which exists since x0 ∈ ViabH(K)). If τ0 = τ0, x starts by a discrete transition to
some x(τ1) ∈ R(x0). Since x0 ∈ R−1
(ViabH(K)), x(τ1) ∈ ViabH(K). If τ0 < τ0, then (τ, x) starts
by continuous evolution. Since x0 ∈ ViabF (ViabH(K) ∩ I, R−1
(ViabH(K))), the execution either
1. leaves ViabH(K) (at time t τ0) before it reaches R−1
(ViabH(K)); or,
2. leaves I (at time τ0) before it reaches R−1
(ViabH(K)); or,
3. takes a transition from some x(τ0) ∈ ViabH(K) ∩ I \ R−1
(ViabH(K))
(see Figure 7.3). In all cases, (τ, x) either blocks or leaves ViabH(K) at some t ∈ τ with t τ1.
But if x(t) ∈ ViabH(K) there is no infinite run of H = (X, F, R, J) starting at x(t) and viable
in K. Therefore, (τ, x) either blocks or is not viable in K. This contradicts the assumption that
x0 ∈ ViabH(K).
It should be stressed that the conditions of Theorem 7.4 ensure that for all initial conditions in the
viability kernel infinite runs of the impulse differential inclusion exist, but do not ensure that these
runs will extend over an infinite time horizon; all runs starting at certain initial conditions in the
viability kernel may turn out to be Zeno.
The proof of Theorem 7.4 is based on the following abstract algorithm.
Algorithm 3 (Viability Kernel Approximation)
initialization: K0 = K, i = 0
repeat
Ki+1 = Pre∃
H(Ki)
i = i + 1
until Ki = Ki−1
The algorithm generates a sequence of nested, closed sets Ki that “converge” to the viability kernel.
In addition to being useful in the proof of the theorem, the algorithm can therefore also be used to
provide progressively better estimates of the viability kernel. This is, of course, provided one can
compute Pre∃
(Ki) at each step. Numerical algorithms for approximating this computation have
been developed see, for example, [87].
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 67
7.7 Invariance Kernels
If K is not invariant under an impulse differential inclusion H, one would like to characterise the
largest subset of K which is invariant under H. This turns out to be the invariance kernel of K
under the impulse differential inclusion. The invariance kernel can be characterised using the notion
of the invariance kernel with target for continuous differential inclusions. For a differential inclusion
˙x ∈ F(x), the invariance kernel of a set K with target C, InvF (K, C) is defined as the set of states
for which all solutions to the differential inclusion remain in K either for ever, of until they reach C.
Lemma 7.5 Consider a Marchaud and Lipschitz map F : X → 2X
and two closed subsets of X, K
and C. InvF (K, C) is the largest closed subset of K satisfying the conditions of Lemma 7.2.
Proof: By definition, InvF (K, C) is the set of x0 ∈ K such that for all solutions x(·) of ˙x ∈ F(x)
starting at x0 either
1. x(t) ∈ K for all t ≥ 0, or,
2. there exists t ≥ 0 such that x(t ) ∈ C and x(t) ∈ K for all t ∈ [0, t ].
Therefore, InvF (K, C) satisfies the conditions of Lemma 7.2. Moreover, every subset L ⊆ K which
satisfies the conditions of Lemma 7.2 must be contained in InvF (K, C), since all runs starting in L
stay in L (and therefore in K) until they reach C.
It remains to show that InvF (K, C) is closed. Consider a sequence xn ∈ InvF (K, C) converging to
x0 and show that x0 ∈ InvF (K, C). Since by definition InvF (K, C) ⊆ K and K is assumed to be
closed, x0 ∈ K. If x0 ∈ K ∩ C there is nothing to prove, since by definition K ∩ C ⊆ InvF (K, C).
If x0 ∈ K \ C, let x(·) be any solution of ˙x ∈ F(x) starting at x0. Let
θ = sup{t | ∀ t ∈ [0, t[, x(t ) ∈ K \ C}.
If θ = ∞ or if x(θ) ∈ C, then x0 ∈ InvF (K, C), and the proof is complete.
Let λ be the Lipschitz constant of F, and assume, for the sake of contradiction, that θ < ∞ and
x(θ) ∈ K \ C. Then, by the definition of θ and the assumption that K and C are closed, there exists
θ > θ such that x(θ ) ∈ K and for all t ∈ [θ, θ ], x(t) ∈ C. Choose such that
d(x(θ ), K) > eλθ
(7.2)
(possible since K is closed and x(θ ) ∈ K) and for all t ∈ [0, θ ]
x(t) + B(0, 1)eλt
∩ C = ∅ (7.3)
(possible since C is closed and for all t ∈ [0, θ ], x(t) ∈ C).
Since xn → x0 there exists n large enough such that xn − x0 < . By Filippovs theorem (see for
example [12], Theorem 5.3.1) there exists a solution xn(·) of ˙x ∈ F(x) starting at xn such that for
all t ∈ [0, θ ]
xn(t) − x(t) ≤ xn − x0 eλt
,
or, in other words, for all t ∈ [0, θ ]
xn(t) ∈ B(x(t), xn − x0 eλt
) ⊆ B(x(t), eλt
).
Therefore, by equation (7.3), for all t ∈ [0, θ ], xn(t) ∈ C, while, by equation (7.2) xn(θ ) ∈ K. This
contradicts the assumption that xn ∈ InvF (K, C). Hence, every converging sequence has its limit
in InvF (K, C), and therefore InvF (K, C) is closed.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 68
Exercise 7.2 Show that K ∩ C ⊆ InvF (K, C) ⊆ K.
Using the notion of invariance kernel with target, one can give an alternative characterisation of the
sets that are invariant under an impulse differential inclusion, as fixed points of an operator. Given
an impulse differential inclusion H = (X, F, R, J), consider the operator Pre∀
H : 2X
→ 2X
defined
by
Pre∀
H(K) = InvF (K, J) ∩ R 1
(K)
Lemma 7.6 Consider an impulse differential inclusion H = (X, F, R, J) such that F is Marchaud
and Lipschitz, R is lower semicontinuous, and J is closed. A closed set K ⊆ X is invariant under
H if and only if it is a fixed point of the operator Pre∀
H.
Proof:
Necessity: We first show that for every closed, invariant set K, K = Pre∀
H(K). Clearly Pre∀
H(K) ⊆
K, since InvF (K, J) ⊆ K. Conversely, consider an arbitrary point x0 ∈ K and show that x0 ∈
InvF (K, J) ∩ R 1
(K). Assume, for the sake of contradiction that this is not the case. Then, either
x0 ∈ InvF (K, J), or x0 ∈ R 1
(K). If x0 ∈ R 1
(K), there exists x1 ∈ R(x0) such that x1 ∈ K; in
other words, there exists a run of the impulse differential inclusion starting at x0 that leaves K by
a discrete transition. This contradicts the assumption that K is invariant. If, on the other hand,
x0 ∈ InvF (K, J) then, in particular, x0 ∈ J ∩K (since J ∩K ⊆ InvF (K, J)); but x0 ∈ K, so we must
have x0 ∈ J, and therefore continuous evolution starting at x0 is possible. Since x0 ∈ InvF (K, J),
there exists a solution to ˙x ∈ F(x) starting at x0 that leaves K before reaching J. This solution is a
run (X, F, R, J) that starts in K but is not viable in K. This also contradicts the assumption that
K is invariant.
Sufficiency: Next, we show that every closed set K such that K = Pre∀
H(K) is invariant. Consider
an arbitrary run (τ, x) starting at some x0 ∈ K. We show that (τ, x) is viable in K by induction.
Assume that we have shown that x(t) ∈ K for all t ∈ [τ0, τ0], [τ1, τ1], . . . , [τi, τi]. Then, since K =
Pre∀
H(K), x(τi) ∈ InvF (K, J) ∩ R 1
(K). If τi = τi the system takes a discrete transition to some
x(τi+1) ∈ R(x(τi )) ⊆ K, since x(τi ) = x(τi) ∈ R 1
(K). If τi < τi the run progresses by continuous
evolution. Since x(τi) ∈ InvF (K, J), then either
1. τi = ∞ and x(t) ∈ K for all t ≥ τi; or,
2. τi < ∞, x(τi ) ∈ J and x(t) ∈ K for all t ∈ [τi, τi ].
Notice that x(τi ) ∈ K = Pre∀
H(K), and, in particular, x(τi ) ∈ R 1
(K). Therefore, x(τi+1) ∈
R(x(τi )) ⊆ K. The claim follows by induction.
Notice that in the last argument R(x(τi )) may, in fact, be empty. In this case the run “blocks”, in
the sense that there exist no infinite runs starting at x(τi ). The conclusion that all runs starting at
x0 are viable in K is still true however. To preclude this somewhat unrealistic situation, one can
add Assumption 7.1 to the lemma and subsequent Theorem 7.5.
Theorem 7.5 (Invariance Kernel) Consider an impulse differential inclusion H = (X, F, R, J)
such that F is Marchaud and Lipschitz, R is lower semicontinuous and J is closed. The invariance
kernel of a closed set K ⊆ X under H is the largest closed subset of K invariant under H, that is,
the largest, closed fixed point of Pre∀
H contained in K.
Proof: The proof makes use of the sequence of sets generated by the Invariance Kernel Algorithm
given below, that is, the sets K0 = K, Ki+1 = Pre∀
H(Ki). Let
K∞ =
∞
i=0
Ki.
The proof proceeds in a sequence of steps. We show that
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 69
1. For every invariant set L ⊆ K, L ⊆ InvH(K).
2. K∞ is closed.
3. InvH(K) ⊆ K∞.
4. K∞ = Pre∀
H(K∞).
Step 2, step 4 and Lemma 7.6 imply that K∞ is invariant. Therefore, by step 1, K∞ ⊆ InvH(K),
and, by step 3, K∞ = InvH(K). Summarising, InvH(K) is the largest (by step 1), closed (by step 2),
invariant (by step 4) subset of K.
Step 1: Every set L ⊆ K which invariant under (X, F, R, J) must be contained in InvH(K), since
all runs starting in L stay in L, and therefore in K.
Step 2: Clearly, for all i, Ki+1 ⊆ InvF (Ki, J) ⊆ Ki. Since K is closed, K0 is closed. Moreover, if
Ki is closed, then InvF (Ki, J) is closed (by Lemma 7.5, since J is closed), R 1
(Ki) is closed (since
R is lower semicontinuous), and, therefore, Ki+1 is closed. By induction, the Ki form a sequence of
nested closed sets, and therefore K∞ is closed (or the empty set).
Step 3: Consider a point x0 ∈ InvH(K) and show that x0 ∈ K∞. Assume, for the sake of
contradiction, that x0 ∈ K∞. Then there exists N ≥ 0 such that x ∈ KN . If N = 0, then
x0 ∈ K0 = K, therefore there exists a (trivial) run starting at x0 that is not viable in K. This
contradicts the assumption that x0 ∈ InvH(K). If N > 0, we show that there exists a run stating
at x0 that after at most one discrete transition finds itself outside KN−1. The claim then follows by
induction. Indeed, since x0 ∈ KN we must either have x0 ∈ InvF (KN−1, J), or x0 ∈ R 1
(KN−1). If
x0 ∈ R 1
(KN−1), there exists x1 ∈ R(x0) such that x1 ∈ KN−1, i.e., there exists a run starting at
x0 that transitions outside KN−1. If, on the other hand, x0 ∈ InvF (KN−1, J), then x0 ∈ J ∩ KN−1.
Therefore either x0 ∈ KN−1 (and the proof is complete), or x0 ∈ J and continuous evolution is
possible. In the latter case, since x0 ∈ InvF (KN−1, J), by Lemma 7.5 there exists a solution to
˙x ∈ F(x) starting at x0 that leaves KN−1 before reaching J. This solution is a run of (X, F, R, J)
that leaves KN−1.
Step 4: Recall that Pre∀
H(K∞) ⊆ K∞. Consider an arbitrary x0 ∈ K∞ and show that x0 ∈
Pre∀
H(K∞). Assume, for the sake of contradiction, that x0 ∈ InvF (K∞, J) ∩ R 1
(K∞). Then there
exists a run (τ, x) starting at x0 and a t τ1 such that2
x(t) ∈ K∞, or, in other words, there exists a
run (τ, x), a t τ1 and a N ≥ 0 such that x(t) ∈ KN . To see this notice that either x(τ0) ∈ R 1
(K∞)
(in which case we can take τ0 = τ0, x(τ1) ∈ K∞ and t = τ1) or x(τ0) ∈ InvF (K∞, J) (in which case
there exists a solution to ˙x ∈ F(x) that leaves K before reaching J). The same argument, however,
also shows that x(τ0) = x0 ∈ KN+1, which contradicts the assumption that x0 ∈ K∞.
Algorithm 4 (Invariance Kernel Approximation)
initialisation: K0 = K, i = 0
repeat
Ki+1 = Pre∀
H(Ki)
i = i + 1
until Ki = Ki−1
At each step, the algorithm computes the set of states for which all solution of the differential
inclusion ˙x ∈ F(x) stay in the Ki until they reach J. Ki+1 is then the subset of those states for
which if a transition is possible, the state after the transition is also in Ki.
2If τ = [τ0, τ0] or τ = [τ0, τ0[, t τ1 should be replaced by t τ0 or, respectively, t τ0.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 70
7.8 The Bouncing Ball Example
It is easy to check that FB is both Marchaud and Lipschitz and that RB is upper and lower semicontinuous
and has closed domain. Moreover, HB also satisfies Assumption 7.1, since R−1
(X) = J.
Therefore, we can immediately draw the following conclusion.
Proposition 7.1 Infinite runs exist for all x0 ∈ XT .
The proposition suggests that the impulse differential inclusion HB does not deadlock. However, it
is easy to show that for all x0 ∈ XT all infinite runs are Zeno.
Despite the Zeno behaviour, HB is in many ways a reasonable model of the bouncing ball system.
For example, one can show that the ball never falls below the surface on which it bounces, and that
the system dissipates energy.
Proposition 7.2 The set K = {x ∈ XT | x1 ≥ 0} is viable and invariant. For all C > 0 the set
L = {x ∈ XT | gx1 + x2
2/2 ≤ C} is invariant.
For the first part, notice that K ∩JB = {x ∈ XT | x1 = 0 and x2 ≤ 0}. Since RB does not affect x1,
K ∩ JB ⊆ R−1
(K) and R(K) ⊆ K. Moreover, K \ JB = {x ∈ XT | x1 > 0 or x1 = 0 and x2 > 0}.
For x such that x1 > 0, FB(x) ⊆ TK(x) = XB. For x such that x1 = 0 and x2 > 0, FB(x) ⊆ {v ∈
X | v1 > 0} = TK(x). Therefore, K is viable by Theorem 7.1 and invariant by Theorem 7.3.
For the second part, R leaves x1 unchanged and maps x2 to αx2. Therefore R(L) ⊆ L since α ∈ [0, 1].
Moreover
L \ J ={x ∈ XT | x1 > 0 or x2 > 0}
∩ {x ∈ XT | gx1 + x2
2/2 ≤ C}
For x ∈ L \ J such that gx1 + x2
2/2 < C, FB(x) ⊆ TK(x) = XB. For x ∈ L \ J such that
gx1 + x2
2/2 = C,
TK(x) = {v ∈ XB | v1g + v2x2 ≤ 0}
⊇ {v ∈ XB | v1g + v2x2 = 0} ⊇ FB(x)
The claim follows by Theorem 7.3.
7.9 Bibliography and Further Reading
Reachability with inputs has also been studied in the context of optimal control and differential
games [66, 94] and using ellipsoidal calculus [54, 53].
Other classes of control problems that have been studied for hybrid systems include supervisory
control [52, 11, 28] and optimal control [21, 35].
Because the analytical study of the resulting equations is rarely possible computational tools have
been developed to approximate the solutions numerically [27, 36, 26, 19, 81, 10, 80, 87].
Bibliography
[1] R. Alur, C. Courcoubetis, N. Halbawachs, T. A. Henzinger, P. H. Ho, X. Nicollin, A. Olivero,
J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer
Science, 138:3–34, 1995.
[2] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235,
1994.
[3] R. Alur and D. L. Dill. Automata for modeling real-time systems. In Proceedings of ICALP
’90, volume 443 of Lecture Notes in Computer Science, pages 322–335. Springer-Verlag, 1990.
[4] R. Alur and T.A. Henzinger. Modularity for timed and hybrid systems. In Proceedings of the
Eighth International Conference on Concurrency Theory (CONCUR 1997), number 1243 in
LNCS, pages 74–88. Springer Verlag, 1997.
[5] R. Alur, T.A. Henzinger, G. Lafferriere, and G.J. Pappas. Discrete abstractions of hybrid
systems. Proceedings of the IEEE, 88(7):971–984, July 2000.
[6] R. Alur and R.P. Kurshan. Timing analysis in COSPAN. In Hybrid Systems III, number 1066
in LNCS, pages 220–231. Springer Verlag, 1996.
[7] M. Anderson, D. Bruck, S. E. Mattsson, and T. Schonthal. Omsim- an integrated interactive
environment for object-oriented modeling and simulation. In IEEE/IFAC joint symposium on
computer aided control system design, pages 285–290, 1994.
[8] M. Andersson. Object-Oriented Modeling and Simulation of Hybrid Systems. PhD thesis, Lund
Institute of Technology, Lund, Sweden, December 1994.
[9] P.J. Antsaklis and A. Nerode, Editors. Special issue on hybrid control systems. IEEE Transactions
on Automatic Control, 43(4), April 1998.
[10] E. Asarin, O. Bournez, T. Dang, and O. Maler. Approximate reachability analysis of piecewiselinear
dynamical systems. In Nancy Lynch and Bruce H. Krogh, editors, Hybrid Systems:
Computation and Control, number 1790 in LNCS. Springer Verlag, 2000.
[11] E. Asarin, O. Bournez, T. Dang, O. Maler, and A. Pnueli. Effective synthesis of switching
controllers for linear systems. Proceedings of the IEEE, 88(7):1011–1025, July 2000.
[12] J.-P. Aubin. Viability Theory. Birkh¨auser, Boston, 1991.
[13] J.-P. Aubin and H. Frankowska. Set Valued Analysis. Birkh¨auser, Boston, 1990.
[14] J.-P. Aubin, J. Lygeros, M. Quincampoix, S.S. Sastry, and N. Seube. Impulse differential
inclusions: A viability approach to hybrid systems. IEEE Transactions on Automatic Control,
47(1):2–20, January 2002.
[15] A. Balluchi, L. Benvenuti, M.D. Di Benedetto, C. Pinello, and A.L. Sangiovanni-Vincentelli.
Automotive engine control and hybrid systems: Challenges and opportunities. Proceedings of
the IEEE, 88(7):888–912, July 2000.
71
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 72
[16] J. Bengtsson, K.G. Larsen, F. Larsson, P. Petterson, and W. Yi. UPAAL: a tool suit for
automatic verification of real-time systems. In Hybrid Systems III, number 1066 in LNCS,
pages 232–243. Springer Verlag, 1996.
[17] B. B´erard, P. Gastin, and A. Petit. On the power of non observable actions in timed automata.
In Actes du STACS ’96, Lecture Notes in Computer Science 1046, pages 257–268. SpringerVerlag,
1996.
[18] V.S. Borkar. Probability theory: an advanced course. Springer Verlag, New York, 1995.
[19] O. Botchkarev and S. Tripakis. Verification of hybrid systems with linear differential inclusions
using ellipsoidal approximations. In Nancy Lynch and Bruce H. Krogh, editors, Hybrid
Systems: Computation and Control, number 1790 in LNCS, pages 73–88. Springer Verlag,
2000.
[20] M.S. Branicky. Multiple Lyapunov functions and other analysis tools for switched and hybrid
systems. IEEE Transactions on Automatic Control, 43(4):475–482, 1998.
[21] M.S. Branicky, V.S. Borkar, and S.K. Mitter. A unified framework for hybrid control: Model
and optimal control theory. IEEE Transactions on Automatic Control, 43(1):31–45, 1998.
[22] M.S. Branicky, E. Dolginova, and N. Lynch. A toolbox for proving and maintaining hybrid
specifications. In A. Nerode P. Antsaklis, W. Kohn and S. Sastry, editors, Hybrid Systems IV,
number 1273 in LNCS, pages 18–30. Springer Verlag, 1997.
[23] R.W. Brockett. Hybrid models for motion control systems. In H.L. Trentelman and J.C.
Willems, editors, Perspectives in Control. Birkh¨auser, 1993.
[24] M. Broucke. Regularity of solutions and homotopy equivalence for hybrid systems. In IEEE
Conference on Decision and Control, Tampa, FL, 1998.
[25] C.G. Cassandras and S. Lafortune. Introduction to Discrete Event Systems. Kluwer Academic
Publishers, 1999.
[26] A. Chutinam and B. Krogh. Verification of polyhedral-invariant hybrid automata using polygonal
flow pipe approximations. In Frits W. Vaandrager and Jan H. van Schuppen, editors,
Hybrid Systems: Computation and Control, number 1569 in LNCS, pages 76–90. Springer
Verlag, 1999.
[27] T. Dang and O. Maler. Reachability analysis via face lifting. In S. Sastry and T.A. Henzinger,
editors, Hybrid Systems: Computation and Control, number 1386 in LNCS, pages 96–109.
Springer Verlag, 1998.
[28] J.M. Davoren and A. Nerode. Logics for hybrid systems. Proceedings of the IEEE, 88(7):985–
1010, July 2000.
[29] C. Daws, A. Olivero, S. Trypakis, and S. Yovine. The tool KRONOS. In R. Alur, T. Henzinger,
and E. Sontag, editors, Hybrid Systems III, number 1066 in LNCS, pages 208–219. Springer
Verlag, 1996.
[30] R. De Carlo, M. Branicky, S. Pettersson, and B. Lennarston. Perspectives and results on the
stability and stabilizability of hybrid systems. Proceedings of the IEEE, 88(7):1069–1082, July
2000.
[31] A. Deshpande, A. Gollu, and L. Semenzato. The SHIFT programming language for dynamic
networks of hybrid automata. IEEE Transactions on Automatic Control, 43(4):584–587, April
1998.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 73
[32] E. Dolginova and N. Lynch. Safety verification for automated platoon maneuvers: a case
study. In Oded Maler, editor, Proceedings of HART97, number 1201 in LNCS, pages 154–170.
Springer Verlag, Berlin, 1997.
[33] S. Engell, S. Kowalewski, C. Schulz, and O. Stursberg. Continuous-discrete interactions in
chemical processing plants. Proceedings of the IEEE, 88(7):1050–1068, July 2000.
[34] A. F. Filippov. Differential equations with discontinuous right-hand sides. Kluwer Academic
Publishers, 1988.
[35] G. Grammel. Maximum principle for a hybrid system via singular pertrubations. SIAM
Journal of Control and Optimization, 37(4):1162–1175, 1999.
[36] M.R. Greenstreet and I. Mitchell. Integrating projections. In S. Sastry and T.A. Henzinger,
editors, Hybrid Systems: Computation and Control, number 1386 in LNCS, pages 159–174.
Springer Verlag, 1998.
[37] M. Heemels. Linear Complementarity Systems: a Study in Hybrid Dynamics. PhD thesis,
Technische Universiteit Eindhoven, 1999.
[38] M. Heemels, H. Schumacher, and S. Weiland. Well-posedness of linear complementarity sysetms.
In Proc. 38th IEEE Conference on Decision and Control, Phoenix, AZ, 1999.
[39] W. P. M. Heemels, B. De Schutter, and A. Bemporad. Equivalence of hybrid dynamical
models. Automatica, 37(7):1085–1091, 2001.
[40] C. Heitmeyer and N. Lynch. The generalized railroad crossing: A case study in formal verification
of real-time systems. In Proc. ICCC Real-Time Systems Symposium, San Juan, Puerto
Rico, 1994.
[41] T. Henzinger, P. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata. In
27th
Annual Symposium on the Theory of Computing, STOC’95, pages 373–382. ACM Press,
1995.
[42] T. A. Henzinger, P. H. Ho, and H. Wong Toi. A user guide to HYTECH. In E. Brinksma,
W. Cleaveland, K. Larsen, T. Margaria, and B. Steffen, editors, TACAS 95: Tools and Algorithms
for the Construction and Analysis of Systems, number 1019 in LNCS, pages 41–71.
Springer Verlag, 1995.
[43] J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to automata theory, languages and
computation. Addison-Wesley Publishing, second edition, 2000.
[44] R. Horowitz and P. Varaiya. Control design of an automated highway system. Proceedings of
the IEEE, 88(7):913–925, July 2000.
[45] B. Hu, X. Xu, A.N. Michel, and P.J. Antsaklis. Robust stabilizing control laws for a class of
second order switched systems. Systems & Control Letters, 38:197–207, 1999.
[46] J. Imura and A. J. van der Schaft. Characterization of well-posedness of piecewise linear
systems. IEEE Transactions on Automatic Control, 45(9):1600–1619, September 2000.
[47] K.H. Johansson, M. Egerstedt, J. Lygeros, and S.S. Sastry. On the regularization of Zeno
hybrid automata. Systems and Control Letters, 38:141–150, 1999.
[48] K.H. Johansson, J. Lygeros, S.S. Sastry, and M. Egerstedt. Simulation of Zeno hybrid automata.
In IEEE Conference on Decision and Control, pages 3538–3543, Phoenix, Arizona,
U.S.A., December 7-10 1999.
[49] M. Johansson. Piecewise linear control systems. PhD thesis, Department of Automatic Control,
Lund Institute of Technology, Sweden, March 1999.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 74
[50] M. Johansson and A. Rantzer. Computation of piecewise quadratic lyapunov functions for
hybrid systems. IEEE Transactions on Automatic Control, 43(4):555–559, 1998.
[51] H.B. Khalil. Nonlinear Systems. Prentice Hall, third edition, 2001.
[52] X.D. Koutsoukos, P.J. Antsaklis, J.A. Stiver, and M.D. Lemmon. Supervisory control of hybrid
systems. Proceedings of the IEEE, 88(7):1026–1049, July 2000.
[53] A. B. Kurzhanski and P. Varaiya. On reachability under uncertainty. SIAM Journal of Control
and Optimization, 41(1):181–216, 2002.
[54] A.B. Kurzhanski and P. Varaiya. Ellipsoidal techniques for reachability analysis. In Nancy
Lynch and Bruce H. Krogh, editors, Hybrid Systems: Computation and Control, number 1790
in LNCS, pages 202–214. Springer Verlag, 2000.
[55] G. Lafferriere, G.J. Pappas, and S.S. Sastry. O-minimal hybrid systems. Mathematics of
Control, Signals, and Systems, 13(1):1–21, March 2000.
[56] M. Lemmon. On the existence of solutions to controlled hybrid automata. In Nancy Lynch and
Bruce H. Krogh, editors, Hybrid Systems: Computation and Control, number 1790 in LNCS,
pages 229–242. Springer Verlag, New York, 2000.
[57] B. Lennartsson, M. Tittus, B. Egardt, and S. Pettersson. Hybrid systems in process control.
Control Systems Magazine, 16(5):45–56, 1996.
[58] H.R. Lewis and C. Papadimitriou. Elements of the Theory of Computation. Prentice Hall,
second edition, 1997.
[59] D. Liberzon, J.P. Hespanha, and A.S. Morse. Stability of switched systems: A Lie algebraic
approach. Systems and Control Letters, 37(3):117–122, 1999.
[60] D. Liberzon and A.S. Morse. Basic problems in stability and design of switched systems. IEEE
Control Systems Magazine, 19:59–70, October 1999.
[61] C. Livadas, J. Lygeros, and N.A. Lynch. High-level modeling and analysis of the traffic alert
and collision avoidance system (TCAS). Proceedings of the IEEE, 88(7):926–948, July 2000.
[62] C. Livadas and N. Lynch. Formal verification of safety-critical hybrid systems. In S. Sastry and
T.A. Henzinger, editors, Hybrid Systems: Computation and Control, number 1386 in LNCS,
pages 253–272. Springer Verlag, 1998.
[63] J. Lygeros, K.H. Johansson, S.S. Sastry, and M. Egerstedt. On the existence of executions of
hybrid automata. In IEEE Conference on Decision and Control, pages 2249–2254, Phoenix,
Arizona, U.S.A., December 7-10 1999.
[64] J. Lygeros, K.H. Johansson, S.N. Simi´c, J. Zhang, and S.S. Sastry. Dynamical properties of
hybrid automata. IEEE Transactions on Automatic Control, 48(1):2–17, January 2003.
[65] J. Lygeros and N. Lynch. Strings of vehicles: Modeling and safety conditions. In S. Sastry and
T.A. Henzinger, editors, Hybrid Systems: Computation and Control, number 1386 in LNCS,
pages 273–288. Springer Verlag, 1998.
[66] J. Lygeros, C.J. Tomlin, and S.S. Sastry. Controllers for reachability specifications for hybrid
systems. Automatica, pages 349–370, March 1999.
[67] N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.
[68] N. Lynch, R. Segala, F. Vaandrager, and H.B. Weinberg. Hybrid I/O automata. In Hybrid
Systems III, number 1066 in LNCS, pages 496–510. Springer Verlag, 1996.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 75
[69] O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems.
In Theoretical Aspects of Computer Science, number 900 in LNCS, pages 229–242. Springer
Verlag, 1995.
[70] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: specification.
Springer-Verlag, Berlin, 1992.
[71] Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag,
New York, 1995.
[72] Zohar Manna and Henny Sipma. Deductive verification of hybrid systems using STeP. In
S. Sastry and T.A. Henzinger, editors, Hybrid Systems: Computation and Control, number
1386 in LNCS, pages 305–318. Springer Verlag, 1998.
[73] Zohar Manna and the STeP group. STeP: The Stanford Temporal Prover. Technical Report
STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994.
[74] S. E. Mattsson. On object-oriented modeling of relays and sliding mode behaviour. In Proc.
13th IFAC World Congress, volume F, pages 259–264, San Francisco, CA, 1996.
[75] S. E. Mattsson, M. Andersson, and K. J. ˚Astr¨om. Object-oriented modelling and simulation.
In D. A. Linkens, editor, CAD for Control Systems, chapter 2, pages 31–69. Marcel Dekker
Inc., New York, 1993.
[76] S. E. Mattsson, M. Otter, and H. Elmqvist. Modelica hybrid modeling and efficient simulation.
In IEEE Conference on Decision and Control, Phoenix, AZ, 1999.
[77] A.S. Matveev and A.V. Savkin. Qualitative theory of hybrid dynamical systems. Birkhauser,
Boston, 2000.
[78] R. May. Stability and Complexity of Model Ecosystems. Princeton University Press, Princeton,
NJ, 1973.
[79] A.N. Michel and B. Hu. Towards a stability theory for hybrid dynamical systems. Automatica,
35:371–384, 1999.
[80] I. Mitchell, A.M. Bayen, and C.J. Tomlin. Validating a hamilton-jacobi approximation to
hybrid system reachable sets. In M. Di Benedetto and A. Sangiovanni-Vincentelli, editors,
Hybrid Systems: Computation and Control, number 2034 in LNCS, pages 418–432. Springer
Verlag, 2001.
[81] I. Mitchell and C.J. Tomlin. Level set methods for computation in hybrid systems. In Nancy
Lynch and Bruce H. Krogh, editors, Hybrid Systems: Computation and Control, number 1790
in LNCS, pages 310–323. Springer Verlag, 2000.
[82] A.S. Morse. Control using logic based switching. In A. Isidori, editor, Trends in Control, pages
69–114. Springer Verlag, 1995.
[83] D.L. Pepyne and C.G. Cassandras. Optimal control of hybrid systems in manufacturing.
Proceedings of the IEEE, 88(7):1108–1123, July 2000.
[84] P.J. Antsaklis, Editor. Special issue on hybrid systems: Theory and applications. Proceedings
of the IEEE, 88(7), July 2000.
[85] A. Pnueli and J. Sifakis Editors. Hybrid systems. Theoretical Computer Science, 138(1), 1995.
[86] A. Puri, P. Varaiya, and V. Borkar. -approximation of differential inclusions. In IEEE
Conference on Decision and Control, pages 2892–2897, New Orleans, LA, 1995.
[87] P. Saint-Pierre. Approximation of viability kernels and capture basins for hybrid systems. In
European Control Conference, pages 2776–2783, Porto, Portugal, September 4-7 2001.
Lecture Notes on Hybrid Systems, c J. Lygeros, 2004 76
[88] S.S. Sastry. Nonlinear Systems: Analysis, Stability and Control. Springer Verlag, New York,
1999.
[89] A. V. Savkin, E. Skafidas, and R.J. Evans. Robust output feedback stabilizability via controller
switching. Automatica, 35:69–74, 1999.
[90] A. Savkin, Editor. Special issue on hybrid systems. Systems and Control Letters, 38(3),
October 1999.
[91] J.M. Schumacher, A.S. Morse, C.C. Pandelides, and S. Sastry, Editors. Special issue on hybrid
systems. Automatica, 35(3), March 1999.
[92] S. Simic, K.H. Johansson, S.S. Sastry, and J. Lygeros. Towards a geometric theory of hybrid
systems. In Nancy Lynch and Bruce H. Krogh, editors, Hybrid Systems: Computation and
Control, number 1790 in LNCS, pages 421–436. Springer Verlag, 2000.
[93] L. Tavernini. Differential automata and their simulators. Nonlinear Analysis, Theory, Methods
and Applications, 11(6):665–683, 1987.
[94] C.J. Tomlin, J. Lygeros, and S.S. Sastry. A game theoretic approach to controller design for
hybrid systems. Proceedings of the IEEE, 88(7):949–969, July 2000.
[95] C.J. Tomlin, G.J. Pappas, and S.S. Sastry. Conflict resolution for air traffic management: a case
study in multi-agent hybrid systems. IEEE Transactions on Automatic Control, 43(4):509–521,
1998.
[96] V. I. Utkin. Sliding Modes in Control and Optimization. Springer-Verlag, Berlin, 1992.
[97] A.J. van der Schaft and H. Schumacher. Complementarity modeling of hybrid systems. IEEE
Transactions on Automatic Control, 43(4):483–490, 1998.
[98] A.J. van der Schaft and H. Schumacher. An Introduction to Hybrid Dynamical Systems.
Number 251 in Lecture Notes in Control and Information Sciences. Springer-Verlag, 1999.
[99] P. Varaiya. Smart cars on smart roads: problems of control. IEEE Transactions on Automatic
Control, AC-38(2):195–207, 1993.
[100] M. Vidyasagar. Nonlinear Systems Analysis. Prentice Hall, second edition, 1992.
[101] H.B. Weinberg, Nancy Lynch, and Norman Delisle. Verification of automated vehicle protection
systems. In Hybrid Systems III, number 1066 in LNCS, pages 101–113. Springer Verlag,
1996.
[102] M. Wicks, P. Peleties, and R. De Carlo. Switched controller synthesis for the quadratic
stabilization of a pair of unstable linear systems. European Journal of Control, 4:140–147,
1998.
[103] S. Wiggins. Introduction to Applied Nonlinear Dynamical Systems and Chaos. Springer-Verlag,
third edition, 1997.
[104] Howard Wong-Toi. The synthesis of controllers for linear hybrid automata. In IEEE Conference
on Decision and Control, pages 4607–4613, San Diego, California, USA, December 10-12 1997.
[105] X. Xu and P.J. Antsaklis. Stabilization of second order LTI switched systems. International
Journal of Control, 73:1261–1279, 2000.
[106] H. Ye, A. Michel, and L. Hou. Stability theory for hybrid dynamical systems. IEEE Transactions
on Automatic Control, 43(4):461–474, 1998.
[107] J. Zhang, K.H. Johansson, J. Lygeros, and S.S. Sastry. Zeno hybrid systems. International
Journal of Robust and Nonlinear Control, 11:435–451, 2001.