1

Safety Verification and Control for Collision
Avoidance at Road Intersections

arXiv:1612.02795v1 [math.OC] 8 Dec 2016

Heejin Ahn and Domitilla Del Vecchio

Abstract—This paper presents the design of a supervisory
algorithm that monitors safety at road intersections and overrides
drivers with a safe input when necessary. The design of the
supervisor consists of two parts: safety verification and control
design. Safety verification is the problem to determine if vehicles
will be able to cross the intersection without colliding with current
drivers’ inputs. We translate this safety verification problem into
a jobshop scheduling problem, which minimizes the maximum
lateness and evaluates if the optimal cost is zero. The zero
optimal cost corresponds to the case in which all vehicles can
cross each conflict area without collisions. Computing the optimal
cost requires solving a Mixed Integer Nonlinear Programming
(MINLP) problem due to the nonlinear second-order dynamics
of the vehicles. We therefore estimate this optimal cost by formulating two related Mixed Integer Linear Programming (MILP)
problems that assume simpler vehicle dynamics. We prove that
these two MILP problems yield lower and upper bounds of the
optimal cost. We also quantify the worst case approximation
errors of these MILP problems. We design the supervisor to
override the vehicles with a safe control input if the MILP
problem that computes the upper bound yields a positive optimal
cost. We theoretically demonstrate that the supervisor keeps
the intersection safe and is non-blocking. Computer simulations
further validate that the algorithms can run in real time for
problems of realistic size.
Index Terms—safety verification; approximation; hybrid systems; least restrictive control; supervisory control; collision
avoidance; intersections; scheduling;

Fig. 1. General intersection. The safety verification problem in this scenario
can be approximately solved within quantified bounds. This intersection is
obtained from [15] to encompass 20 top crash locations in Massachusetts,
USA.

I. I NTRODUCTION

T

HE first fatality caused by a self-driving technology has
raised concerns about the safety of autonomous vehicles
[1]. As an approach to ensuring safety particularly at a road
intersection, this paper proposes the design of a safeguard,
called a supervisory algorithm or supervisor. The supervisor
monitors vehicles’ current states and inputs through vehicle-tovehicle and vehicle-to-infrastructure communications [2], and
determines if their inputs will cause collisions. If this is the
case, the supervisor intervenes to prevent collisions.
Informally, we state safety verification as a problem that
determines if the state trajectory can be kept outside an
unsafe set given an initial condition, where the unsafe set
is defined as the set of states corresponding to a collision
configuration. Reachability analysis has been used to solve
this problem by calculating the reachable region of a system
to find a set of initial states that can be controlled to avoid the
unsafe set [3]–[5]. However, reachability analysis of dynamical
This work was in part supported by NSF Award #1239182.
Heejin Ahn and Domitilla Del Vecchio are with the Department of Mechanical Engineering, Massachusetts Institute of Technology, 77 Massachusetts Avenue, Cambridge, USA. Email: hjahn@mit.edu and ddv@mit.edu

systems with large state spaces is usually challenging due to
the complexity of computing reachable sets. This motivates
the development of several approximation approaches. One
approximation approach is to consider a simpler dynamical
model to compute reachable sets instead of using the original
complex dynamical model, as studied in [6]–[8]. Another approximation approach is to approximate the original reachable
set by employing various geometric representations, which
include polyhedra [9], ellipsoids [10], or parallelotopes [11]. It
has been shown in [12] that monotonicity of system dynamics,
for which state trajectories preserve a partial ordering on
states and inputs, makes the reachability analysis relatively
simple. This is because for such systems, the boundary of a
reachable set can be computed by considering only maximum
and minimum states and inputs [13]. Indeed, an exact method
for the reachability analysis is presented in [14] for piecewise
continuous and monotone systems.
Our approach relies on the monotonicity of the system
and on the approximation of vehicle dynamics. In this paper,
we consider complex intersection scenarios in which vehicles
follow predefined paths as shown in Figure 1. The longitudinal

2

dynamics of vehicles are piecewise continuous and monotone
[14], which enables us to translate the safety verification
problem to a scheduling problem. This scheduling problem
minimizes the maximum lateness and determines if the optimal
cost is zero. The zero optimal cost implies that every job
(vehicle) can be processed on each machine (conflict area)
in time, and equivalently, vehicles can cross the intersection
without collision. However, because of the nonlinear secondorder dynamics of vehicles, the scheduling problem is a Mixed
Integer Nonlinear Programming (MINLP) problem, which
is computationally difficult to solve. We therefore estimate
the optimal cost of the scheduling problem by formulating
two Mixed Integer Linear Programming (MILP) problems
that assume first-order dynamics and nonlinear second-order
dynamics on a restricted input set, respectively. We prove
that these MILP problems yield lower and upper bounds of
the optimal cost. These lower and upper bound problems are
equivalent to computing over- and under-approximation of the
reachable sets of the original problem. These approximation
bounds are quantified in this paper.
The scheduling problem has been employed to solve the
safety verification problem for collision avoidance at an intersection [16]–[21]. In [16]–[20], the safety verification problem
is solved exactly with an assumption that the paths of vehicles
intersect only at a single conflict point. Multiple conflict points
are considered in [21] and the safety verification problem
is solved exactly when vehicle dynamics are restricted to
first-order linear dynamics. By contrast, the main contribution
of this paper is to solve the safety verification problem
on multiple conflict points for general longitudinal vehicle
dynamics, which are nonlinear and second-order. A similar
problem of robots following predefined paths is considered
in [22], [23], but their approach is not designed for safety
verification and thus restricted to zero initial speed with the
double integrator dynamics. Our scheduling approach can deal
with general vehicle dynamics and verify safety at any given
state.
Recently, intersection management has been receiving considerable research attention. Most of the recent works concentrate on autonomous intersection management, where a
controller takes control of vehicles at all times until they cross
the intersection [24]–[30]. Our approach, instead, is to design a
least restrictive supervisor in the sense that it overrides drivers
only when they cannot avoid a collision.
Collision avoidance for multiple vehicles has been an active
area of research mostly in air traffic management. Various
approximation approaches are employed to solve collision
avoidance problems, such as approximation of dynamics [31]–
[36] or relaxation of the original problems [37], [38]. The
controllers presented in these works are not least restrictive,
as opposed to the controller considered in this paper. While
least restrictive controllers are presented in [3], [4], they are
applicable only to a small number of vehicles due to the
computational complexity of safety verification. As a scalable
approach with the number of vehicles, decentralized control
is also employed in [39]–[41]. However, decentralized control
usually terminates with suboptimal solutions or deadlock. In
this paper, we present the design of a centralized controller and

2

2

1

3

3

1

Fig. 2. An intersection is modeled as a set of conflict areas near which two
longitudinal predefined paths intersect.

prove that it is non-blocking. We validate through computer
simulations that this controller can run in real time for realistic
size scenarios such as that illustrated in Figure 1.
The rest of this paper is organized as follows. In Section II,
we define an intersection model and a vehicle dynamic model.
The safety verification problem is stated in Section III and
translated into a scheduling problem in Section IV. To solve
this problem, we formulate the lower and upper bound problems and quantify their approximation bounds in Section V.
Based on the upper bound problem, a supervisory algorithm
is introduced and proved to be non-blocking in Section VI.
We present simulation results in Section VII and conclude the
paper in Section VIII.
II. S YSTEM D EFINITION
A. Intersection Model
At a road intersection, vehicles tend to follow predefined
paths, which intersect at several conflict points. We define an
area around each conflict point accounting for the length of
vehicles and call it a conflict area. In this paper, we model an
intersection as a collection of all conflict areas. For example,
in Figure 2, the intersection is modeled as a set of conflict
areas 1-3.
The main focus of this paper is to prevent collisions among
vehicles whose paths intersect at conflict areas. Thus, we
assume that there is only one vehicle per lane and neglect rearend collisions. These can be included using a similar approach
as used in [17].
B. Vehicle Dynamical Model
With a vehicle state (xj , ẋj ) where xj ∈ Xj ⊆ R is the
position of vehicle j on its longitudinal path and ẋj ∈ Ẋj :=
[ẋj,min , ẋj,max ] ⊂ R is the speed, the longitudinal dynamics
of vehicle j are described as follows:
ẍj = fj (xj , ẋj , uj ).

(1)

The input uj is the throttle or brake input in the space Uj :=
[uj,min , uj,max ] ⊂ R.
Let us consider n vehicles approaching an intersection. The
whole system dynamics can be obtained by combining the
individual dynamics (1) and written as follows:
ẍ = f (x, ẋ, u),

(2)

3

where x = (x1 , . . . , xn ) ∈ X ⊆ Rn and similarly, ẋ ∈ Ẋ =
[ẋmin , ẋmax ] ⊂ Rn , u ∈ U = [umin , umax ] ⊂ Rn .
We define an input signal uj (·) : t ∈ R 7→ uj (t) ∈ Uj in the
input signal space Uj . Let xj (t, uj (·), xj (0), ẋj (0)) denote the
position reached at time t starting from (xj (0), ẋj (0)) using
an input signal uj (·) ∈ Uj . We also use the aggregate position
x(t, u(·), x(0), ẋ(0)) with the aggregate input signal u(·) ∈ U.
Similarly, we use ẋ(t, u(·), x(0), ẋ(0)) to denote the speed
at time t evolving with u(·). Regarding these, we make the
following assumption.
Assumption 1. For all j ∈ {1, . . . , n}, the position
xj (t, uj (·), xj (0), ẋj (0)) depends continuously on uj (·) ∈ Uj ,
and the input signal space Uj is path-connected.
u′j (·)

