1

Hierarchical decomposition of LTL synthesis
problem for mixed-monotone control systems

arXiv:1712.06014v1 [cs.SY] 16 Dec 2017

Pierre-Jean Meyer, Dimos V. Dimarogonas

Abstract—This paper deals with the control synthesis problem
for a continuous nonlinear dynamical system under a Linear
Temporal Logic (LTL) formula. The proposed solution is a topdown hierarchical decomposition of the control problem involving
three abstraction layers of the problem, iteratively solved from
the coarsest to the finest. The LTL planning is first solved on
a small transition system only describing the regions of interest
involved in the LTL formula. For each pair of consecutive regions
of interest in the resulting accepting path satisfying the LTL
formula, a discrete plan is then constructed in the partitioned
workspace to connect these two regions while avoiding unsafe
regions. Finally, an abstraction refinement approach is applied
to synthesize a controller for the dynamical system to follow
each discrete plan. The first two steps let us find a discrete
plan satisfying the LTL formula with reduced computation need,
even for large workspaces. The second main contribution, used
in the third abstraction layer, is the extension of finite-time
reachability analysis based on the monotonicity property to any
(non-monotone) continuously differentiable system, at the cost
of an increased conservativeness. The proposed framework is
demonstrated in simulation for a motion planning problem of a
mobile robot modeled as a unicycle.
Index Terms—Hierarchical decomposition, LTL planning,
abstraction-based synthesis, mixed-monotone systems, reachability analysis.

I. I NTRODUCTION
Control synthesis and planning for continuous dynamical
systems under high-level specifications, such as Linear Temporal Logic (LTL) formulas [2], usually cannot be solved directly
on the continuous dynamics. The classical solutions to this
problem thus rely on a two-step approach, where we first
create a finite abstraction (the abstract or symbolic model)
of the continuous dynamical system (the concrete model),
and then leverage formal methods from the field of computer
science to synthesize a controller for the abstraction to satisfy
the high-level specifications. Provided that the abstraction was
created to obtain some behavioral relationship (such as (approximate) alternating simulation [25] or feedback refinement
relation [21]) between the concrete and abstract models, the
controller obtained on the abstraction can then be concretized
into a controller for the concrete model to satisfy the desired
specifications.
This work was supported by the H2020 ERC Starting Grant BUCOPHSYS,
the EU H2020 AEROWORKS project, the EU H2020 Co4Robots project, the
Swedish Foundation for Strategic Research, the Swedish Research Council
and the KAW Foundation.
P.-J. Meyer is with the Department of Electrical Engineering and Computer
Sciences at University of California, Berkeley, CA 94720-1770, USA (email:
pjmeyer@berkeley.edu).
D. V. Dimarogonas is with the Department of Automatic Control at
KTH Royal Institute of Technology, 10044 Stockholm, Sweden (email:
dimos@kth.se).

This topic recently received significant interest resulting in
various abstraction methods such as designing local feedback
controllers between any two neighboring cells of a state
space partition to guarantee the creation of a deterministic
abstraction [10], [4], considering infinite-time reachability
analysis of neighboring cells [20], [29], or fixed and finite-time
reachability analysis [5], [21], which we consider in this paper.
While the combined results of all these approaches cover
a wide range of dynamical systems and control objectives,
when taken separately most of these approaches (as well as
others in the literature) are restricted to particular classes
of systems (e.g. multi-affine [10], mixed-monotone [5]) and
subsets of LTL formulas (e.g. reach-avoid-stay [20], [29],
co-safe LTL [10]). However, providing a framework capable
of solving the synthesis problem for any dynamical systems
under general LTL formulas remains a challenging problem.
This can particularly be observed when considering the
main software toolboxes in the literature aimed at addressing
such high-level control problems on dynamical systems, which
can be split in two categories. On one side are tools such as
TuLiP [28], conPAS2 [26] and LTLMoP [9] which can handle
general LTL specifications (conPAS2) or the large subset of
GR(1) formulas (TuLiP, LTLMoP) but are restricted to simpler
dynamical systems such as fully actuated (LTLMoP) and
piecewise affine models (TuLiP, conPAS2). On the other side,
more general switched or nonlinear dynamical systems can
be considered by tools such as PESSOA [14], CoSyMa [19]
and SCOTS [22], but only for limited specifications combining
safety and reachability objectives.
To overcome these limitations, in this paper we propose a 3layer hierarchical decomposition of the control problem aimed
at addressing general control synthesis for nonlinear dynamical
systems under LTL specifications. As opposed to the 2-step
bottom-up symbolic control approach presented above which
starts by computing an abstraction of the dynamical system
before synthesizing a controller on this abstraction, we rather
take inspiration from top-down hierarchical decomposition in
the field of artificial intelligence [23]. In this approach, we
have several granularities of abstraction of the control problem
and we first solve the problem on the most abstract layer, then
iteratively refine this result by going down to a more detailed
layer where we solve a new problem consisting of realizing
the solution of the above layer. Given an initial partition of
the state space (possibly containing unsafe regions) and an
LTL formula defined over a set of regions of interest, each
corresponding to a single cell of this partition, the proposed
hierarchical decomposition proceeds to the following three
steps.

2

1) Solve the LTL planning problem on a finite transition
system that only represents the regions of interest, and
obtain a resulting (possibly infinite) sequence of regions
to visit.
2) For each pair of consecutive regions in this sequence, find
a discrete plan in the partitioned state space connecting
both regions of interest in the considered pair while
avoiding unsafe regions.
3) Compute an abstraction of the dynamical system using
an abstraction refinement approach [17] to synthesize a
controller for the dynamical system to follow each of the
above discrete plans in a sampled-time manner.
The first two layers can easily be solved by classical
methods for LTL model checking on finite systems [2] and
graph searches [7], respectively. As mentioned above, the
considered abstraction method in the third step relies on the
finite-time reachability analysis of the dynamical system to
compute the non-deterministic transitions of the abstraction. In
this paper, we focus on the use of a generalized monotonicity property [24] for the reachability analysis of dynamical
systems which are not monotone. A first abstraction-based
control approach relying on the monotonicity property was
introduced in [18] for monotone systems. This approach was
then extended in [5] for the larger class of mixed-monotone
systems, which do not satisfy the monotonicity property but
can be decomposed into their increasing and decreasing components defining a monotone decomposition function. Based
on the initial results in [30] introduced for another type
of abstraction [29], we further extend the use of monotone
decomposition functions to the finite-time reachability analysis
for any continuously differentiable nonlinear system, thus
opening the use of monotonicity-based abstraction approaches
to any such system.
To further compare the proposed approach with the previously mentioned works, we can first note that the introduction of the intermediate layer in our hierarchical decomposition allows the consideration of more general control
objectives than PESSOA [14], CoSyMa [19] or SCOTS [22]
by translating a general LTL specification into a sequence of
reachability problems. In addition, the new contribution on
monotonicity-based reachability analysis for any continuously
differentiable nonlinear system opens this approach to a much
wider class of systems than those considered in TuLiP [28],
conPAS2 [26] and LTLMoP [9]. Regarding other tools also
covering nonlinear systems, it should be noted that PESSOA [14] does not natively handle those systems and requires
the user to manually provide a Matlab function computing
an over-approximation of the reachable set, while an overapproximation method is included by default in our approach.
The consideration of nonlinear systems in CoSyMa [19] is
based on an incremental stability assumption, which is relaxed
in this paper. Finally, SCOTS [22] simply uses a different
over-approximation method based on Lipschitz arguments to
create a growth bound on the nonlinear system’s reachable set.
Although we compare our contributions to existing tools and
software as they are good indicators of the generality of results
that can be covered in the field of symbolic control, this paper

mainly focuses on providing the initial theoretical results and
structure for a possible future development of a general and
fully reusable tool.
Among other relevant work, 2-layer top-down structures are
proposed in [13], [27] for fully actuated and piecewise affine
systems respectively, where the first layer of the present paper
is skipped to look directly for a discrete plan satisfying the
LTL formula in the partitioned environment, then a continuous
controller is designed to realize this discrete plan. Similarly,
the 3-layer top-down decomposition mentioned in [3] also
skips the first layer but splits the second one in two components: first finding all discrete plans satisfying the LTL
formula in the partitioned environment without obstacle, then
picking one of these plans based on optimization and obstacle
avoidance criteria. The third layer in [3] uses a deterministic
abstraction approach similar to [10] to implement this discrete
plan on a robot modeled by an affine system. Another 3-step
hierarchical decomposition of an LTL control problem is also
presented in [8], but for a bottom-up decomposition whose
steps are significantly different from our approach as they
consist in first abstracting the dynamical system into a fully
actuated model (similarly to our second step), then robustifying the specification to compensate for the mismatches with
the initial system and finally solving the new LTL problem on
the robust specification.
This paper is structured as follows. In Section II, we
provide preliminary definitions and properties related to the
monotonicity properties and we then present our first main
contribution on the monotonicity-based over-approximation of
the reachable set for any continuously differentiable nonlinear
system. Section III formulates the control problem and gives
an overview of our second main contribution: a 3-layer hierarchical decomposition to solve LTL control problems on
nonlinear dynamical systems. A more detailed algorithmic
description of the third step of this solution on abstraction
refinement is then provided in Section IV. Finally, Section V
presents a numerical implementation of the proposed approach
to a motion planning problem for a unicycle robot.
II. R EACHABILITY ANALYSIS OF NON - MONOTONE
SYSTEMS