u′j (t)

We say uj (·) ≤
∈ Uj if uj (t) ≤
∈ Uj for all
t ≥ 0. We consider ẋj,min > 0 to exclude a trivial scenario
in which vehicles come to a full stop before an intersection
and do not cross it. Most importantly, we assume that the
individual dynamics (1) are monotone, that is, they satisfy the
following property.
Assumption 2. For all j ∈ {1, . . . , n}, if uj (·) ≤ u′j (·),
xj (0) ≤ x′j (0), ẋj (0) ≤ ẋ′j (0), and t ≤ t′ ,

1,1

3,1

2,2

1,2

3,3

2,3
(a)

3,1
2,2

1,2
2,3
(b)

Fig. 3. (a) All operations of the scenario in Figure 2. (b) Operations when
β11 ≤ x1 (0) < β31 , x2 (0) < β22 , and β33 ≤ x3 (0) < β23 . See
Example 1 for more details.

IV. S CHEDULING : E QUIVALENT P ROBLEM

TO

P ROBLEM 1

In this section, we formulate a scheduling problem and
present the theorem stating that this problem is equivalent to
the safety verification problem (Problem 1).
A scheduling problem can be described by a graph representation [42]. For a node, let (i, j) be an operation of vehicle
j processing on conflict area i. The collection of all operations
is denoted by N̄ .
N̄ := {(i, j) ∈ {1, . . . , m} × {1, . . . , n} :
conflict area i is on the route of vehicle j}.

xj (t, uj (·), xj (0), ẋj (0)) ≤ xj (t′ , u′j (·), x′j (0), ẋ′j (0))

We also define a set N ⊆ N̄ that contains operations to be
processed given an initial position x(0).

for all t ≥ 0.

N := {(i, j) ∈ N̄ : xj (0) < βij }.

III. P ROBLEM S TATEMENT
Let us consider n vehicles approaching an intersection that
is modeled as a collection of m conflict areas. We denote the
location of conflict area i on the longitudinal path of vehicle j
as an open interval (αij , βij ) ⊂ R. We say a collision occurs
at an intersection if two vehicles stay inside the same conflict
area simultaneously. This configuration is referred to as a bad
set, which is denoted by B and defined as follows:
B := {x ∈ X : xj ∈ (αij , βij ) and xj ′ ∈ (αij ′ , βij ′ )
for some i ∈ {1, . . . , m} and j 6= j ′ ∈ {1, . . . , n}}

Recall that (αij , βij ) ⊂ R denotes the location of conflict
area i on the longitudinal path of vehicle j. Notice that N
is the set of all the operations of interest given x(0) because
βij ≤ xj (0) indicates that vehicle j has exited conflict area i.
A first operation set F ⊆ N and a last operation set L ⊆ N
are defined as follows:
F := {(i, j) ∈ N : (i, j) is the first operation of vehicle j},
L := {(i, j) ∈ N : (i, j) is the last operation of vehicle j}.

(3)

The main interest of this paper is safety verification, that is,
verifying whether the system can avoid entering the bad set
at all future time. We approach this by stating a mathematical
problem, called the safety verification problem, as follows.
Problem 1 (safety verification). Given an initial condition
(x(0), ẋ(0)), determine if there exists u(·) ∈ U such that
x(t, u(·), x(0), ẋ(0)) ∈
/ B for all t ≥ 0.
To answer this problem, we need to evaluate all possible
input signals, which are functions of time, until finding one
satisfying the condition. To avoid this exhaustive and infinite
set of computations, we translate this problem to a scheduling
problem, which is to find feasible schedules, non-negative real
numbers, for vehicles to cross the conflict areas. The rationale
behind this translation is that real numbers are computationally
less complicated to manipulate than functions. While this
scheduling problem is still not easy to solve, we can provide
its approximate solutions efficiently.

Now, let us define arcs in the graph. We define sets of
conjunctive arcs C and disjunctive arcs D, which connect two
operations in N as follows:
C := {(i, j) → (i′ , j) : vehicle j crosses conflict area i
and then conflict area i′ for some i, j, j ′ },
D := {(i, j) ↔ (i, j ′ ) : vehicles j and j ′ share
the same conflict area i for some i, j, j ′ }.
That is, an element in C represents the sequence of operations
on the path of a vehicle, and an element in D represents the
undetermined sequence of operations on the same conflict area.
Example 1. In the scenario in Figure 2, suppose β11 ≤
x1 (0) < β31 , x2 (0) < β22 , and β33 ≤ x3 (0) < β23 . The
operations are illustrated in Figure 3, where the operation sets
N̄ and N become as follows:
N̄ = {(1, 1), (3, 1), (2, 2), (1, 2), (3, 3), (2, 3)},
N = {(3, 1), (2, 2), (1, 2), (2, 3)}.

4

Here, the first and last operation sets are F
=
{(3, 1), (2, 2), (2, 3)}, L = {(3, 1), (1, 2), (2, 3)}. The sets of
conjunctive and disjunctive arcs are C = {(2, 2) → (1, 2)}
and D = {(2, 2) ↔ (2, 3)}.
We now introduce scheduling parameters, release times,
deadlines, and process times, to formulate a jobshop scheduling problem [42].
Given an initial condition (xj (0), ẋj (0)), let Tij be the
time that vehicle j will enter conflict area i, that is,
xj (Tij , uj (·), xj (0), ẋj (0)) = αij for some uj (·) ∈ Uj . Let
T be the set of Tij for all (i, j) ∈ N . A jobshop scheduling
problem is to find this set, called a schedule, such that vehicles
never meet inside a conflict area.
Given T, the release time Rij (T) is the soonest time at
which vehicle j can enter conflict area i under the constraint
that it enters the previous conflict area i′ at Ti′ j . The deadline
Dij (T) is the latest such time. The process time Pij (T) is
the minimum time that vehicle j takes to exit conflict area
i under the constraint that it enters the same conflict area at
time Tij and the next conflict area i′′ at time Ti′′ j . We omit
the argument T if it is clear from context.
Formally, the release time and deadline are defined as
follows. Given an initial condition (x(0), ẋ(0)) and T, for
all (i, j) ∈ N \ F , there is a preceding operation (i′ , j) such
that (i′ , j) → (i, j) ∈ C.
Rij (T) :=

min {t : xj (t, uj (·), xj (0), ẋj (0)) = αij

uj (·)∈Uj

with constraint xj (Ti′ j , uj (·), xj (0), ẋj (0)) = αi′ j },
(4)
Dij (T) := max {t : xj (t, uj (·), xj (0), ẋj (0)) = αij
uj (·)∈Uj

with constraint xj (Ti′ j , uj (·), xj (0), ẋj (0)) = αi′ j }.
If the constraint is not satisfied, set Rij = ∞ and Dij = −∞.
For all (i, j) ∈ F , such a preceding operation (i′ , j) does not
exists. If xj (0) < αij ,
Rij :=

min {t : xj (t, uj (·), xj (0), ẋj (0)) = αij },

uj (·)∈Uj

Dij := max {t : xj (t, uj (·), xj (0), ẋj (0)) = αij }.

(5)

uj (·)∈Uj

If αij ≤ xj (0), set Rij = Dij = 0. Notice that for (i, j) ∈ F ,
the release time and deadline are independent of T.
The process time is defined as follows. Given an initial
condition (x(0), ẋ(0)) and T, for all (i, j) ∈ N \ L, there is
a succeeding operation (i′′ , j) such that (i, j) → (i′′ , j) ∈ C.
If xj (0) < αij ,
Pij (T) :=

min {t : xj (t, uj (·), xj (0), ẋj (0)) = βij

uj (·)∈Uj

with constraints xj (Tij , uj (·), xj (0), ẋj (0)) = αij

(6)

and xj (Ti′′ j , uj (·), xj (0), ẋj (0)) = αi′′ j }.
Set Pij (T) := minuj (·)∈Uj {t : xj (t, uj (·), xj (0), ẋj (0)) =
βij with constraint xj (Ti′′ j , uj (·), xj (0), ẋj (0)) = αi′′ j } if
αij ≤ xj (0) < βij . For all (i, j) ∈ L, such a succeeding
operation (i′′ , j) does not exist. If xj (0) < αij ,
Pij (T) :=

min {t : xj (t, uj (·), xj (0), ẋj (0)) = βij

uj (·)∈Uj

with constraint xj (Tij , uj (·), xj (0), ẋj (0)) = αij }.

(7)

If αij ≤ xj (0) < βij , set Pij := minuj (·)∈Uj {t :
xj (t, uj (·), xj (0), ẋj (0)) = βij }. If βij ≤ xj (0), operation
(i, j) is not of interest since vehicle j has already crossed
conflict area i. If the constraints are not satisfied, set Pij = ∞.
Using the definitions above, a jobshop scheduling problem
is formulated as follows.
Problem 2 (jobshop scheduling problem). Given an initial
condition (x(0), ẋ(0)), determine if s∗ = 0:
s∗ := minimize max (Tij − Dij (T), 0)
T,k

(i,j)∈N

subject to
for all (i, j) ∈ N ,
Rij (T) ≤ Tij ,
′
for all (i, j) ↔ (i, j ) ∈ D,


Pij (T) ≤ Tij ′ + M (1 − kijj ′ ),
Pij ′ (T) ≤ Tij + M (1 − kij ′ j ),


kijj ′ + kij ′ j = 1.

(P2.1)

(P2.2)

where T = {Tij : (i, j) ∈ N }, k = {kijj ′ ∈ {0, 1} :
for all (i, j) ↔ (i, j ′ ) ∈ D}, and M > 0 is a large number.
In the scheduling literature, max(Tij − Dij (T), 0) is called
the maximum lateness. This cost indicates the existence of a
schedule that violates the deadline, and thus its minimization
is one of the most studied scheduling problems [42].
If s∗ = 0, we have Tij that satisfies Tij ≤ Dij (T) for
all (i, j) ∈ N . The fact that Tij is bounded by Rij (T) and
Dij (T) encodes the bounds of the input. Constraint (P2.2)
says that for two vehicles j and j ′ that share the same conflict
area i, either vehicle j ′ enters it after vehicle j exits (when
kijj ′ = 1) or the other way around (when kij ′ j = 1). By
this constraint, each conflict area is exclusively used by one
vehicle at a time. Thus, the existence of such T and k that
yield s∗ = 0 is equivalent to the existence of u(·) ∈ U to avoid
the bad set. This is the essence of the proof of the following
theorem.
Theorem 1 ( [21]). Problem 1 is equivalent to Problem 2.
In [21], Problem 2 was introduced as a feasibility problem
and the above theorem was proved.
Theorem 1 implies the following: given an initial condition
(x(0), ẋ(0)),
s∗ = 0 =⇒ a safe input signal exists to avoid B,
s∗ > 0 =⇒ no safe input signal exists to avoid B.
That is, s∗ is the indicator of the vehicles’ safety.
While this theorem holds for general dynamics (1), Problem 2 can be difficult to solve depending on which vehicle dynamics are considered. In [21], vehicle dynamics are assumed
to be first-order and linear in which case Problem 2 becomes
a Mixed Integer Linear Programming (MILP) problem, which
can be easily solved by a commercially available solver, such
as CPLEX [43]. In this paper, due to the nonlinear and
higher order vehicle dynamics, the constraints are nonlinear
in Tij and therefore, Problem 2 is a Mixed Integer NonLinear Programming (MINLP) problem, which is notorious
for its computational intractability. To approximately solve

5

Problem 2, we formulate two MILP problems that yield lower
and upper bounds of s∗ , respectively. The MILP problem that
computes the lower bound is a reformulation of the MILP
problem given in [21], and the MILP problem that computes
the upper bound is based on nonlinear second-order dynamics
with a limited input space.
V. A PPROXIMATE S OLUTIONS

TO

P ROBLEM 2

In this section, we provide two MILP problems that yield
lower and upper bounds of the optimal cost of Problem 2.
Using these bounds, we can quantify the approximation error
between the approximate solution and the exact solution to
Problem 2.

Let us consider first-order vehicle dynamics, that is,
χ̇ = v,

Definition 1. Given an initial condition (x(0), ẋ(0)) and
χ(0) = x(0), release times rij and deadlines dij are defined
as follows.
For all (i, j) ∈ F , if xj (0) < αij ,
min {t : xj (t, uj (·), xj (0), ẋj (0)) = αij },

uj (·)∈Uj

dij := max {t : xj (t, uj (·), xj (0), ẋj (0)) = αij }.
uj (·)∈Uj

If αij ≤ xj (0), then rij = dij = 0.
For (i, j) ∈ N \ F , there exists a preceding operation (i′ , j)
such that (i′ , j) → (i, j) ∈ C. Given pi′ j ≥ 0 such that
χj (pi′ j , vj (·), χj (0)) = βi′ j for some vj (·) ∈ Vj ,
αij − βi′ j
,
ẋj,max

dij := pi′ j +

for all (i, j) ∈ N ,

rij ≤ tij ,
(P3.1)
βij − αij
βij − αij
≤ pij − tij ≤
,
ẋj,max
ẋj,min
(P3.2)

for all (i, j) ↔ (i, j ′ ) ∈ D,


pij ≤ tij ′ + M (1 − kijj ′ ),
pij ′ ≤ tij + M (1 − kij ′ j ),


kijj ′ + kij ′ j = 1.

(P3.3)

where t = {tij : (i, j) ∈ N }, p = {pij : (i, j) ∈ N },
k := {kijj ′ ∈ {0, 1} : for all (i, j) ↔ (i, j ′ ) ∈ D} and M is
a large number in R+ .

Theorem 2. s∗L ≤ s∗

where χ ∈ X is the vector representing the position of vehicles
on their longitudinal paths, and v is the input. The input v
lies in the space Ẋ = [ẋmin , ẋmax ] with ẋmin > 0. We also
define an input signal vj (·) : R+ → Ẋj in the space Vj for
vehicle j.
We define release times and deadlines for the lower bound
problem. Process times are considered as decision variables.

rij := pi′ j +

for all (i, j) ∈ N ,

From (8), we know that the objective function and constraint (P3.1) are linear with the decision variables. Thus,
this problem is a Mixed Integer Linear Programming (MILP)
problem.

A. Lower bound problem

rij :=

subject to

αij − βi′ j
.
ẋj,min

(8)

Notice that for the first operations, (i, j) ∈ F , release times
and deadlines consider general dynamics (1) and thus rij =
Rij and dij = Dij by (5). This is a different definition from
that in [21] and results in a tighter constraint than rij = (αij −
χj (0))/ẋj,max and dij = (αij − χj (0))/ẋj,min .
Using Definition 1, the lower bound problem is formulated
as a decision problem in which the maximum lateness is
minimized.

Proof: Suppose Problem 2 finds T∗ and k∗ with the
corresponding cost s∗ , whether or not s∗ = 0. We will show
that t̃ = T∗ and k̃ = k∗ become a feasible solution for
Problem 3 with some p̃.
Given T∗ , we have Pij (T∗ ) for all (i, j) ∈ N . Consider
p̃ij = Pij (T∗ ). From (6) and (7), Pij (T∗ ) − Tij∗ = p̃ij − t̃ij
is the time to reach βij from αij and thus satisfies (P3.2).
Constraint (P3.3) is the same as constraint (P2.2) in Problem 2.
We will show that rij ≤ Rij (T∗ ) and Dij (T∗ ) ≤ dij . As
mentioned earlier, for (i, j) ∈ F , rij = Rij and dij = Dij .
For (i, j) ∈ N \ F , we have a preceding operation (i′ , j) such
that (i′ , j) → (i, j) ∈ C. By (4), Rij is equal to Ti∗′ j plus
the minimum time to reach αij from αi′ j . Considering this
definition with (6), Rij is again equal to Pi′ j plus the minimum
time to reach αij from βi′ j , thereby Rij ≥ Pi′ j + (αij −
βi′ j )/ẋj,max . Also, since Pi′ j = p̃i′ j , we have Pi′ j + (αij −
βi′ j )/ẋj,max = rij . Thus rij ≤ Rij . Similarly, Dij ≤ dij . By
these inequalities, Rij ≤ Tij∗ implies rij ≤ Tij∗ = t̃ij , which
is constraint (P3.1).
Therefore, t̃, p̃, and k̃ is a feasible solution of Problem 3.
Since Dij ≤ dij , s∗L ≤ max(t̃ij − dij , 0) ≤ max(Tij∗ −
Dij , 0) = s∗ .
B. Upper bound problem
In this section, we relax Problem 2 to a MILP problem by
considering general dynamics (1) on a restricted input space.
This problem is to find a set of times at which vehicles enter
their first conflict area, assuming that to reach the following
conflict areas all vehicles apply maximum input. The rationale
here is that once a vehicle enters an intersection, the driver tries
to exit as soon as possible.
We define αj,min to denote the first conflict area as follows:

Problem 3 (lower bound problem). Given an initial condition
(x(0), ẋ(0)), determine if s∗L = 0:

αj,min := min αij .

s∗L := minimize max (tij − dij , 0)

Recall that N̄ is a set of all operations independent of an initial
condition.

t,p,k

(i,j)∈N

(i,j)∈N̄

6

If xj (0) < αj,min , for (i, j) ∈ F ,
T̄ij = TijF ,
P̄ij =

TijF

(11)
+ min {t : xj (t, uj (·), αij , ẋj,min ) = βij },
uj (·)∈Uj

and for (i, j) ∈ N \ F , there exists the first operation (i′ , j)
such that (i′ , j) ∈ F and αi′ j = αj,min .
T̄ij = TiF′ j + min {t : xj (t, uj (·), αj,min , ẋj,max ) = αij },
uj (·)∈Uj

(a) xj (0) < αj,min = αi′ j

P̄ij =

(b) αi′ j ≤ xj (0) < βi′ j
(i′ , j)

TiF′ j

+ min {t : xj (t, uj (·), αj,min , ẋj,min ) = βij }.
uj (·)∈Uj

(i′ , j)

Fig. 4. Illustration of Definitions 2 and 3. Suppose
∈ F and
→
(i, j) ∈ C. We can compute P̄i′ j , T̄ij , P̄ij by considering the maximum input
inside the intersection.