R+
0

R−
0

Let N, R,
and
be the sets of positive integers,
reals, non-negative reals and non-positive reals, respectively.
For a, b ∈ Rn , the interval [a, b] ⊆ Rn is defined as
[a, b] = {z ∈ Rn | a ≤ z ≤ b} using componentwise
inequalities.
A. System description
We consider a class of continuous-time nonlinear control
systems subject to disturbances and modeled by:
ż = f (z, u, d),

(1)

where z ∈ Z ⊆ Rn , u ∈ U ⊆ Rp and d ∈ D ⊆ Rq
are the state, bounded control input and bounded disturbance
input, respectively. Throughout this paper, the vector field f
of (1) is assumed to be continuously differentiable. We denote
as Φf (t, z, u, d) the state (assumed to exist and be unique)

3

reached by (1) at time t ∈ R+
0 from initial state z ∈ Z, under
the piecewise continuous control u : R+
0 → U and disturbance
functions d : R+
0 → D. We use Φf (t, z, u, d) with u ∈ U and
d ∈ D in the case of constant input functions u : R+
0 → {u}
and d : R+
0 → {d}.
For a sampling period τ ∈ R+
0 whose value is discussed
in Section III-C, a sampled version of system (1) can be
described as a non-deterministic (due to the disturbance)
infinite transition system Sτ = (Xτ , Uτ , δτ ) where
• Xτ = Z is the set of states,
• Uτ = U is the set of control inputs,
• the transition relation δτ : Xτ × Uτ → Xτ is such that
z 0 ∈ δτ (z, u) if there exists a disturbance d : [0, τ ] → D
such that z 0 = Φf (τ, z, u, d), i.e. z 0 can be reached from
z exactly in time τ by applying the constant control u on
[0, τ ].
B. Monotonicity
Monotone systems are commonly described as systems
whose trajectories preserve some partial orders as below. A
formal definition of a partial order is omitted in this paper but
can be found in [1].
Definition 1. System (1) is monotone with respect to partial
orders z , u and d on the state, control and disturbance
inputs respectively, if for all time t ∈ R+
0 , initial states
z, z 0 ∈ Z, control functions u, u0 : [0, t] → U and disturbance
functions d, d0 : [0, t] → D we have
z z z 0 , u u u0 , d d d0
⇒ Φf (t, z, u, d) z Φf (t, z 0 , u0 , d0 ).
For systems (1) with a continuously differentiable vector
field f , a sufficient condition for a system to be monotone is
as follows [1].
Proposition 2. System (1) is monotone if there exists
(εz1 , . . . , εzn ) ∈ {0, 1}n , (εu1 , . . . , εup ) ∈ {0, 1}p and
(εd1 , . . . , εdq ) ∈ {0, 1}q such that for all z ∈ Z ⊆ Rn ,
u ∈ U ⊆ Rp and d ∈ D ⊆ Rq we have:
z
z ∂fi
(z, u, d) ≥ 0, ∀i, j ∈ {1, . . . , n}, i 6= j,
(−1)εi +εj
∂zj
z
u ∂fi
(−1)εi +εk
(z, u, d) ≥ 0, ∀i ∈ {1, . . . , n}, k ∈ {1, . . . , p},
∂uk
z
d ∂fi
(−1)εi +εl
(z, u, d) ≥ 0, ∀i ∈ {1, . . . , n}, l ∈ {1, . . . , q}.
∂dl
C. Mixed-monotonicity
The larger class of mixed-monotone systems can be defined through the use of a monotone decomposition function,
decomposing the dynamics of the system into its increasing
and decreasing components.
Definition 3. System (1) with vector field f : Z ×U ×D → Rn
is mixed-monotone if there exists a decomposition function
g : Z × U × D × Z × U × D → Rn such that:
• f is embedded on the diagonal of g:
g(z, u, d, z, u, d) = f (z, u, d),

•

g is increasing in its first 3 arguments: ∀z, z 0 , z ∗ ∈ Z,
u, u0 , u∗ ∈ U and d, d0 , d∗ ∈ D,
z z z 0 , u u u0 , d d d0
⇒ g(z, u, d, z ∗ , u∗ , d∗ ) ≤ g(z 0 , u0 , d0 , z ∗ , u∗ , d∗ ),

•

g is decreasing in its last 3 arguments: ∀z, z 0 , z ∗ ∈ Z,
u, u0 , u∗ ∈ U and d, d0 , d∗ ∈ D,
z ∗ z z 0 , u∗ u u0 , d∗ d d0
⇒ g(z, u, d, z ∗ , u∗ , d∗ ) ≥ g(z, u, d, z 0 , u0 , d0 ),

where ≤ and ≥ are the componentwise inequalities.
Note that in [30], a continuous-time system (1) is instead
defined as mixed-monotone when its trajectory Φf has a
decomposition function. For the sake of brevity, we replace it
by Definition 3 (where the vector field f has a decomposition
function) by virtue of [30, Theorem 1] stating that under mild
conditions, having a decomposition function for f implies that
we can construct one for Φf (which will be provided in the
proof of Theorem 6 below).
Similarly to monotone systems, mixed-monotone systems
can be characterized by having a vector field whose partial
derivatives have a constant sign, but without the constraint that
these signs must be compatible with each other (in Proposition 2, εzi , εuk and εdl are involved in several inequalities) [5].
Proposition 4. System (1) is mixed monotone if there exists
2
{εzij | i, j ∈ {1, . . . , n}} ∈ {0, 1}n , {εuik | i ∈ {1, . . . , n}, k ∈
np
{1, . . . , p}} ∈ {0, 1}
and {εdil | i ∈ {1, . . . , n}, l ∈
nq
{1, . . . , q}} ∈ {0, 1} such that for all z ∈ Z ⊆ Rn ,
u ∈ U ⊆ Rp and d ∈ D ⊆ Rq we have:
z ∂fi
(z, u, d) ≥ 0, ∀i, j ∈ {1, . . . , n},
(−1)εij
∂zj
u ∂fi
(−1)εik
(z, u, d) ≥ 0, ∀i ∈ {1, . . . , n}, k ∈ {1, . . . , p},
∂uk
d ∂fi
(z, u, d) ≥ 0, ∀i ∈ {1, . . . , n}, l ∈ {1, . . . , q}.
(−1)εil
∂dl
Note that unlike Proposition 2 for monotone systems,
i
Proposition 4 also contains a condition on the sign of ∂f
∂zi
(i.e. with i = j) to obtain sufficient conditions adapted
to Definition 3. Sufficient conditions closer to the ones in
Proposition 2 (∀i, j, i 6= j) have been proposed in [6] for a
different definition of mixed-monotonicity involving the partial
derivatives of g.
Although, to the best of our knowledge, the conditions in
Proposition 4 do not appear in the literature for continuoustime systems, its proof is omitted here since in the next
section we provide a weaker sufficient condition for mixedmonotonicity encompassing the one in Proposition 4.
D. General monotonicity-based reachability analysis
A recent result described in [30] extended the sufficient
conditions for mixed-monotonicity of continuous-time systems
by defining decomposition functions as in Definition 3 for
systems which do not satisfy the conditions in Proposition 4,
i.e. vector fields whose partial derivatives do not necessarily
have constant signs. While this result was then used to create

4

abstractions in [29], the considered abstraction approach involving infinite-time reachability analysis is different from the
one in this paper, where transitions of our abstractions describe
states that may be reached in a fixed and known finite time.
Below, we thus describe how this extended characterization of
mixed-monotonicity can be exploited to compute a finite-time
over-approximation of reachable sets for any continuously
differentiable continuous-time dynamical system.
In what follows, several steps need to be identically applied
to all three variables z ∈ Z ⊆ Rn , u ∈ U ⊆ Rp and d ∈
D ⊆ Rq . When this is the case, we will use generic notations
with variable c ∈ {z, u, d} and dimension m ∈ {n, p, q} such
that c ∈ Rm . We first denote as acij and bcij the bounds of
the partial derivatives of the vector field f as follows: for all
z ∈ Z, u ∈ U, d ∈ D, i ∈ {1, . . . , n} and j ∈ {1, . . . , m},
∂fi
(z, u, d) ∈ [acij , bcij ].
∂cj

(2)