(12)
If αj,min ≤ xj (0), for (i, j) ∈ F ,
T̄ij = TijF ,

In the upper bound problem, the time to reach the first
conflict area is a decision variable, as opposed to Problems 2
and 3 whose decision variables are the entering times for all
conflict areas. This decision variable, called a schedule, is
denoted by TF = {TijF : for all (i, j) ∈ F } and defined
as xj (TijF , uj (·), xj (0), ẋj (0)) = αij for some uj (·) ∈ Uj if
xj (0) < αij and otherwise TijF = 0.
The release times and deadlines are defined only for the
first operation as follows.
Definition 2. Given an initial condition (x(0), ẋ(0)), release
times R̄ = {R̄ij : for all (i, j) ∈ F } and deadlines D̄ =
{D̄ij : for all (i, j) ∈ F } are defined as follows.
For all (i, j) ∈ F , if xj (0) < αj,min ,
R̄ij :=

min {t : xj (t, uj (·), xj (0), ẋj (0)) = αj,min },

uj (·)∈Uj

D̄ij := max {t : xj (t, uj (·), xj (0), ẋj (0)) = αj,min }.

(9)

uj (·)∈Uj

uj (·)∈Uj

and for (i, j) ∈ N \ F , there exists the first operation (i′ , j)
such that (i′ , j) ∈ F .
T̄ij = TiF′ j − R̄i′ j +
min {t : xj (t, uj (·), xj (0), ẋj (0)) = αij },

uj (·)∈Uj

(14)

P̄ij = TiF′ j − R̄i′ j +
min {t : xj (t, uj (·), xj (0), ẋj (0)) = βij }.

uj (·)∈Uj

In (13) and (14), we have R̄ij = D̄ij by (10) and thus for
(i′ , j) ∈ F , TiF′ j − R̄i′ j = 0 if TiF′ j ∈ [R̄i′ j , D̄i′ j ].
Using these definitions, we formulate the upper bound
problem.

min {t : xj (t, uj (·), xj (0), ẋj (0)) = αij },

uj (·)∈Uj

(13)

min {t : xj (t, uj (·), xj (0), ẋj (0)) = βij }.

Problem 4 (upper bound problem). Given an initial condition
(x(0), ẋ(0)), determine if s∗U = 0:

If αj,min ≤ xj (0) < αij ,
R̄ij :=

P̄ij = TijF − R̄ij +

s∗U := minimize max (TijF − D̄ij , 0)

(10)

D̄ij = R̄ij .
If αij ≤ xj (0), set R̄ij = D̄ij = 0.
Notice that R̄ij = Rij and D̄ij = Dij if xj (0) < αj,min ,
and D̄ij = R̄ij = Rij if xj (0) ≥ αj,min . The release time
R̄ij and the deadline D̄ij depend only on an initial condition
(xj (0), ẋj (0)), not on the decision variable TijF .
Given a schedule TF , we define T̄ = {T̄ij : for all (i, j) ∈
N } and P̄ = {P̄ij : for all (i, j) ∈ N } as illustrated in
Figure 4. Suppose vehicle j has the first operation (i′ , j).
When vehicle j is outside the intersection (xj (0) < αj,min ),
T̄ij and P̄ij represent the minimum times at which vehicle j
can enter and exit conflict area i, respectively, no matter what
speed it has at TiF′ j . When vehicle j is inside the intersection
(αj,min ≤ xj (0)), T̄ij and P̄ij are the minimum times at
which it enters and exits conflict area i, respectively. These
are formally defined as follows.
Definition 3. Given an initial condition (x(0), ẋ(0)) and a
schedule TF , we define T̄ = {T̄ij : for all (i, j) ∈ N } and
P̄ = {P̄ij : for all (i, j) ∈ N } as follows.

(i,j)∈F

TF ,k

subject to
R̄ij ≤ TijF ,

for all (i, j) ∈ F ,

(P4.1)

′

for all (i, j) ↔ (i, j ) ∈ D,


P̄ij ≤ T̄ij ′ + M (1 − kijj ′ ),
P̄ij ′ ≤ T̄ij + M (1 − kij ′ j ),


kijj ′ + kij ′ j = 1.

(P4.2)

where TF = {TijF : for all (i, j) ∈ F }, k = {kijj ′ ∈ {0, 1} :
for all (i, j) ↔ (i, j ′ ) ∈ D}, and M is a large number in R+ .
The constraints in the problem are written in linear forms
with the decision variable TF as noticed in (11)-(14). Thus,
the problem is a MILP problem.
We will show that s∗U in Problem 4 can be considered as an
upper bound of s∗ in Problem 2 in the sense that s∗ ≤ M s∗U
for a large number M > 0. This inequality is not trivial if
s∗U = 0. In the following thereom, therefore, we will show that
s∗U = 0 implies s∗ = 0 for any initial condition (x(0), ẋ(0)).
Theorem 3. s∗U = 0 ⇒ s∗ = 0.

7

TABLE I
S UMMARY OF T HEOREMS 2 AND 3

Proof: Suppose Problem 4 finds an optimal solution
∗
TF ∗ = {TijF ∗ : (i, j) ∈ F } and k∗ = {kijj
′ : (i, j) ↔
′
∗
(i, j ) ∈ D} that yields sU = 0.
We define T̃ and P̃ as follows. For (i, j) ∈ F , if xj (0) <
αij ,

Case I
Case II
Case III

s∗L
·
0
+

s∗U
0
+
·

s∗
0
?
+

T̃ij =TijF ∗,
P̃ij =TijF ∗ + min {t : xj (t, uj (·), αij , ẋ0j ) = βij },

(15)

uj (·)∈Uj

where ẋ0j = ẋj (TijF ∗, uj (·), xj (0), ẋj (0)) with αij =
xj (TijF ∗ , uj (·), xj (0), ẋj (0)). If xj (0) ≥ αij , let T̃ij = TijF ∗ =
0 and P̃ij = min{t : xj (t, uj (·), xj (0), ẋj (0)) = βij }.
For (i, j) ∈ N \ F , there exists the first operation (i′ , j) ∈
F , and
T̃ij =TiF′ j∗ + min {t : xj (t, uj (·), αi′ j , ẋ0j ) = αij },
uj (·)∈Uj

P̃ij =TiF′ j∗

+ min {t : xj (t, uj (·), αi′ j , ẋ0j ) = βij },

(16)

uj (·)∈Uj

where
= ẋj (TiF′ j∗ , uj (·), xj (0), ẋj (0)) with αi′ j =
F∗
xj (Ti′ j , uj (·), xj (0), ẋj (0)).
Notice that P̃ij is Pij (T̃) by (6) and (7). We will show that
T̃ and k̃ = k∗ is a feasible solution to Problem 2.
First, we will show that T̃ satisfies constraint (P2.1) in
Problem 2. For all (i, j) ∈ F , R̄ij = Rij and D̄ij ≤ Dij .
Since TijF ∗ satisfies constraint (P4.1), we have Rij ≤ T̃ij . For
(i, j) ∈ N \ F , we define T̃ij as the minimum time to reach
conflict area i, thereby T̃ij = Rij (T̃) by (4). This establishes
that Rij ≤ T̃ij for all (i, j) ∈ N .
For constraint (P2.2) in Problem 2, let us focus on (15), (16),
and Definition 3 given TF ∗ . If xj (0) < αj,min , we have T̄ij ≤
T̃ij and P̃ij ≤ P̄ij because T̄ij and P̄ij are computed with
the maximum and minimum speed, respectively. If xj (0) ≥
αj,min , for (i′ , j) ∈ F we have TiF′ j∗ = R̄i′ j since s∗U = 0
and R̄i′ j = D̄i′ j . This implies that T̄ij = T̃ij and P̄ij = T̃ij .
Thus, constraint (P4.2) becomes
ẋ0j

∗
∗
P̃ij ≤ P̄ij ≤ T̄ij ′ + M (1 − kijj
′ ) ≤ T̃ij ′ + M (1 − kijj ′ ),

P̃ij ′ ≤ P̄ij ′ ≤ T̄ij + M (1 −

∗
kij
′j )

≤ T̃ij + M (1 −

∗
kij
′ j ).

That is, T̃ and k̃ = k∗ satisfy constraint (P2.2) in Problem 2.
Now we have a feasible solution T̃ and k̃. For (i, j) ∈ N \
F , we have T̃ij = Rij ≤ Dij , and thus, max(i,j)∈N \F (T̃ij −
Dij , 0) = 0. For (i, j) ∈ F , we have D̄ij ≤ Dij and the
following inequalities complete the proof.
s∗ ≤ max (T̃ij − Dij , 0) = max (T̃ij − Dij , 0)
(i,j)∈N

(i,j)∈F

≤ max (T̃ij − D̄ij , 0) = s∗U .
(i,j)∈F

Therefore, if s∗U = 0, we have s∗ = 0.
By Theorems 2 and 3, we have
s∗L > 0 ⇒ s∗ > 0 and s∗U = 0 ⇒ s∗ = 0.
That is, from Problems 3 and 4, which can be solved with a
commercial solver such as CPLEX, we can find the solution
for Problem 2 as shown in Table I. However, when s∗L = 0
and s∗U > 0, represented by Case II in the table, s∗ is not exactly determined. In this case, we will provide approximation
bounds.

C. Approximation bounds
We exactly solve Problem 2 in cases I and III as noted in
Table I, but have to approximate the solution in case II. In
this section, we will focus on the latter case when s∗L = 0 and
s∗U > 0 and quantify the approximation bounds. Notice that
s∗L > 0 and s∗U = 0 cannot occur.
We will prove the following statement: if s∗L = 0 and s∗U >
0, an input exists that makes the system avoid a shrunk bad
set but not an inflated bad set. These bad sets are defined
independent of time and thus we consider N = N̄ .
A shrunk conflict area and an inflated conflict area are
defined in the following definitions. See Figure 5.
Definition 4. A shrunk conflict area (α̂ij , β̂ij ) for all (i, j) ∈
N is defined as follows. For all (i, j) ∈ F ,
α̂ij = αij ,
β̂ij =

min xj

uj (·)∈Uj




βij − αij
, uj (·), αij , ẋj,min .
ẋj,max

(17)

For all (i, j) ∈ N \ F , there exists the first operation (i′ , j)
for i 6= i′ such that (i′ , j) ∈ F .


αij − αi′ j
′
, uj (·), αi j , ẋj,max ,
α̂ij = max xj
ẋj,min
uj (·)∈Uj


(18)
βij − αi′ j
, uj (·), αi′ j , ẋj,min .
β̂ij = min xj
ẋj,max
uj (·)∈Uj
If α̂ij ≥ β̂ij , set (α̂ij , β̂ij ) as an empty set.
Definition 5. An inflated conflict area (α̌ij , β̌ij ) for all (i, j) ∈
N is defined as follows. For all (i, j) ∈ F ,
α̌ij = αij , β̌ij = max xj (t∗ , uj (·), αij , ẋj,max ), (19)
uj (·)∈Uj

where t∗ = minuj (·)∈Uj {t : xj (t, uj (·), αij , ẋj,min ) = βij }
and αij = αj,min .
For all (i, j) ∈ N \ F ,
α̌ij =

min xj (t∗∗ , uj (·), αj,min , ẋj,min ),

uj (·)∈Uj

β̌ij = max xj (t∗∗∗ , uj (·), αj,min , ẋj,max ),

(20)

uj (·)∈Uj

where t∗∗ = minuj ∈Uj {t : xj (t, uj (·), αj,min , ẋj,max ) = αij }
and t∗∗∗ = minuj ∈Uj {t : xj (t, uj (·), αj,min , ẋj,min ) = βij }.
Notice that t∗ , t∗∗ , and t∗∗∗ are the same as the added times
in (11) and (12).
A shrunk bad set B̂ and an inflated bad set B̌ are defined
as follows:
B̂ := {x ∈ X : for some (i, j) ↔ (i, j ′ ) ∈ D
xj ∈ (α̂ij , β̂ij ) and xj ′ ∈ (α̂ij ′ , β̂ij ′ )}.

(21)

8

t*
(a)

(b)
(i′ , j)

t** t***

(c)

(d)

(i′ , j)

Fig. 5. Shrunk and Inflated conflict areas for
∈ F and
→ (i, j) ∈ C. Figures (a)-(d) illustrate (17)-(20), respectively. By definition,
(α̂i′ j , β̂i′ j ) ⊆ (αi′ j , βi′ j ) ⊆ (α̌i′ j , β̌i′ j ) and (α̂ij , β̂ij ) ⊆ (αij , βij ) ⊆ (α̌ij , β̌ij ).

B̌ := {x ∈ X : for some (i, j) ↔ (i, j ′ ) ∈ D
xj ∈ (α̌ij , β̌ij ) and xj ′ ∈ (α̌ij ′ , β̌ij ′ )}.

(22)

Similarly for any input u∗j (·) : [t∗i′ j , p∗ij ) → Uj ,
xj (p∗ij − t∗i′ j , u∗j (·), αi′ j , ẋj (t∗i′ j )) ≥ β̂ij .

It can be checked that

(26)

u∗j (·)

B̂ ⊆ B ⊆ B̌
by showing that (α̂ij , β̂ij ) ⊆ (αij , βij ) ⊆ (α̌ij , β̌ij ) for all
(i, j) ∈ N .
In the following theorems, we prove that the shrunk and
inflated bad sets can represent the approximation errors of the
solutions of Problems 3 and 4, respectively. More precisely,
we prove that 1) if the solution of Problem 3 is yes, that is,
s∗L = 0, then there exists an input that makes the system avoid
the shrunk bad set, and 2) if the solution of Problem 4 is no,
that is, s∗U > 0, then there is no input that makes the system
avoid the inflated bad set.
Theorem 4. Given an initial condition (x(0), ẋ(0)), if sL ∗ =
0, then there exists an input signal u(·) ∈ U such that
x(t, u(·), x(0), ẋ(0)) ∈
/ B̂ for all t ≥ 0.

Thus, there exists an input
∈ Uj that satisfies (23)-(26).
Now we will show that x(t, u∗ (·), x(0), ẋ(0)) ∈
/ B̂ for all
t ≥ 0. By (P3.3), we have for (i, j) ↔ (i, j ′ ) ∈ D either
p∗ij ≤ t∗ij ′ or p∗ij ′ ≤ t∗ij . Without loss of generality, we consider
p∗ij ≤ t∗ij ′ . Then, at time t∗ij ′ , vehicle j ′ has not yet entered
shrunk conflict area i as shown in (23) and (25). At the same
time, vehicle j has already exited the shrunk conflict area as
shown in (24) and (26). Thus, two vehicles never meet inside
the same shrunk conflict area, and thus the system avoids the
shrunk bad set with the input signal u∗ (·).
Theorem 5. Given an initial condition (x(0), ẋ(0)), if s∗U >
0, then for all input signal u(·) ∈ U, x(t, u(·), x(0), ẋ(0)) ∈ B̌
for some t ≥ 0.
Proof: We prove the contra-position: if there exists an
input signal u∗ (·) ∈ U such that x(t, u∗ (·), x(0), ẋ(0)) ∈
/ B̌
for all t ≥ 0, then s∗U = 0.
For all (i, j) ∈ N , let us define

Proof: If s∗L = 0, there exists an optimal solution t∗ , p∗
and k∗ that satisfies t∗ij ≤ dij for all (i, j) ∈ N and
constraints (P3.1)-(P3.3) in Problem 3.
For (i, j) ∈ F , rij ≤ t∗ij ≤ dij implies that there exists
∗
uj (·) : [0, t∗ij ) → Uj such that

if xj (0) < α̌ij . Otherwise, set Tij∗ = 0. Also, if xj (0) < β̌ij ,

xj (t∗ij , u∗j (·), xj (0), ẋj (0)) = αij = α̂ij

Pij∗ := {t : xj (t, u∗j (·), xj (0), ẋj (0)) = β̌ij }.

(23)

Tij∗ := {t : xj (t, u∗j (·), xj (0), ẋj (0)) = α̌ij },

since the flow of xj is a continuous function of u∗j (·) and the
input space is path connected by Assumption 1. Let ẋj (t∗ij )
denote ẋj (t∗ij , u∗j (·), xj (0), ẋj (0)). Constraint (P3.2), (βij −
αij )/ẋj,max ≤ p∗ij − t∗ij ≤ (βij − αij )/ẋj,min , implies that
for any input u∗j (·) : [t∗ij , p∗ij ) → Uj ,

Otherwise, set Pij∗ = 0.
Since x(t, u∗ (·), x(0), ẋ(0)) ∈
/ B̌ for all t ≥ 0, we have for
all (i, j) ↔ (i, j ′ ) ∈ D,

xj (p∗ij − t∗ij , u∗j (·), αij , ẋj (t∗ij )) ≥ β̂ij ,

which indicates that each inflated conflict area is occupied by
only one vehicle at a time.
Let us define a schedule T̃F = {T̃ijF : for all (i, j) ∈ F }
as follows: if xj (0) < αj,min ,

(24)

because β̂ij defined in (17) is the minimum distance from αij
traveled for time (βij − αij )/ẋj,max .
For (i, j) ∈ N \ F , there exists the first operation (i′ , j) ∈
F . By the definition of rij and dij in (8), we have
αij − αi′ j
αij − αi′ j
≤ rij ≤ t∗ij ≤ dij ≤ t∗i′ j +
.
t∗i′ j +
ẋj,max
ẋj,min
Since α̂ij is the maximum distance from αi′ j traveled for time
(αij − αi′ j )/ẋj,min , for any input u∗j (·) : [t∗i′ j , t∗ij ) → Uj ,
xj (t∗ij − t∗i′ j , u∗j (·), αi′ j , ẋj (t∗i′ j )) ≤ α̂ij .

(25)

(Tij∗ , Pij∗ ) ∩ (Tij∗ ′ , Pij∗ ′ ) = ∅,

(27)

T̃ijF := {t : xj (t, u∗j (·), xj (0), ẋj (0)) = αj,min }.
If αj,min ≤ xj (0), set T̃ijF = R̄ij . By Definition 2, T̃ijF ∈
[R̄ij , D̄ij ]. Thus, T̃F satisfies constraint (P4.1) and T̃ijF −
D̄ij ≤ 0 for all (i, j) ∈ F . If T̃F satisfies constraint (P4.2),
T̃F is a feasible solution to Problem 4 with a corresponding
binary variable k̃ = {k̃ijj ′ : for all (i, j) ↔ (i, j ′ ) ∈ D} and
thus s∗U = 0.