The values of these bounds lead us to consider the 4 cases
below, covering all possibilities for the sign of each partial
derivative, as in [30]:
(C1) acij ≥ 0: positive,
(C2) acij ≤ 0 ≤ bcij and |acij | ≤ |bcij |: mostly positive,
(C3) acij ≤ 0 ≤ bcij and |acij | ≥ |bcij |: mostly negative,
(C4) bcij ≤ 0: negative.
(C1) and (C4) correspond to a partial derivative with a constant
sign and their influence on the definition of the decomposition
function can be handled as in [5] for systems satisfying
Proposition 4. On the other hand, the decomposition method
needs to be adapted in the non-constant sign cases (C2) and
(C3) in order to obtain a monotone decomposition function as
in Definition 3.
We define the function g such that for all z, z ∗ ∈ Z, u, u∗ ∈
U, d, d∗ ∈ D and i ∈ {1, . . . , n} we have
gi (z, u, d, z ∗ , u∗ , d∗ ) = fi (Zi , Ui , Di ) + αiz (z − z ∗ ) (3)
+ αiu (u − u∗ ) + αid (d − d∗ ),
where the components of Zi = (zi1 . . . zin )> , Ui =
c
c
(ui1 . . . uip )> , Di = (di1 . . . diq )> and αic = (αi1
. . . αim
)
∂fi
are defined according to cases (C1)-(C4) for ∂cj as follows
with c ∈ {z, u, d} in all notations below:

c
(

−aij if (C2),
cj if (C1) or (C2),
c
cij =
αij = bcij
if (C3),

c∗j if (C3) or (C4),

0
otherwise.
Proposition 5. The function g : Z ×U ×D ×Z ×U ×D → Rn
defined in (3) is a decomposition function for system (1) with
vector field f : Z × U × D → Rn .
Proof. This proof is an immediate extension of the one
provided in more details in [30] for the case of autonomous
systems. By taking c = c∗ in (3) for all c ∈ {z, u, d}, we first
obtain the embedding g(z, u, d, z, u, d) = f (z, u, d). Then due
∂gi
to the terms αic (c − c∗ ) in (3), we can show that
≥ 0
∂cj
∂gi
and
≤ 0 for all i and j, resulting in the increasing and
∂c∗j
decreasing components, respectively, as in Definition 3.

Up to this point, all considerations in Section II-D are
reminders and extensions, to non-autonomous systems with
control and disturbance inputs, of the results in [30] leading
to Proposition 5 stating that any continuously differentiable
system is mixed-monotone as in Definition 3, i.e. a monotone decomposition function can be found for any such
system. In what follows, we provide our main contribution
on this topic which describes how to compute an interval
over-approximation of the finite-time reachable set for any
continuously differentiable system (1), without needing any
additional assumption. This approach uses the monotonicity of
the decomposition function (3) to efficiently obtain this overapproximation from the computation of a single successor of
the dynamical system defined below:
 


ż
g(z, u, d, z ∗ , u∗ , d∗ )
∗
∗ ∗
=
h(z,
u,
d,
z
,
u
,
d
)
=
.
ż ∗
g(z ∗ , u∗ , d∗ , z, u, d)
(4)
Similarly to Φf , we denote the trajectories of (4) as
2
Φh (·, z, u, d, z ∗ , u∗ , d∗ ) : R+
0 → Z , where bold variables are
piecewise continuous input functions. Let Φ1h and Φ2h denote
the first n and last n components of Φh , respectively. Then,
system (4) can be used to compute over-approximations of the
reachable sets of (1) as follows.
Theorem 6. For all bounds z, z ∈ Rn , u, u ∈ Rp , d, d ∈ Rq
and for all t ∈ R+
0 , z ∈ [z, z], u : [0, t] → [u, u] and d :
[0, t] → [d, d] we have
Φ1h (t, z, u, d, z, u, d) ≤ Φf (t, z, u, d) ≤ Φ2h (t, z, u, d, z, u, d),
using componentwise inequalities.
Proof. We first prove that (4) is a monotone system as
in Proposition 2. From Proposition 5 and Definition 3 we
know that for all variables c ∈ {z, u, d} (with c ∈ Rm ,
m ∈ {n, p, q}), i ∈ {1, . . . , 2n} and j ∈ {1, . . . , m} we have
(
(
∂hi ≥ 0 if i ≤ n,
∂hi ≤ 0 if i ≤ n,
and
∂cj ≤ 0 if i ≥ n,
∂c∗j ≥ 0 if i ≥ n.
It follows from Proposition 2 that (4) is monotone with
εzi = εuk = εdl = 0 for i ∈ {1, . . . , n}, k ∈ {1, . . . , p}, l ∈
{1, . . . , q} and εzi = εuk = εdl = 1 for i ∈ {n + 1, . . . , 2n},
k ∈ {p + 1, . . . , 2p}, l ∈ {q + 1, . . . , 2q}. Then from [1], the
monotonicity of (4) can be described as in Definition 1 with the
partial orders z , u and d on the spaces R2n , R2p and R2q ,
respectively, as defined below. For all variables c ∈ {z, u, d}
with c ∈ Rm , the partial order c is characterized by the
− m
m
orthant (R+
of space R2m as follows:
0 ) × (R0 )
(
 1
 3
c1 ≤ c3 ,
c
c
1 2 3 4
m
∀c , c , c , c ∈ R ,

⇔
(5)
c
c2
c4
c2 ≥ c4 ,
m
where ≤ and ≥ are the componentwise inequalities on
 R
 .
c
c
Noting that for all c ∈ [c, c] ⊆ Rm we can write
c
 
 
c
c
c
, we can then use Definition 1 for system (4)
c
c

5

to obtain the following over-approximation: for all t ∈ R+
0,
z ∈ [z, z], u : [0, t] → [u, u] and d : [0, t] → [d, d] we have
(
Φh (t, z, u, d, z, u, d) z Φh (t, z, u, d, z, u, d),
Φh (t, z, u, d, z, u, d) z Φh (t, z, u, d, z, u, d).


Φf (t, z, u, d)
Since Φh (t, z, u, d, z, u, d) =
from DefiniΦf (t, z, u, d)
tion 3, Φ1h is thus the decomposition function for Φf . By symmetry of the dynamics (4), we have Φ1h (t, z, u, d, z, u, d) =
Φ2h (t, z, u, d, z, u, d) finally giving the result in Theorem 6.
Theorem 6 thus provides a method to obtain overapproximations of the finite-time reachable sets for any continuously differentiable system (1) by computing a single
successor state Φh (t, z, u, d, z, u, d) of system (4). As will
be shown in the next sections of this paper, these overapproximations can then be used to define the transition
relation of a symbolic abstraction for the dynamical system
(1), similarly to [18], [5] but applicable to the much wider
class of continuously differentiable systems. To simplify the
notations in the remainder of this paper, we denote as
RS(t, Z 0 , u) = [Φ1h (t, z, u, d, z, u, d), Φ2h (t, z, u, d, z, u, d)],
(6)
the over-approximation obtained as in Theorem 6 from an
interval of initial states Z 0 = [z, z], with a constant control
input function u : [0, t] → {u} and assuming that the
disturbance set of (1) is bounded within the interval D = [d, d].
Remark 7. Similar methods for monotone systems as in [18]
or the subclass of mixed-monotone systems as in Proposition 4
and [5] provide a tight over-approximation of the reachable set
(i.e. the boundary of the over-approximation interval intersects
the closure of the reachable set). Although the result in
Theorem 6 relies on the monotonicity of (4), the tightness
of the obtained over-approximation for system (1) cannot be
guaranteed in the general case due to the new terms αic (c−c∗ )
in the decomposition function (3). Therefore and as expected
intuitively, big deviations from the constant sign cases (i.e.
large |acij | in (C2) or large |bcij | in (C3)) will result in more
conservative over-approximations.
The conservativeness described in Remark 7 can be partially
mitigated in the scope of abstraction creation.
Remark 8. Since the computation of the over-approximation
RS(t, Z 0 , u) as in (6) only requires the knowledge of Φh on the
time period [0, t], the conditions “∀z ∈ Z, u ∈ U, d ∈ D” on
∂fi
(z, u, d) ∈ [acij , bcij ] in (2) can be relaxed to any
the bounds ∂c
j
0
subset Z ⊆ Z, U 0 ⊆ U and D0 ⊆ D containing all possible
states and inputs during the time period [0, t]. In such case,
the system (1) would not be described as mixed-monotone as
in Definition 3 (although it could), but as piecewise mixedmonotone since a different decomposition function g would be
used for each computation of a less conservative RS(t, Z 0 , u).
Apart from taking U 0 = {u}, the choice of the other subsets is
application dependent and a strict subset may not always be
obtained. An example is provided in Section V-A for a unicycle
model.

III. H IERARCHICAL DECOMPOSITION
We consider a high-level control problem on a continuous
dynamical system (1) with continuously differentiable vector
field f evolving in a given workspace Z ⊆ Rn associated to a
uniform partition P ⊆ 2Z into intervals (for compatibility
with the monotonicity-based over-approximation as in (5)).
The description of this workspace also includes a set Obs ⊆ P
of unsafe regions (referred to as obstacles in this section) and a
set Π ⊆ P\Obs of regions of interest. The control specification
is described by a Linear Temporal Logic (LTL) formula ϕ
defined over the set of regions of interest Π. The reader is
referred to [2] for an introduction on the LTL framework.
Given a sampling period τ ∈ R+
0 , we thus aim at solving the
following problem on the sampled version Sτ = (Xτ , Uτ , δτ )
of (1) with Xτ = Z, Uτ = U and δτ as defined in Section II-A.
Problem 9. Find a controller C : Xτ → Uτ such that the
closed-loop sampled system Sτ with transitions δτ (z, C(z))
satisfies the LTL formula ϕ while avoiding the obstacles
Obs ⊆ P.
To solve Problem 9, we propose a hierarchical control structure involving three different abstraction layers of the dynamical system and its environment, each of which successively
addresses one aspect of the control problem as sketched in
Figure 1. The evolution of the control objectives (highlighted
in red in Figure 1) is obtained through the following three
steps, each applied on a different abstraction layer (in blue).
• We first solve the LTL planning problem on a finite transition system representing only the regions of interest (RoI
in Figure 1) of the workspace. The resulting accepting
path is a (possibly infinite) sequence of regions of interest
satisfying the LTL formula ϕ.
• Based on the workspace partition P and its subset of
obstacles Obs ⊆ P, a finite transition system describing
possible motion in this workspace (disregarding the dynamics of (1)) taking into account obstacle avoidance is
created and used to obtain a discrete plan in P connecting
all pairs of consecutive regions of interest in the accepting
path.
• A controller for the dynamical system to follow these
discrete plans is finally synthesized through an abstraction
refinement approach relying on the over-approximation
operator (6).
LTL formula

Workspace (RoI,
obstacles, partition)
Dynamical system

Sequence
of RoI
FTS of
the RoI

Discrete plan
between each
pair of RoI

Control synthesis
using abstraction
refinement

FTS of the
partitioned
workspace
Symbolic
abstraction

Fig. 1. Hierarchical structure of the problem solution (RoI = Regions of
Interest, FTS = Finite Transition System).

The proposed structure with the first and second layers has
the advantage of providing a solution to the LTL planning
on P at a significantly lower computational cost than if this
planning problem were to be solved in a single step, directly on

6

the larger transition system describing all possible motions in
the partitioned workspace. In addition, the use of a refinement
approach in the third layer is to make sure that the dynamical
system can deterministically follow the plans obtained in the
second layer.
A. Solution of the LTL problem
Let SΠ = (Π, δΠ ) be a transition system whose states are
the regions of interest in the finite set Π ⊆ P\Obs and its
transition relation is δΠ : Π → 2Π . The easiest choice is
to define this relation such that δΠ (π) = Π for all π ∈ Π,
thus implying that this first layer of abstraction considers that
any region of interest can be reached from any other region,
disregarding the workspace geometry, distance and time for
such transition. Alternatively, the transition relation can be
manually created with δΠ (π) Π to take into consideration
specific constraints related to the considered workspace geometry or control problem. Such an example is presented in
Section V-B2 for the simulation example of Section V.
While verification problems are usually solved by creating
a Büchi Automaton representing the negation ¬ϕ of the LTL
formula ϕ, computing the product of the transition system
with this automaton and then searching this product for paths
satisfying ¬ϕ (i.e. counter-examples of ϕ), LTL planning
problems can similarly be solved but by using a Büchi
Automaton representing ϕ (instead of its negation) in order
to obtain an accepting path in SΠ satisfying the LTL formula
ϕ [2]. The problem of finding such an accepting path can
thus be solved by using any existing LTL model checker (see
e.g. [12]). Let π̄ = π 0 π 1 π 2 . . . denote this accepting path (if it
exists) represented as a (possibly infinite) sequence of regions
of interest in Π.
B. Extraction of a discrete plan
For any cell σ ∈ P of the workspace partition P, let
N (σ) ⊆ P be the set of its neighbor cells (i.e. the partition
elements having a common facet with σ). We also consider
that σ ∈ N (σ). The second abstraction layer thus describes the
environment while disregarding the system dynamics and is
represented by the transition system SP = (P, δP ) whose set
of states (or cells) is P and its transition relation δP : P → 2P
is such that δP (σ) = N (σ)\Obs for all σ ∈ P\Obs. As a
result, any behavior of SP induced by the above transition
relation δP is guaranteed to satisfy the obstacle avoidance.
Then for each pair (π i , π i+1 ) ∈ Π2 of consecutive regions
of interest in the accepting path π̄, we look for a plan
Σi = σ0i σ1i . . . σri i in P\Obs connecting the two cells σ0i = π i
and σri i = π i+1 . Note that since Π is finite, there is necessarily
a finite number of such pairs despite the accepting path π̄
being infinite. The search for the plan Σi = σ0i σ1i . . . σri i
can be obtained through classical graph search algorithms
on SP (see e.g. [7]), such as a Breadth-First Search or by
applying a Dijkstra algorithm if we want to add some weight
on the transitions (e.g. to penalize transitions going to a
cell neighboring an obstacle). Note that these searches are
guaranteed to find such plans Σi as long as π i and π i+1 can be
connected by SP . If some Σi cannot be found, it means that

the accepting path π̄ is not feasible in P\Obs and Problem 9
may not have a solution (at least not without revising the path
π̄, which is not in the scope of this paper).
Remark 10. Our problem formulation with Π ⊆ P (i.e. each
region of interest corresponds to a single cell of the workspace
partition) ensures that each pair (π i , π i+1 ) in π̄ only needs one
plan Σi as above. The more general case with Π ⊆ 2P can still
be handled but at a much greater computational cost, since a
plan in P needs to be found for each pair in π i × π i+1 ⊆ P 2 .
C. Control synthesis
Considering both steps described in Sections III-A
and III-B, Problem 9 can then be solved by obtaining a
solution to the following problem for each plan Σi .
Problem 11. For a plan Σi = σ0i σ1i . . . σri i in P as in
Section III-B, find a controller C i : Xτ → Uτ such that
the closed-loop sampled system Sτ follows this plan, i.e. for
any trajectory z0 . . . zri of Sτ with z0 ∈ σ0i and zk+1 ∈
δτ (zk , C i (zk )) for all k ∈ {0, . . . , ri − 1}, it holds that
zk ∈ σki .
In this paper, this last step is solved through the use of
a third abstraction layer over-approximating the dynamics of
the sampled system Sτ . In what follows, the sampling period
τ ∈ R+
0 used in both Sτ and its abstraction is assumed
to be given. While, to the best of our knowledge, there
exists very few results involving the choice of this sampling
period for abstraction-based approaches [4], some guidelines
are provided in Section V-B4 for a unicycle model and in [15]
for a class of dynamical systems with additive control input
(ż = f (z, d) + u with z, u ∈ Rn ). An abstraction Sa of Sτ
can then be obtained from the over-approximation method of
the reachable set in time τ as described in Theorem 6 and
(6), and is defined as the transition system Sa = (Xa , Ua , δa ),
where
• the set of states (or symbols) Xa is a partition of the
workspace Z ⊆ Rn into intervals, i.e. any symbol s ∈ Xa
is also an interval s ⊆ Z of the workspace,
• the set of inputs Ua is a finite subset of control values in
U,
0
• a transition s ∈ δa (s, u) between symbols s ∈ Xa and
0
s ∈ Xa with input u ∈ Ua exists if s0 ∩ RS(τ, s, u) 6= ∅
as defined in (6).
Since the above approach creates a non-deterministic abstraction, taking the partition Xa = P would most likely
result in being unable to synthesize a controller such that
the abstraction Sa deterministically follows a desired plan
Σi = σ0i σ1i . . . σri i in P. Instead of manually looking for a finer
partition on which the control problem is feasible, we consider
an abstraction refinement approach, detailed in Section IV,
where an abstraction Sa = (Xa , Ua , δa ) is created on the
initial coarse partition Xa = P and then iteratively refined
by re-partitioning the elements of Xa that are responsible for
preventing the synthesis of a controller. Since this refinement
procedure is guided by the plan to be followed, each plan Σi
will be associated with its own abstraction Sai = (Xai , Ua , δai )
(using the same control set Ua for all plans).

7

Remark 12. This type of abstractions is chosen to combine
the hierarchical decomposition with the results on reachability
analysis in Section II-D, and the need for refinement then
follows from the non-determinism of these abstractions. This
third abstraction layer can however be replaced by any alternative method which could synthesize a controller for Sτ to
follow the plan Σi . One possible candidate is the deterministic
abstraction in [10] which would not require any refinement.

i

1

2

3

i
Algorithm 1: ValidSet(σki , V i (σk+1
)). Computes the
i i
valid set V (σk ) and associated controller Cai at step k ∈
{0, . . . , ri − 1} of the plan Σi = σ0i σ1i . . . σri i .

IV. A BSTRACTION REFINEMENT
While the first two steps of the hierarchical solution in
Section III can be solved with well established tools as
mentioned in Sections III-A and III-B, the solution to the third
step using abstraction refinement is a more recent result in the
scope of control synthesis for continuous dynamical systems.
For the sake of self containment of this paper, this section thus
details the considered abstraction refinement approach initiated
in [17].
A. Valid sets
Given a plan Σi = σ0i σ1i . . . σri i in the partition P, we first
define the notion of valid sets with respect to the plan Σi . For
the abstraction Sai = (Xai , Ua , δai ) associated to Σi , we define
i
the function Pai : P → 2Xa such that Pai (σ) = {s ∈ Xai | s ⊆
σ} corresponds to the projection of a cell σ ∈ P onto the
given finer partition Xai .
Definition 13. For the plan Σi = σ0i . . . σri i , we define the
i
function V i : P → 2Xa such that V i (σri i ) = {σri i } and for
all k ∈ {0, . . . , ri − 1}:

V i (σki ) = s ∈ Pai (σki ) | ∃u ∈ Ua such that
i
δai (s, u) ⊆ V i (σk+1
) .

The set V i (σki ) is called the valid set of cell σki . A cell σ ∈ P
and a symbol s ∈ Xai such that s ∈ Pai (σ) are said to be
valid if V i (σ) 6= ∅ and s ∈ V i (σ), respectively. Conversely, a
symbol s ∈ Pai (σ) is invalid if s ∈
/ V i (σ).
σri i

i

Since
is the final cell of the plan Σ to be reached,
i
it is considered as valid and the function V i : P → 2Xa is
initialized with V i (σri i ) = {σri i }. We then proceed backwards
on the plan Σi to iteratively define the other valid sets V i (σki )
as the subset of symbols in σki which can be driven towards
i
the valid set V i (σk+1
) of the next cell for at least one control
input in Ua .
i
The function ValidSet(σki , V i (σk+1
)) in Algorithm 1 first
i i
computes the valid set V (σk ) with respect to the plan Σi as in
Definition 13. Then, the controller Cai : Xai → Ua associates to
each valid symbol s ∈ V i (σki ) the first control value ensuring
that s is valid, therefore reducing the computational complexity by stopping the search of such inputs as soon as one is
found. An alternative version of Algorithm 1 can be proposed
by defining a non-deterministic controller Cai : Xai → 2Ua
containing more than one satisfying input, thus allowing for a
future optimization on the choice of the control.

Data: P, Xai , Ua , Pai : P → 2Xa .
Input: Considered cell σki ∈ P.
i
i
) ⊆ Pai (σk+1
).
Input: Targeted valid set V i (σk+1
i i
V (σk ) =
i
)
s ∈ Pai (σki ) ∃u ∈ Ua such that δai (s, u) ⊆ V i (σk+1
i i
i
∀s
∈
V
(σ
),
C
(s)
is
taken
as
the
first
value
in
a
k

i
u ∈ Ua δai (s, u) ⊆ V i (σk+1
)
i i
i
i
return {V (σk ), Ca : Xa → Ua }

B. Refinement
The abstraction refinement approach then follows Algorithm 2 that we describe below. The abstraction Sai =
(Xai , Ua , δai ) is initialized with respect to the initial coarse
partition Xai = P and the valid set V i (σri i ) of the last cell of
the plan Σi is initialized as in Definition 13 (line 1). Then,
similarly to Definition 13, we proceed backwards on the plan
Σi = σ0i σ1i . . . σri i and compute the valid set V i (σki ) and
associated controller Cai as in Algorithm 1 from σri i −1 to σ0i
(lines 2-3).
i

1
2
3
4
5
6
7
8
9

Data: P, Σi = σ0i σ1i . . . σri i ∈ P ri +1 , Pai : P → 2Xa .
Initialization: Xai = P, V i (σri i ) = {σri i }
for k from ri − 1 to 0 do
i
))
{V i (σki ), Cai } = ValidSet (σki , V i (σk+1
while V i (σki ) = ∅ or V i (σ0i ) 6= Pai (σ0i ) do
j = Pick(k, ri − 1)
forall s ∈ Pai (σji )\V i (σji ) do
Xai = (Xai \{s}) ∪ Split(s)
for l from j to k do
i
))
{V i (σli ), Cai } = ValidSet (σli , V i (σl+1
i

Output: {Xai , V i : P → 2Xa , Cai : Xai → Ua }
Algorithm 2: Abstraction refinement algorithm.
If for some k the valid set V i (σki ) is empty (line 4), the
partition Xai needs to be refined to improve the valid sets.
For this, we first pick a cell σji with j ∈ {k, . . . , ri − 1} to
be refined (line 5), split each of its invalid subsymbols s ∈
Pai (σji )\V i (σji ) into a set of subsymbols Split(s) and update
the partition Xai accordingly (lines 6-7), and finally update the
valid sets and controller (using Algorithm 1) for all cells from
σji to σki whose valid sets may include additional symbols
after this refinement (lines 8-9). This refinement procedure is
then repeated until all cells of the plan are valid (V i (σki ) 6=
∅) and the valid set of the initial cell covers the whole cell
(V i (σ0i ) = Pa (σ0i ), line 4) to guarantee that any initial state
in σ0i = π i can be controlled to follow the plan Σi leading
to the cell σri i = π i+1 . For each plan Σi , Algorithm 2 then
returns the refined partition Xai , the valid set function V i and
the associated controller Cai .
The definition of both functions Pick and Split can be
arbitrary but we can provide some guidelines. It is usually

8

advised to prioritize the refinement of the coarsest of the
i
visited cells σki , . . . , σr−1
as they are more likely to be the
i i
reason for having V (σk ) = ∅. Possible choices of the
function Pick are described in [16] using a priority queue
and in [15] using a cost function estimating the complexity
of the remaining computations. For Split, one should aim
at obtaining subsymbols which remain compatible with the
over-approximation method used to obtain Sai (intervals of Rn
for the monotonicity-based approach of this paper). Classical
examples include: splitting the symbol s along its longest
dimension only; and uniformly splitting s ⊆ Rn into 2n
subsymbols (2 per dimension).
C. Solution to Problem 11
To control the sampled system Sτ along the plan Σi =
i i
σ0 σ1 . . . σri i with the controller Cai obtained for the abstraction Sai in Algorithm 2, systems Sτ = (Xτ , Uτ , δτ ) and
Sai = (Xai , Ua , δai ) must satisfy a feedback refinement relation
defined below, adapted from [21].
Definition 14. A map H i : Xτ → Xai is a feedback refinement
relation from Sτ to Sai if: ∀z ∈ Xτ , s = H i (z), ∀u ∈ Ua ⊆
Uτ , ∀z 0 ∈ δτ (z, u) we have H i (z 0 ) ∈ δai (s, u).
Such a relation implies that for any pair (z, s) of matching
state and symbol and any control u of the abstraction Sai , the
behaviors of the original system Sτ with the same control u
can be matched by behaviors of Sai . As a consequence, if a
controller is synthesized so that Sai satisfies some specification, then this controller can be composed with the feedback
refinement relation H i for Sτ to satisfy the same specification.
Theorem 15. If Algorithm 2 terminates for a plan Σi =
σ0i σ1i . . . σri i , let H i : Xτ → Xai such that H i (z) = s ⇔
z ∈ s. Then the controller C i : Xτ → Uτ defined by
C i (z) = Cai (H i (z)) for all z ∈ Xτ solves Problem 11,
i.e. for any trajectory z0 . . . zri of Sτ with z0 ∈ σ0i and
zk+1 ∈ δτ (zk , C i (zk )) for all k ∈ {0, . . . , ri − 1}, we have
zk ∈ σki .
Proof. We first prove that the map H i is a feedback refinement
relation from Sτ to Sai as in Definition 14. Let z ∈ Xτ ,
s = H i (z) ∈ Xai , u ∈ Ua ⊆ Uτ , z 0 ∈ δτ (z, u) and
s0 = H i (z 0 ). From the definition of Sτ and Theorem 6, we
have z 0 ∈ RS(τ, s, u), where RS is the over-approximation
operator defined in (6). Since we also have z 0 ∈ s0 , then
s0 ∩ RS(τ, s, u) 6= ∅ which implies that s0 ∈ δai (s, u) as in the
definition of Sai in Section III-C.
It is then sufficient to prove that the controller Cai : Xai →
Ua solves Problem 11 for the abstraction Sai , which is the case
by construction of Algorithm 2. Indeed if Algorithm 2 terminates, then its line 4 guarantees that any symbol s0 ∈ Pai (σ0i )
is valid with respect to Σi : s0 ∈ V i (σ0i ). Then by definition
of the valid sets in Definition 13 and Algorithm 1, for all
i
k ∈ {0, . . . , ri − 1} we have δai (sk , Cai (sk )) ⊆ V i (σk+1
), and
i
i
i
thus for all sk+1 ∈ δa (sk , Ca (sk )) we have sk+1 ∈ σk+1
.
A solution to the main LTL control problem immediately
follows from Theorem 15.

Corollary 16. If Algorithm 2 terminates for all plans Σi
derived in Section III-B, then the controller C : N × Xτ → Uτ
defined by C(i, z) = Cai (H i (z)) solves Problem 9.
Although the proposed hierarchical decomposition as in
Section III enables the consideration of a general high-level
control problem (both in terms of specification and dynamics) with a reduced complexity, guarantees for the converse
implication of Corollary 16 (“if Problem 9 can be solved on
Sτ , then the problem decomposition and Algorithm 2 will find
a controller solving it”) cannot be provided in general due to
both the hierarchical decomposition of the problem and the use
of over-approximations (6) in the definition of the abstractions
Sai .
Remark 17. Since this third step has the largest computational cost of the problem decomposition, a further reduction
of the computational burden with higher chances of finding
a controller could be obtained by combining the abstraction
refinement with a plan revision approach as in [15], allowing
to look for alternative plans of Σi connecting the same two
regions of interest.
V. A PPLICATION TO NON - HOLONOMIC MOTION PLANNING
In this section, we consider a high-level motion planning
problem for a mobile robot evolving in an office environment.
The robot is modeled by disturbed unicycle dynamics:


v cos(θ) + d1
ż = f (z, u, d) =  v sin(θ) + d2 
(7)
ω + d3
where z = (x, y, θ) ∈ Z ⊆ R3 is the state (2D position and
orientation), u = (v, ω) ∈ U ⊆ R2 is the control input (linear
and angular velocities) and d = (d1 , d2 , d3 ) ∈ D ⊆ R3 is the
disturbance. We further assume that the disturbance take its
values in an interval D = [d, d] of R3 .
In what follows, we first present in Section V-A how
to apply the proposed reachability analysis results to the
unicycle (7). Section V-B then describes the considered motion
planning problem and the associated simulation results.
A. Reachability analysis
We first define the decomposition function g : Z × U ×
D × Z × U × D → R3 as in (3) for the unicycle model (7).
Since all partial derivatives of f3 are non-negative (ac3j ≥ 0
as in (C1) of Section II-D
 for all c ∈ {z, u, d}), we thus have
α3z = α3d = 0 0 0 , α3u = 0 0 , Z3 = z, U3 = u and
D3 = d, leading to:
g3 (z, u, d, z ∗ , u∗ , d∗ ) = f3 (z, u, d) = ω + d3 .

(8)

As mentioned in Remark 8 (U 0 = {u}), the overapproximation (6) of the reachable set computed to create
abstractions as in Section III-C considers known and constant
control values over the sampling period [0, τ ] (i.e. u = u∗ in
i
(3)). Although ∂f
∂v do not have a constant sign for i ∈ {1, 2},
this will be disregarded in what follows since the corresponding term αiu (u − u∗ ) in (3) is equal to 0 when u = u∗ (i.e.

9

these signs have no influence on the computation of the overapproximation as in (6)). In addition, taking u = u∗ results
in U1 = U2 = u. Since for i, j ∈ {1, 2} and k ∈ {1, 2, 3}
∂fi
∂fi
the partial derivatives ∂z
and ∂d
are non-negative, we have
j
k
z
z
αi1
= αi2
= 0, αid = 0 0 0 and Di = d, and we thus
obtain for i ∈ {1, 2}:
z
gi (z, u, d, z ∗ , u, d∗ ) = fi (Zi , u, d) + αi3
(θ − θ∗ ),
z
α13

(9)

z
α23

where Z1 , Z2 ,
and
are defined as in Section II-D
according to the values of the four bounds az13 , bz13 , az23 and
bz23 of the remaining two partial derivatives whose signs are
not constant:
∂f2
∂f1
= −v sin(θ) ∈ [az13 , bz13 ],
= v cos(θ) ∈ [az23 , bz23 ].
∂θ
∂θ
(10)
1 ∂f2
To avoid taking the too conservative bounds ∂f
∂θ , ∂θ ∈
[−v, v] resulting from all possible orientations θ ∈ (−π, π]
as in (2), we rather follow Remark 8 to find a subset of
possible orientations on each sampling period [0, τ ] and thus
obtain tighter bounds in (10). Given an interval of initial
orientations [θ0 , θ0 ] ⊆ (−π, π] and a known angular velocity
ω, (7) gives θ̇ ∈ [ω + d3 , ω + d3 ], and thus the orientation
θ(τ ) after the sampling period of τ > 0 is bounded as
θ(τ ) ∈ [θ0 + τ (ω + d3 ), θ0 + τ (ω + d3 )]. Over the whole
sampling period [0, τ ], we obtain the following set [θ, θ] of
possible orientations θ([0, τ ]) ∈ [θ, θ]:
[θ, θ] = [θ0 +min(0, τ (ω+d3 )), θ0 +max(0, τ (ω+d3 ))]. (11)
The bounds in (10) can thus be computed by:


az13 = −v maxθ∈[θ,θ] (sin(θ))



bz = −v min
13
θ∈[θ,θ] (sin(θ))
v≥0⇒
z
a23 = v minθ∈[θ,θ] (cos(θ))



bz = v max
23
θ∈[θ,θ] (cos(θ))

(12)

and similar equations swapping the min and max operators
when v < 0.
In addition, we note that the maxima and minima of the cos
and sin functions can be expressed as follows:
(
−1
if θ ≥ π or θ ≤ −π
min (cos(θ)) =
(13)
cos(max(|θ|,
|θ|)) otherwise
θ∈[θ,θ]


1 if θ ≤0 ≤ θ or θ ≥ 2π or θ ≤ −2π




|mod(θ + π, 2π) − π|,
max (cos(θ)) = cos min
|mod(θ + π, 2π) − π|

θ∈[θ,θ]



otherwise
(14)
(
3π
π
−1
if θ ≥ 2 or θ ≤ − 2
min (sin(θ)) =
π
cos(max(|θ − 2 |, |θ − π2 |)) otherwise
θ∈[θ,θ]
(15)

π
5π
3π
1 if θ ≤

2

 2 ≤ θ or θπ≥ 2 or θ ≤ −




|mod(θ + , 2π) − π|,
2 π

max (sin(θ)) = cos min 

θ∈[θ,θ]
|mod(θ
+
,
2π)
−
π|


2


otherwise
(16)

where mod(·, 2π) : R → [0, 2π] is the modulo function and
| · | the absolute value.
From the bounds az13 , bz13 , az23 and bz23 defined in (11)-(16)
for each sampling period, the decomposition function g given
in (8) and (9) leads to the definition of the duplicated dynamical system (4) with the vector field h and the trajectories Φh
as in Section II-D. Finally, Theorem 6 provides the desired
over-approximation as in (6), for all state intervals [z, z] ⊆ Z
and constant control inputs u ∈ U:
RS(τ, [z, z], u) = [Φ1h (τ, z, u, d, z, u, d), Φ2h (τ, z, u, d, z, u, d)].
B. Problem description and simulation results
While the reachability analysis of the unicycle in Section V-A is presented for a disturbed unicycle for the sake
of generality, the following simulation results consider the
undisturbed case (D = {0}3 ). Although the general disturbed
case could still be handled by the proposed framework, the
addition of disturbances increases the conservativeness of the
reachability analysis (see Remark 7), which thus requires more
abstraction refinement steps before finding a controller, and in
turn increases the required computation time and degrades the
visualization of the obtained results.
1) Problem description: We consider a high-level motion
planning problem for a mobile robot evolving in a 33 × 20
square meters office environment. This 2D workspace is
formed by four rooms and a central hallway, as sketched in
Figure 2 uniformly partitioned into 20×12 cells and where the
black cells represent static obstacles (walls). The four regions
of interest (in blue) denoted as π1 to π4 correspond to the
cells in which the observation tasks of each room are to be
carried out.

Fig. 2. Office environment with obstacles (black) and four regions of interest
(blue) as the center of each room.

The considered mobile robot is modeled as a unicycle as
in (7) where the state z = (x, y, θ) evolves in the set Z =
[0, 33] × [0, 20] × (−π, π], the control input u = (v, ω) takes
values in the set U = [−0.5, 0.5] × [−0.3, 0.3] and we assume
that the system is not disturbed (D = {0}3 ). To create finite

10

abstractions as in Section IV, the control set U is uniformly
discretized into the set Ua = {−0.5, −0.25, 0, 0.25, 0.5} ×
{−0.3, −0.15, 0, 0.15, 0.3} with 5 discrete values per dimension. The initial state of (7) is taken in the cell π1 .
The control objective is expressed by the LTL formula
ϕ = ♦π2 ∧ ♦π4 ∧ ♦π3 ∧ ¬π3 Uπ4 .

(17)

In English, the first two elements of this specification mean
that we want to achieve a surveillance task in both π2 and
π4 by visiting each region infinitely often. The last two
elements mean that in addition to this surveillance, we want to
eventually visit π3 but not before π4 has been visited at least
once. Although we could include in (17) the additional safety
specification ¬obstacles of avoiding obstacles at all times,
this obstacle avoidance will actually be handled in the second
step of this approach when exploring the physical environment
to find discrete plans.
The simulation results in this section are obtained on a laptop with a 2.6 GHz CPU and 8 GB of RAM. The computations
for steps 2 and 3 are done on Matlab.
2) First layer - LTL problem on regions of interest: As
in Section III-A, we first define the finite transition system
SΠ = (Π, δΠ ), where Π = {π1 , π2 , π3 , π4 } is the set of regions
of interest. Since the regions of interest are representative cells
for each room, the particular structure of the environment in
Figure 2 leads us to define the transition relation δΠ : Π → 2Π
as follows: δΠ (π1 ) = {π1 , π2 } (leaving room 1 can only be
done through room 2), δΠ (π2 ) = Π (from room 2, the robot
can reach any other room) and δΠ (π3 ) = δΠ (π4 ) = Π\{π1 }
(room 1 cannot be reached directly apart from room 2).
We then solve the LTL problem on SΠ using the model
checker P-MAS-TG described in [11] and the obtained accepting path takes the form of a prefix-suffix sequence π̄ =
π1 π2 π4 π3 (π2 π4 )ω describing an infinite behavior where the
finite prefix π1 π2 π4 π3 is followed once and the finite suffix
π2 π4 is repeated infinitely often. Due to the small size of SΠ ,
this accepting path is obtained in less than 2 milliseconds.
The following two layers then needs to be repeated for each
pair of regions of interest involved in this accepting path: π1 −
π2 , π2 − π4 , π4 − π3 , π3 − π2 and π4 − π2 . Although the pair
π2 − π4 appears in both the prefix and the suffix of π̄, the next
two steps only need to be applied once for this pair.
3) Second layer - Discrete plan in the physical environment:
Following Section III-B, we then define the finite transition
system SP = (P, δP ) representing the evolution of the robot
in the partition environment in Figure 2 but disregarding the
system dynamics (7). The set P then contains the 20 × 12
cells obtained from the partition of the 2D workspace. If a cell
σ ∈ P belongs to an obstacle, we take δP (σ) = ∅. Otherwise,
δP (σ) ⊆ P contains the four neighboring cells (left, right,
top, bottom) of σ, excluding those outside of the considered
environment or belonging to an obstacle. Therefore, the safety
specification ¬obstacles mentioned above is immediately
satisfied as long as we only follow behaviors allowed in SP .
For each of the 5 pairs πi − πj of regions of interest
to be considered, we then use a Breadth-First Search algorithm [7] on SP to obtain one of the shortest discrete plan
Σij = σ0ij σ1ij . . . σrijij in P with σ0ij = πi , σrijij = πj and

ij
σk+1
∈ δP (σkij ) for all k ∈ {0, . . . , rij − 1}. The average
computation time of these search algorithms is 33 milliseconds
per pair πi − πj .
4) Third layer - Abstraction refinement and control synthesis: We first choose the value of the sampling period τ (i.e.
the time for (7) to be controlled from each cell σkij to the next
ij
σk+1
in some discrete plan Σij ) by taking inspiration from
the guidelines provided in [15] for another class of systems.
Considering the unicycle (7) with vertical and horizontal
orientations θ ∈ {−π/2, 0, π/2, π} and using the maximal
linear velocity u = (v, 0) (with v = 0.5 m/s), the minimal
time to control (7) from any initial state in a cell σ ∈ P to
a state in one of its neighbor cells σ 0 ∈ δP (σ) is given by
max(size(σ, 1), size(σ, 2))/v, where size(σ, i) is the dimension of any cell σ ∈ P along the ith axis. Given that (7) may
not always start and keep orientations θ ∈ {−π/2, 0, π/2, π}
or use the maximal linear velocity v, a longer time may
be needed to reach a neighbor cell and we thus choose the
sampling period as slightly larger (by a factor 1.2) than the
computed value: τ = 1.2 ∗ max(33/20, 20/12)/0.5 = 4
seconds.
To take advantage of having a control objective in the 2D
workspace (discrete plan Σij to follow) while the system (7)
actually evolves in a 3D state-space, the abstraction refinement
algorithm is applied with a modified version of Definition 13
for the valid sets: given a cell σ ∈ P of the 2D workspace,
its valid set is
i
V2D
(σ) =

{s ⊆ σ | ∃sθ ⊆ (−π, π], s × sθ ∈

(18)
Xai

i

∩ V (σ × (−π, π])},

i
(σ) contains any projection in the 2D workspace of
that is, V2D
a 3D symbol which belongs to the refined partition Xai and is
valid according to the 3D cell σ × (−π, π] as in Definition 13.
The abstraction refinement thus still needs to work on the
partition Xai of the 3D state space since the orientation θ and
the angular velocity ω influence the reachability analysis of
(7) as in Section V-A, but with a reduced complexity since
this new definition of a valid 2D symbol s only requires the
existence of one valid 3D symbol s × sθ ∈ Xai (instead of the
previous condition where all s × sθ ∈ Xai needed to be valid).
This complexity reduction however comes with the drawback
that we need to rotate the robot between each application of
the symbolic controller using a constant rotation u = (0, ω)
in order to go to an orientation θ ∈ sθ for one of the valid
3D symbols s × sθ corresponding to the current 2D position
(x, y) ∈ s.
The function Pick from Algorithm 2 is chosen similarly
to [16] as a queue which selects the oldest cell added to the
queue among those in the plan Σij which have been refined
the least. Before the first iteration of refinement, each 3D cell
σ × (−π, π] with σ ∈ P is initially split by taking a uniform
partition into 4 subsymbols only on its third dimension (i.e.
partitioning (−π, π] in 4 intervals). The following refinement
iterations (function Split(s) in Algorithm 2) are done by
taking a uniform partition of the 3D symbol s into 2 subsymbols per dimension (i.e. resulting in 23 subsymbols).
For the 5 plans Σ12 , Σ24 , Σ43 , Σ32 and Σ42 obtained above,
the computation time varies between 33 and 186 seconds, with

11

an average of 82 seconds per plan. The number of refinement
iterations per plan ranges from 20 to 46, with an average of
32 iterations.
5) Simulation results: For each of the five plans Σ12 , Σ24 ,
Σ43 , Σ32 and Σ42 obtained in the second step, the results
of the abstraction refinement are displayed in Figures 3-7.
The 2D projection of the refined partition Xai corresponds to
i
the finer black grid. The 2D valid sets V2D
(σ) are displayed
in red. Note that these valid sets are not represented for
the four regions of interest (in blue), but by construction in
Algorithm 2 (line 4), these sets necessarily cover the whole
cell corresponding to the region of interest.
Finally, a simulation of the unicycle model (7) using the
symbolic controller obtained as in Section IV is created. The
initial state z0 is taken randomly in the set π1 × (−π, π]. At
each step in a 3D cell σ3D = σ2D ×(−π, π] with σ2D ∈ P, the
robot measures its position z = (x, y, θ) ∈ σ3D and finds the
corresponding 3D symbol H i (z) ∈ Xai . If H i (z) ∈ V i (σ3D )
is a valid symbol for the current plan, we apply the constant
control value Cai (H i (z)) for τ = 4 seconds. Otherwise, we
know that by construction the 2D projection s2D of the symbol
i
(σ2D ), meaning
H i (z) ∈ Xai belongs to the 2D valid set V2D
0
that there exists another 3D symbol s ∈ Xai with the same
projection s2D and such that s0 ∈ V i (σ3D ). We thus apply a
constant rotation u = (0, ω) until the system reaches a new
state z 0 = (x, y, θ0 ) ∈ s0 and then apply the constant control
value Cai (H i (z 0 )) = Cai (s0 ) for τ = 4 seconds. This is then
repeated at the next measurement of the state.
The trajectory of (7) obtained after applying the above
control strategy for the first occurrence of each plan Σij is then
displayed in green in Figures 3-7. The snaps in this trajectory
correspond to the rotations before applying the next value of
the symbolic controller, while smoother sections over several
cells mean that no such rotation was needed. The trajectory of
(7) following the whole accepting path π̄ = π1 π2 π4 π3 (π2 π4 )ω
is displayed in Figure 8 (without the abstraction refinement
results) for the whole prefix π1 π2 π4 π3 followed by a single
iteration of the suffix π2 π4 . This trajectory is displayed with
a color gradient going from blue to red while progressing
through π̄.
VI. C ONCLUSION
The first contribution of this paper is to define a method
to compute an interval over-approximation of the finite-time
reachable set for any continuously differentiable system. This
method relies on the creation of an auxiliary monotone system
obtained by compensating the non-monotone components of
the initial system with the extremal values of the corresponding
partial derivative over the considered time interval. The generality of this result naturally comes at the cost of an increased
conservativeness due to this compensation of the dynamics
to obtain a monotone system. The second contribution is a
three-layer hierarchical decomposition of a high-level control
problem under a Linear Temporal Logic formula by iteratively
solving finer versions of the problem: first solve the problem
only on the regions of interest involved in the LTL formula,
then realize the obtained sequence of regions by finding discrete plans in the partitioned workspace, and finally synthesize

Fig. 3. Plan Σ12 between π1 and π2 .

Fig. 4. Plan Σ24 between π2 and π4 .

Fig. 5. Plan Σ43 between π4 and π3 .

12

Fig. 6. Plan Σ32 between π3 and π2 .

Fig. 8. Trajectory of the mobile robot following the accepting path π̄ =
π1 π2 π4 π3 (π2 π4 )ω for a single iteration of the suffix. Color gradient from
blue to red while progressing through π̄.

R EFERENCES

Fig. 7. Plan Σ42 between π4 and π2 .

a controller for the dynamical system to follow these plans
using an abstraction refinement approach relying on the above
over-approximation based reachability analysis.
Since the proposed three-layer approach already provides
a very fast solution to the first 2 steps, the main goal for
future work is to improve the efficiency of the third step using
abstraction refinement which represents the main computation
time. In particular, to further increase the generality of this
solution to dynamical systems of large dimensions, a possible
direction is to propose a compositional abstraction refinement
approach similar to [17] where the dynamical system is first
decomposed into subsystems (each considering a subset of
state and control variables) before applying the abstraction
method to each subsystem at a lower computational cost. For
a greater re-usability of this solution minimizing inputs from
the user, this decomposition of the dynamics should ideally be
automated.

[1] D. Angeli and E. D. Sontag. Monotone control systems. IEEE
Transactions on Automatic Control, 48(10):1684–1698, 2003.
[2] C. Baier, J.-P. Katoen, et al. Principles of model checking, volume
26202649. MIT press Cambridge, 2008.
[3] C. Belta, A. Bicchi, M. Egerstedt, E. Frazzoli, E. Klavins, and G. J. Pappas. Symbolic planning and control of robot motion [grand challenges of
robotics]. IEEE Robotics & Automation Magazine, 14(1):61–70, 2007.
[4] D. Boskos and D. V. Dimarogonas.
Decentralized abstractions
for multi-agent systems under coupled constraints. arXiv preprint
arXiv:1506.05297, 2015.
[5] S. Coogan and M. Arcak. Efficient finite abstraction of mixed monotone
systems. In Hybrid Systems: Computation and Control, pages 58–67.
2015.
[6] S. Coogan and M. Arcak. Stability of traffic flow networks with a
polytree topology. Automatica, 66:246–253, 2016.
[7] T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction
to algorithms. MIT press, 2009.
[8] G. E. Fainekos, A. Girard, and G. J. Pappas. Hierarchical synthesis of
hybrid controllers from temporal logic specifications. In HSCC, pages
203–216. Springer, 2007.
[9] C. Finucane, G. Jing, and H. Kress-Gazit. Ltlmop: Experimenting with
language, temporal logic and robot control. In Intelligent Robots and
Systems (IROS), 2010 IEEE/RSJ International Conference on, pages
1988–1993. IEEE, 2010.
[10] E. A. Gol and C. Belta. Time-constrained temporal logic control of
multi-affine systems. Nonlinear Analysis: Hybrid Systems, 10:21–33,
2013.
[11] M. Guo and D. V. Dimarogonas. Multi-agent plan reconfiguration under
local ltl specifications. The International Journal of Robotics Research,
34(2):218–235, 2015.
[12] G. Holzmann. The Spin model checker: primer and reference manual.
Addison-Wesley Professional, 2003.
[13] H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. Temporal-logic-based
reactive mission and motion planning. IEEE transactions on robotics,
25(6):1370–1381, 2009.
[14] M. Mazo Jr, A. Davitian, and P. Tabuada. Pessoa: A tool for embedded
controller synthesis. In CAV, volume 6174, pages 566–569. Springer,
2010.
[15] P.-J. Meyer and D. V. Dimarogonas. Abstraction refinement and
plan revision for control synthesis under high level specifications. In
Proceedings of the 20th IFAC World Congress, pages 9664–9669, 2017.
[16] P.-J. Meyer and D. V. Dimarogonas. Compositional abstraction refinement for control synthesis under lasso-shaped specifications. In
Proceedings of the American Control Conference, pages 523–528, 2017.

13

[17] P.-J. Meyer and D. V. Dimarogonas. Compositional abstraction refinement for control synthesis. Nonlinear Analysis: Hybrid Systems, 27:437–
451, 2018.
[18] T. Moor and J. Raisch. Abstraction based supervisory controller
synthesis for high order monotone continuous systems. In Modelling,
Analysis, and Design of Hybrid Systems, pages 247–265. Springer, 2002.
[19] S. Mouelhi, A. Girard, and G. Gössler. Cosyma: a tool for controller
synthesis using multi-scale abstractions. In Proceedings of the 16th
international conference on Hybrid systems: computation and control,
pages 83–88. ACM, 2013.
[20] P. Nilsson and N. Ozay. Incremental synthesis of switching protocols
via abstraction refinement. In Decision and Control (CDC), 2014 IEEE
53rd Annual Conference on, pages 6246–6253. IEEE, 2014.
[21] G. Reissig, A. Weber, and M. Rungger. Feedback refinement relations
for the synthesis of symbolic controllers. IEEE Transactions on
Automatic Control, 62(4):1781–1796, 2016.
[22] M. Rungger and M. Zamani. Scots: A tool for the synthesis of symbolic
controllers. In Proceedings of the 19th International Conference on
Hybrid Systems: Computation and Control, pages 99–104. ACM, 2016.
[23] S. Russell and P. Norvig. Artificial Intelligence: A Modern Approach.
Prentice Hall Press, 3rd edition, 2009.
[24] H. L. Smith. Monotone dynamical systems: an introduction to the
theory of competitive and cooperative systems, volume 41. American
Mathematical Soc., 1995.
[25] P. Tabuada. Verification and control of hybrid systems: a symbolic
approach. Springer, 2009.
[26] J. Tumova, B. Yordanov, C. Belta, I. Černá, and J. Barnat. A symbolic
approach to controlling piecewise affine systems. In Decision and
Control (CDC), 2010 49th IEEE Conference on, pages 4230–4235.
IEEE, 2010.
[27] T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding horizon
temporal logic planning for dynamical systems. In Decision and Control,
2009 held jointly with the 2009 28th Chinese Control Conference.
CDC/CCC 2009. Proceedings of the 48th IEEE Conference on, pages
5997–6004. IEEE, 2009.
[28] T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R. M. Murray. Tulip:
a software toolbox for receding horizon temporal logic planning. In
Proceedings of the 14th international conference on Hybrid systems:
computation and control, pages 313–314. ACM, 2011.
[29] L. Yang, A. Karnik, B. Pence, M. T. B. Waez, and N. Ozay.
Fuel cell thermal management: Modeling, specifications and correctbyconstruction control synthesis. In Proceedings of American Control
Conference, 2017.
[30] L. Yang and N. Ozay. A note on some sufficient conditions for mixed
monotone systems. Technical report, 2017.

Pierre-Jean Meyer received a Master degree
(diplôme d’ingénieur) in Electrical Engineering and
Automatic Control from the Institut National Polytechnique de Toulouse, France, in 2011. He then
PLACE
received a Ph.D. in Automatic Control from UniPHOTO
versité Grenoble Alpes, France, in 2015. Between
HERE
November 2015 and November 2017, he was a
postdoctoral researcher at the Automatic Control
Department of KTH Royal Institute of Technology,
Stockholm, Sweden. Since November 2017, he is a
postdoctoral researcher at the Department of Electrical Engineering and Computer Sciences at University of California, Berkeley,
USA.
His research interests include formal methods for hybrid control and
more particularly symbolic abstractions, decentralized and compositional
approaches, monotone systems and multi-agent systems.

Dimos V. Dimarogonas received the Diploma in
Electrical and Computer Engineering in 2001 and
the Ph.D. in Mechanical Engineering in 2007, both
from the National Technical University of Athens
PLACE
(NTUA), Greece. From May 2007 to February 2009,
PHOTO
he was a Postdoctoral Researcher at the Automatic
HERE
Control Laboratory, School of Electrical Engineering, KTH Royal Institute of Technology, Stockholm, Sweden, and a Postdoctoral Associate at the
Laboratory for Information and Decision Systems,
Massachusetts Institute of Technology (MIT), Cambridge, MA, USA. He is currently a Professor in Automatic Control, School
of Electrical Engineering, KTH Royal Institute of Technology. His current
research interests include multi-agent systems, hybrid systems, robot navigation, networked control and event-triggered control. Dr. Dimarogonas serves
on the Editorial Board of Automatica, the IEEE Transactions on Automation
Science and Engineering and the IET Control Theory and Applications. He
received an ERC Starting Grant from the European Commission for the
proposal BUCOPHSYS in 2014 and was awarded a Wallenberg Academy
Fellow grant in 2015.