9

Given T̃F , T̄ = {T̄ij : for all (i, j) ∈ N } and P̄ = {P̄ij :
for all (i, j) ∈ N } are defined according to Definition 3.
First, consider xj (0) < αj,min . For (i, j) ∈ F , we have by
(11), T̄ij = T̃ijF and P̄ij = T̃ijF + t∗ where t∗ is introduced
in (19). Since α̌ij ≤ αj,min by definition, Tij∗ ≤ T̄ij . Also,
since β̌ij represents the maximum distance from αj,min that
vehicle j can travel during t∗ , traveling from αj,min to β̌ij
takes no less time than t∗ . Thus, P̄ij ≤ Pij∗ . For (i, j) ∈
N \ F , there exists (i′ , j) ∈ F . By (12), T̄ij = T̃iF′ j + t∗∗ and
P̄ij = T̃iF′ j + t∗∗∗ , where t∗∗ and t∗∗∗ are introduced in (20).
Since α̌ij and β̌ij are the minimum and maximum distance
traveled from αj,min for time t∗∗ and t∗∗∗ , respectively, we
have Tij∗ ≤ T̄ij and P̄ij ≤ Pij∗ .
Next, consider αj,min ≤ xj (0). In this case, R̄ij = D̄ij
for all vehicle j’s operations by (10) and thus for (i′ , j) ∈ F ,
we have T̃iF′ j = R̄i′ j . By (13), T̄i′ j = T̃iF′ j and P̄i′ j is the
minimum time to reach βij since T̃iF′ j − R̄i′ j = 0. The fact
that α̌ij ≤ αij and βij ≤ β̌ij implies Tij∗ ≤ T̄ij and P̄ij ≤ Pij∗ ,
respectively. For (i, j) ∈ N \ F , T̄ij and P̄ij are the minimum
time to reach αij and βij , respectively, starting from xj (0).
Since T̄ij ≥ (αij − xj (0))/ẋj,max and α̌ij is the minimum
distance traveled in (αij − xj (0))/ẋj,max , Tij∗ ≤ T̄ij . Also,
βij ≤ β̌ij implies P̄ij ≤ Pij∗ .
Therefore, (T̄ij , P̄ij ) ⊆ (Tij∗ , Pij∗ ) for all (i, j) ∈ N . By
(27), we derive (T̄ij , P̄ij ) ∩ (T̄ij ′ , P̄ij ′ ) = ∅ for all (i, j) ↔
(i, j ′ ) ∈ D. This is equivalent to constraint (P4.2), and thus
there exists k̃ijj ′ and k̃ij ′ j satisfying the constraint.
Therefore, T̃F and k̃ is a feasible solution with s∗U = 0.
By Theorem 4, if Problem 3 returns yes, there is an input
to make the system avoid the shrunk bad set. Otherwise, no
input exists to make the system avoid the bad set. Similarly
for Problem 4, if it returns yes, there is an input to make
the system avoid the bad set. Otherwise, no input exists to
avoid the inflated bad set by Theorem 5. Thus, the shrunk and
inflated bad sets represent the over-approximation and underapproximation of the reachable set from an initial condition
(x(0), ẋ(0)), respectively.

A PPROX V ERIFICATION return (s∗U , TF ∗ ) where TF ∗ is the
optimal solution.
The supervisory algorithm runs in discrete time with a time
step τ . At time kτ , it receives the measurements of the state
(x(kτ ), ẋ(kτ )) and the desired input ukd ∈ U, which is a
vector of inputs that the drivers are applying at the time. These
measurements are used to predict the desired state at the next
time step, which is denoted by (xkd , ẋkd ). We solve Problem 4
to see if the desired state has a safe input signal within the
approximation bound.
If A PPROX V ERIFICATION (xkd , ẋkd ) returns TF ∗ that makes
∗
sU = 0, we can find a safe input signal by defining an input
generator function σ : X × Ẋ × Rn → U as follows:
σ(xkd , ẋkd , TF ∗ ) ∈ {u(·) ∈ U : for all (i, j) ∈ F ,
xj (TijF ∗ , uj (·), xkj,d , ẋkj,d ) = αij and uj (t) = uj,max ∀ t ≥ TijF ∗},
where xkj,d and ẋkj,d denote the j-th entries of xkd and ẋkd ,
respectively. The supervisor stores this safe input restricted to
time (0, τ ) for a possible use at the next time step. Since there
is an input signal that makes the system avoid entering the bad
set from (xkd , ẋkd ), the supervisor allows the desired input.
If A PPROX V ERIFICATION (xkd , ẋkd ) returns s∗U > 0, the
supervisor overrides the drivers with the safe input stored at
the previous step. This safe input is used to predict the safe
state, denoted by (xksaf e , ẋksaf e ), and this safe state is used to
generate a safe input for the next time step. We will prove in
the next theorem that A PPROX V ERIFICATION (xksaf e , ẋksaf e )
always returns s∗U = 0 and thus a safe input signal is defined.
This supervisor is provided in Algorithm 1. An input signal
with superscript k, such as uk (·), denotes an input function
from [0, τ ) to U. We define the desired input signal as ukd (·) :
t 7→ ukd given ukd ∈ U. Also, an input signal with superscript
k, ∞ indicates that the domain of the input signal is [0, ∞).
Algorithm 1 Supervisory control algorithm at t = kτ
1:
2:
3:
4:

D. Other upper bound solutions

5:

In Section V-B, we formulate an MILP problem that yields
an upper bound by considering the maximum input inside
an intersection. Different MILP formulations are possible, for
example, by considering the minimum input inside an intersection. To obtain a tighter upper bound, various combinations of
the maximum and minimum inputs can be considered inside
an intersection with a binary variable associated with each
combination. At the expense of computational complexity, this
approach is less conservative since more choices of inputs are
allowed.

6:
7:
8:
9:
10:
11:
12:
13:
14:
15:

VI. C ONTROL

procedure S UPERVISOR(x(kτ ), ẋ(kτ ), ukd )
xkd ← x(τ, ukd (·), x(kτ ), ẋ(kτ ))
ẋkd ← ẋ(τ, ukd (·), x(kτ ), ẋ(kτ ))
∗
k
k
(s∗U , TF
1 ) = A PPROX V ERIFICATION (xd , ẋd )
∗
if sU = 0 then
k
k
F∗
uk+1,∞
saf e (·) ← σ(xd , ẋd , T1 )
k+1,∞
uk+1
saf e (·) ← usaf e (t) for t ∈ [0, τ )
return ukd (·)
else
xksaf e ← x(τ, uksaf e (·), x(kτ ), ẋ(kτ ))
ẋksaf e ← ẋ(τ, uksaf e (·), x(kτ ), ẋ(kτ ))
∗
k
k
(·, TF
2 ) = A PPROX V ERIFICATION (xsaf e , ẋsaf e )
k+1,∞
∗
usaf e (·) ← σ(xksaf e , ẋksaf e , TF
2 )
k+1,∞
k+1
usaf e (·) ← usaf e (t) for t ∈ [0, τ )
return uksaf e (·)

DESIGN

Based on the results of Section V, we can design a supervisor that is activated when a future collision is detected inside
the inflated conflict areas.
Let A PPROX V ERIFICATION(x(0), ẋ(0)) be an algorithm
solving Problem 4 given an initial condition (x(0), ẋ(0)). Let

By Theorem 5, s∗U > 0 indicates that no input signal
exists to avoid the inflated bad set, that is, there may exist
an input to avoid the bad set. Thus, we say this supervisor
overrides vehicles when a future collision is detected within
the approximation bound.

10

Theorem 6. Algorithm 1 is non-blocking, that is, if
S UPERVISOR (x(0), ẋ(0), u0d ) 6= ∅, then for any ukd ∈ U,
S UPERVISOR (x(kτ ), ẋ(kτ ), ukd ) 6= ∅.
Proof: We prove this by induction on k. For the base
1,∞
case, assume S UPERVISOR (x(0), ẋ(0), u0d ) 6= ∅ and usaf
e (·)
1,∞
is well-defined, that is, usaf e (·) ∈ U. Suppose at time (k −
1)τ , S UPERVISOR(x((k − 1)τ ), ẋ((k − 1)τ ), udk−1 ) is nonk
empty and uk,∞
saf e is well-defined. At time kτ , for any ud ∈ U,
k
S UPERVISOR (x(kτ ), ẋ(kτ ), ud ) is not empty since it returns
either ukd (·) : t 7→ ukd or uksaf e (·) : t 7→ uk,∞
saf e (t). We need to
show that uk+1,∞
(·)
is
well-defined
in
lines
6 or 13.
saf e
∗
F∗
In line 6, since TF
=
{T
:
(i,
j)
∈
F
}
yields s∗U = 0,
1
ij,1
F∗
we have R̄ij ≤ Tij,1 ≤ D̄ij for all (i, j) ∈ F and thus there
F∗
exists uj (·) ∈ Uj that satisfies xj (Tij,1
, uj (·), xkj,d , ẋkj,d ) =
∗
αij . Thus, σ(xkd , ẋkd , TF
1 ) is well-defined.
∗
In line 13, we will show that TF
satisfies s∗U = 0
2
and thus a safe input signal is well-defined. We have that
k−1
k−1
(x(kτ ), ẋ(kτ )) is either (xdk−1 , ẋdk−1 ) or (xsaf
e , ẋsaf e ) depending on the output of the supervisor at the previous
time step. Thus, at time (k − 1)τ , A PPROX V ERIFICA TION (x(kτ ), ẋ(kτ )) yielded s∗
U = 0 with an optimal solution
k−1
k−1
TF ,k−1 = {TijF ,k−1 : (i, j) ∈ F }. Let R̄ij
, D̄ij
, T̄ijk−1 ,
k−1
and P̄ij be the parameters used in the problem. Now, consider A PPROX V ERIFICATION(xksaf e , ẋksaf e ) with parameters
k
k
R̄ij
, D̄ij
, T̄ijk , and P̄ijk . If we define T̃ijF = TijF ,k−1 − τ for
k
k
] since TijF ,k−1 ∈
, D̄ij
all (i, j) ∈ F , we have T̃ijF ∈ [R̄ij
k−1
k−1
k
[R̄ij , D̄ij ] and usaf e (·) is in U. Also, since (T̄ijk , P̄ijk ) ⊆
(T̄ijk−1 , P̄ijk−1 ) − τ and (T̄ijk−1 , P̄ijk−1 ) ∩ (T̄ijk−1
, P̄ijk−1
) = ∅ for
′
′
k
′
k
all (i, j) ↔ (i, j ) ∈ D, we have (T̄ij , P̄ij ) ∩ (T̄ijk ′ , P̄ijk ′ ) = ∅.
Therefore, T̃F = {T̃ijF : for all (i, j) ∈ F } is a feasible solution that yields s∗U = 0, and thus there exists the optimal solu∗
F∗
∗
tion TF
2 satisfying sU = 0. Therefore, σ(xsaf e , ẋsaf e , T2 )
is well-defined.
VII. S IMULATION R ESULTS
We implemented Algorithm 1 on the cases illustrated in
Figures 1 and 2 to validate its collision avoidance performance
and its non-blocking property. We implemented the algorithm
on MATLAB and performed simulations on a personal computer consisting of an Intel Core i7 processor at 3.10 GHz and
8 GB RAM.
In the simulations, we consider the vehicle dynamics with
a quadratic drag term [44] as follows: for all j ∈ {1, . . . , n}
ẍj = auj + bẋ2j .
Also, the following parameters are used: τ = 0.1, a =
1, b = 0.005. For all j ∈ {1, . . . , n}, uj,max = 2, uj,min =
−2, αj,min = 20. For all (i, j) ∈ N , βij − αij = 5 and for all
(i, j) → (i′ , j) ∈ C, αi′ j − αij = 6.
Let us consider the scenario illustrated in Figure 2 with
the following initial condition and parameters: x(0) =
(0, 0, 0), ẋ(0) = (10, 8, 8), and ẋj,min = 8, ẋj,max = 10
for all j ∈ {1 . . . , n}. Without implementing the supervisor
(Algorithm 1), we let the vehicles travel with the desired input
ukd = (−2, −2, 2) for all k and plot the optimal values of

Fig. 6.
Simulation results without the supervisor (Algorithm 1) for the
scenario in Figure 2. Cases I, II, and III denote the same cases in Table I.

Problems 3 and 4. These are shown in Figure 6. As proved
in Theorems 2 and 3, s∗U = 0 implies s∗L = 0. The trajectory
of the system with implementing the supervisor is shown in
Figure 7(a)-(c). The trajectory (black line) is controlled by the
supervisor when s∗U > 0 (the line is thicker in blue) so that
it avoids the bad set (solid in (b)). Notice that the trajectory
penetrates the inflated bad set (solid in (a)) but not the shrunk
bad set (solid in (c)) as proved in Theorems 4 and 5.
Now, let us consider the scenario illustrated in Figure 1
with the following initial condition and parameters: x(0) =
(0, −2, 5, −5, 0, 5, 0, 1, 5, 4, 0, −2, 5, 5, 0, 5, −2, 0, −2, 0) and
for all j ∈ {1, . . . , n}, ẋj (0) = 5, ẋj,min = 1, ẋj,max = 10.
With the desired input ukd = umax for all k, the result
is shown in Figure 8. The trajectory of vehicle 1 (black
line) and the trajectories of other vehicles that share the
same conflict area (red dotted lines) never stay inside the
conflict area simultaneously. This implies that the supervisor
overrides vehicles when necessary (when blue boxes appear) to
make them cross the intersection without collisions. Because
unnecessary to prove optimality, solving feasibility problems
requires less computational effort than solving optimization
problems [43]. That is, solving the following problem takes
less computation time than solving Problem 4: given an initial
condition, determine if there exists a feasible solution (TF , k)
that satisfies (P4.1), (P4.2), and TijF ≤ D̄ij for all (i, j) ∈ F .
Notice that this problem is equivalent to Problem 4. Based
on the solution of this feasibility problem, Algorithm 1 takes
no more than 0.05 s per iteration, even in this realistic size
scenario involving 20 vehicles, 48 conflict areas, and 120 operations on a representative geometry of dangerous intersections.
Given that the allocated time step for intelligent transportation
systems is 0.1 s [2], this algorithm can be implemented in real
time.
VIII. C ONCLUSIONS
In this paper, we presented the design of a supervisory algorithm that determines the existence of a future collision among
vehicles at an intersection (safety verification) and overrides
the drivers with a safe input if a future collision is detected

11

(a) Inflated bad set B̌

(b) Bad set B

(c) Shrunk bad set B̂

Fig. 7. Simulation results with the supervisor for the scenario in Figure 2. The black line represents the system trajectory and is the same on each figure.
The line turns to blue when the supervisor intervenes to prevent a predicted collision. The solid in each figure is (a) the inflated bad set, (b) the bad set, and
(c) the shrunk bad set. The supervisor manages the system to avoid entering the bad set.

While we assumed in this paper that there is only one
vehicle per lane, our approach can be easily modified to deal
with the case in which multiple vehicles are present on each
lane. One possible modification can be solving the scheduling
problem only for the first vehicles on lanes while letting the
following vehicles maintain a safe distance from their front
vehicles. Instead of this naive approach, we are currently investigating a less conservative approach. Also, Problem 4 can be
extended to include the presence of uncertainty sources, such
as measurement noises, process errors, and not communicating
vehicles, as done in our previous works [18], [19] for the single
conflict area intersection model. Also, in future work, the
assumption that the routes of vehicles are known in advance
will be relaxed.
Fig. 8. Trajectory of vehicle 1 in the scenario of Figure 1 crossing six conflict
areas. The blue boxes represent the times at which the supervisor overrides
the vehicles. The red dotted lines are the trajectories of the other vehicles that
share the same conflict area. This graph shows that each conflict area is used
by only one vehicle at a time.

(control design). We translated the safety verification problem
into a scheduling problem by exploiting monotonicity of the
system. This scheduling problem minimizes the maximum
lateness and determines if the optimal cost is zero where the
zero optimal cost corresponds to the case in which all vehicles
can cross the intersection without collisions. Because of the
nonlinear second-order dynamics of vehicles, the scheduling
problem is a Mixed Integer Nonlinear Programming (MINLP)
problem, which is computationally difficult to solve. We thus
approximately solved this scheduling problem by solving two
Mixed Integer Linear Programming (MILP) problems that
yield lower and upper bounds of the optimal cost of the
scheduling problem. We quantified the approximation error
between the exact and approximate solutions to the scheduling
problem. We presented the design of the supervisor based on
the MILP problem that computes the upper bound and proved
that it is non-blocking. Computer simulations validated that
the supervisor can be implemented in real time applications.

R EFERENCES

[1] E. Ackerman, “Fatal Tesla self-driving car crash reminds us
that robots aren’t perfect,” Jul. 2016. [Online]. Available:
http://spectrum.ieee.org/cars-that-think/transportation/self-driving/fatal-tesla-autopilot-c
[2] U.S. Department of Transportation, “ITS Strategic research plan 20152019,” http://www.its.dot.gov/strategicplan.pdf, 2014.
[3] C. Tomlin, G. J. Pappas, and S. Sastry, “Conflict resolution for air traffic
management: a study in multiagent hybrid systems,” IEEE Transactions
on Automatic Control, vol. 43, no. 4, pp. 509–521, Apr. 1998.
[4] C. Tomlin, J. Lygeros, and S. Sastry, “A game theoretic approach to
controller design for hybrid systems,” Proceedings of the IEEE, vol. 88,
no. 7, pp. 949–970, Jul. 2000.
[5] J. Lygeros, C. Tomlin, and S. Sastry, “Controllers for reachability
specifications for hybrid systems,” Automatica, vol. 35, no. 3, pp. 349–
370, Mar. 1999.
[6] T. A. Henzinger, P.-H. Ho, and H. Wong-Toi, “Algorithmic analysis of
nonlinear hybrid systems,” IEEE Transactions on Automatic Control,
vol. 43, no. 4, pp. 540–554, Apr. 1998.
[7] R. Alur, T. Dang, and F. Ivani, “Predicate abstraction for reachability
analysis of hybrid systems,” ACM Transactions on Embedded Computing
Systems, vol. 5, no. 1, pp. 152–199, Feb. 2006.
[8] A. Girard, A. A. Julius, and G. J. Pappas, “Approximate simulation
relations for hybrid systems,” Discrete Event Dynamic Systems, vol. 18,
no. 2, pp. 163–179, Oct. 2007.
[9] E. Asarin, O. Bournez, T. Dang, and O. Maler, “Approximate reachability analysis of piecewise-linear dynamical systems,” in Hybrid Systems:
Computation and Control. Springer, Mar. 2000, no. 1790, pp. 20–31.
[10] P. Gagarinov and A. A. Kurzhanskiy, “Ellipsoidal Toolbox,” 2014. [Online]. Available: http://systemanalysisdpt-cmc-msu.github.io/ellipsoids/
[11] T. Dreossi, T. Dang, and C. Piazza, “Parallelotope bundles for polynomial reachability,” in Proc. 19th International Conference on Hybrid
Systems: Computation and Control (HSCC). ACM, 2016, pp. 297–306.

12

[12] T. Moor and J. Raisch, “Abstraction based supervisory controller syntheApproach,” IEEE Transactions on Intelligent Transportation Systems,
sis for high order monotone continuous systems,” in Modelling, Analysis,
vol. 12, no. 1, pp. 47–57, Mar. 2011.
and Design of Hybrid Systems. Springer, 2002, no. 279, pp. 247–265.
[35] A. Alonso-Ayuso, L. F. Escudero, and F. J. Martn-Campo, “On modeling
[13] D. Del Vecchio, M. Malisoff, and R. Verma, “A separation principle
the air traffic control coordination in the collision avoidance problem by
for a class of hybrid automata on a partial order,” in Proc. American
mixed integer linear optimization,” Annals of Operations Research, vol.
Control Conference (ACC), 2009, pp. 3638–3643.
222, no. 1, pp. 89–105, Mar. 2013.
[14] M. R. Hafner and D. Del Vecchio, “Computational tools for the safety
[36] J. Omer, “A space-discretized mixed-integer linear model for air-conflict
control of a class of piecewise continuous systems with imperfect inforresolution with speed and heading maneuvers,” Computers & Operations
mation on a partial order,” SIAM Journal on Control and Optimization,
Research, vol. 58, pp. 75–86, Jun. 2015.
vol. 49, pp. 2463–2493, 2011.
[37] M. Soler, M. Kamgarpour, J. Lloret, and J. Lygeros, “A hybrid optimal
[15] Massachusetts
Department
of
Transportation,
“2012
Top
control approach to fuel-efficient aircraft conflict avoidance,” IEEE
Crash
Locations
Report,”
2014.
[Online].
Available:
Transactions on Intelligent Transportation Systems, vol. 17, no. 7, pp.
https://www.massdot.state.ma.us/Portals/8/docs/traffic/CrashData/12TopCrashLocationsRpt.pdf
1826–1838, Jul. 2016.
[16] A. Colombo and D. Del Vecchio, “Efficient algorithms for collision
[38] W. Chen, J. Chen, Z. Shao, and L. T. Biegler, “Three-dimensional
avoidance at intersections,” in Proc. 15th international conference on
aircraft conflict resolution based on smoothing methods,” Journal of
Hybrid Systems: Computation and Control (HSCC). ACM, 2012, pp.
Guidance, Control, and Dynamics, vol. 39, no. 7, pp. 1481–1490, 2016.
145–154.
[39] L. Pallottino, V. Scordio, A. Bicchi, and E. Frazzoli, “Decentralized
[17] ——, “Least restrictive supervisors for intersection collision avoidance:
Cooperative Policy for Conflict Resolution in Multivehicle Systems,”
A scheduling approach,” IEEE Transactions on Automatic Control, 2014.
IEEE Transactions on Robotics, vol. 23, no. 6, pp. 1170–1183, Dec.
[18] L. Bruni, A. Colombo, and D. Del Vecchio, “Robust multi-agent
2007.
collision avoidance through scheduling,” in Proc. IEEE Conference on
[40] T. Keviczky, F. Borrelli, K. Fregene, D. Godbole, and G. J. Balas,
Decision and Control (CDC), Dec. 2013, pp. 3944–3950.
“Decentralized receding horizon control and coordination of autonomous
[19] H. Ahn, A. Colombo, and D. Del Vecchio, “Supervisory control for invehicle formations,” IEEE Transactions on Control Systems Technology,
tersection collision avoidance in the presence of uncontrolled vehicles,”
vol. 16, no. 1, pp. 19–33, 2008.
in Proc. American Control Conference (ACC), Jun. 2014, pp. 867–873.
[41] W. Zhang, M. Kamgarpour, D. Sun, and C. J. Tomlin, “A hierarchical
[20] H. Ahn, A. Rizzi, A. Colombo, and D. Del Vecchio, “Experimental testflight planning framework for air traffic management,” Proceedings of
ing of a semi-autonomous multi-vehicle collision avoidance algorithm
the IEEE, vol. 100, no. 1, pp. 179–194, Jan. 2012.
at an intersection testbed,” in Proc. IEEE/RSJ International Conference
[42] M. Pinedo, Scheduling, 4th ed. Springer, 2012.
on Intelligent Robots and Systems (IROS), Sep. 2015, pp. 4834–4839.
[43] IBM Corporation, “CPLEX User’s Manual,” 2015. [Online]. Available:
[21] H. Ahn and D. Del Vecchio, “Semi-autonomous intersection collision
http://www.ibm.com/support/knowledgecenter/SSSA5P 12.6.3/ilog.odms.studio.help/pd
avoidance through job-shop scheduling,” in Proc. 19th International
[44] M. Hafner, D. Cunningham, L. Caminiti, and D. Del Vecchio, “CooperConference on Hybrid Systems: Computation and Control (HSCC).
ative collision avoidance at intersections: algorithms and experiments,”
ACM, Apr. 2016, pp. 185–194.
IEEE Transactions on Intelligent Transportation Systems, vol. 14, no. 3,
[22] J. Peng and S. Akella, “Coordinating Multiple Double Integrator Robots
pp. 1162–1175, 2013.
on a Roadmap: Convexity and Global Optimality,” in Proc. IEEE
International Conference on Robotics and Automation (ICRA), Apr.
2005, pp. 2751–2758.
[23] ——, “Coordinating multiple robots with kinodynamic constraints along
specified paths,” The International Journal of Robotics Research, vol. 24,
no. 4, pp. 295–310, Apr. 2005.
[24] K.-D. Kim and P. Kumar, “An MPC-based approach to provable systemwide safety and liveness of autonomous ground traffic,” IEEE Transactions on Automatic Control, vol. 59, no. 12, pp. 3341–3356, Dec. 2014.
[25] M. Kamal, J. Imura, T. Hayakawa, A. Ohata, and K. Aihara, “A VehicleIntersection Coordination Scheme for Smooth Flows of Traffic Without
Using Traffic Lights,” IEEE Transactions on Intelligent Transportation
Systems, 2014.
[26] F. Zhu and S. V. Ukkusuri, “A linear programming formulation for
autonomous intersection control within a dynamic traffic assignment
and connected vehicle environment,” Transportation Research Part C:
Emerging Technologies, vol. 55, pp. 363–378, Jun. 2015.
[27] N. Murgovski, G. R. de Campos, and J. Sjöberg, “Convex modeling of
conflict resolution at traffic intersections,” in Proc. IEEE Conference on
Decision and Control (CDC), Dec. 2015, pp. 4708–4713.
[28] L. Chen and C. Englund, “Cooperative intersection management: A survey,” IEEE Transactions on Intelligent Transportation Systems, vol. 17,
no. 2, pp. 570–586, Feb 2016.
[29] R. Tachet, P. Santi, S. Sobolevsky, L. I. Reyes-Castro, E. Frazzoli,
D. Helbing, and C. Ratti, “Revisiting street intersections using slot-based
systems,” PLoS ONE, vol. 11, no. 3, p. e0149607, Mar. 2016.
[30] F. Altché, X. Qian, and A. de La Fortelle, “Time-optimal coordination
of mobile robots along specified paths,” 2016. [Online]. Available:
http://arxiv.org/abs/1603.04610
[31] A. Richards, T. Schouwenaars, J. P. How, and E. Feron, “Spacecraft
Trajectory Planning with Avoidance Constraints Using Mixed-Integer
Linear Programming,” Journal of Guidance, Control, and Dynamics,
vol. 25, no. 4, pp. 755–764, 2002.
[32] L. Pallottino, E. Feron, and A. Bicchi, “Conflict resolution problems
for air traffic management systems solved with mixed integer programming,” IEEE Transactions on Intelligent Transportation Systems, vol. 3,
no. 1, pp. 3–11, Mar. 2002.
[33] A. E. Vela, S. Solak, J. P. B. Clarke, W. E. Singhose, E. R. Barnes, and
E. L. Johnson, “Near real-time fuel-optimal en route conflict resolution,”
IEEE Transactions on Intelligent Transportation Systems, vol. 11, no. 4,
pp. 826–837, Dec. 2010.
[34] A. Alonso-Ayuso, L. Escudero, and F. Martn-Campo, “Collision Avoidance in Air Traffic Management: A Mixed-Integer Linear Optimization

