Robust Abstractions for Control Synthesis:
Robustness Equals Realizability for Linear-Time Properties
Jun Liu
Department of Applied Mathematics
University of Waterloo

arXiv:1803.01387v1 [cs.SY] 4 Mar 2018

j.liu@uwaterloo.ca
ABSTRACT
We define robust abstractions for synthesizing provably correct and robust controllers for (possibly infinite) uncertain
transition systems. It is shown that robust abstractions
are sound in the sense that they preserve robust satisfaction of linear-time properties. We then focus on discretetime control systems modelled by nonlinear difference equations with inputs and define concrete robust abstractions for
them. While most abstraction techniques in the literature
for nonlinear systems focus on constructing sound abstractions, we present computational procedures for constructing
both sound and approximately complete robust abstractions
for general nonlinear control systems without stability assumptions. Such procedures are approximately complete in
the sense that, given a concrete discrete-time control system
and an arbitrarily small perturbation of this system, there
exists a finite transition system that robustly abstracts the
concrete system and is abstracted by the slightly perturbed
system simultaneously. A direct consequence of this result
is that robust control synthesis for discrete-time nonlinear
systems and linear-time specifications is robustly decidable.
More specifically, if there exists a robust control strategy
that realizes a given linear-time specification, we can algorithmically construct a (potentially less) robust control
strategy that realizes the same specification. The theoretical results are illustrated with a simple motion planning
example.

Keywords
Nonlinear systems; control synthesis; abstraction; robustness; linear-time property; linear temporal logic; decidability

1.

INTRODUCTION

Abstraction serves as a bridge for connecting control theory and formal methods in the sense that hybrid control
design for dynamical systems and high-level specifications
can be done using finite abstractions of these systems [1,
21]. There has been a rich literature on computing abstractions for linear and nonlinear dynamical systems in the past
decade (see, e.g., [10, 13, 14, 16, 17, 23, 25]). Early work on
abstraction focuses on constructing symbolic models that
are bisimilar (equivalent) to the original system. The seminal work in [22] shows that bisimilar symbolic models exist
for controllable linear systems. As a result, existence of controllers for such systems to meet linear-time properties (such
as those specified by linear temporal logic [6]) is decidable.

For nonlinear systems that are incrementally stable [3], it
is shown in [16] that approximately bisimilar models can
be constructed (see also [10], for construction of approximately bisimilar models for switched systems, and [9] for
its use in control synthesis). The work in [25] considered
symbolic models for nonlinear systems without stability assumptions, in which it is shown that symbolic models that
approximately alternatingly simulate the sample-data representation of a general nonlinear control system can be
constructed. The work in [17] and [23] both proposes computational procedures for constructing finite abstractions of
discrete-time nonlinear systems. The abstraction techniques
in [17, 23, 25] are conservative and sound in the sense that
they are useful in the design of provably correct controllers,
but do not necessarily yield a feasible design because the
computational procedures for constructing abstractions for
potentially unstable nonlinear systems are not complete.
Robustness is a central property to consider in control
design, because all practical control systems need to be robust to imperfections in all aspects of control design and
implementation, such as modelling, sensing, computation,
communication, and actuation. For abstraction-based control design, how to preserve robustness poses a particular
challenge because the hierarchical control design approach
based on abstraction often use quantized state measurements (modelled as symbolic states in the abstraction) to
compute appropriate control signals. Because of the state
quantizers by definition are discontinuous, special attention
is required to ensure that the resulting design is actually
robust to measurement errors and disturbances. The work
in [13] (see also [14]) proposes a novel notion of abstractions that are equipped with additional robustness margins
to cope with different types of uncertainties in modelling,
such as measurement errors, delays, and disturbances. The
work in [18] (see also [19]) defines a new notation of system
relations for abstraction-based control design. By explicitly
considering the interconnection of state quantizers and feedback controllers, it is shown that the new system relation can
also be used to design robust controllers against uncertainties and disturbances. The type of abstractions considered
in [13, 14, 18, 19] resemble the approximate alternating simulations considered in [25] for nonlinear systems. These abstractions, nonetheless, are all conservative and sound. To
the best knowledge of the authors, how to compute complete abstractions (or approximately complete) abstractions
for general nonlinear systems without stability assumptions
remains an open problem.
As an attempt to bridge this gap, in this paper, we define

robust abstractions as a system relation from a (possibly infinite) transition system subject to uncertainty to anther transition system. We show that, while this abstraction relation
is to some extent similar to the type of system relations considered in [14,19,25], it also has some subtle differences that
are important for proving the approximate completeness results later in the paper. We show that robust abstractions
are sound in the sense that they preserve robust satisfaction
of linear-time properties. The main contributions of the paper include computational procedures for constructing both
sound and approximately complete robust abstractions for
general discrete-time nonlinear control systems without stability assumptions. We show that such procedures are complete in the sense that, given a concrete discrete-time control
system and an arbitrarily small perturbation of this system,
there exists a finite transition system that robustly abstracts
the concrete system, whereas the perturbed system abstracts
this finite transition system. An important consequence of
this main result asserts that existence of robust controllers
for discrete-time nonlinear systems and linear-time specifications is decidable. Finally, we would like to make clear
upfront that the main point of this paper is not on providing more efficient algorithms for computing abstractions.
Therefore, complexity issues, though important, are not a
concern for the current paper and will be investigated in
future work.
The organization of the paper is very straightforward.
Section 2 presents some background material on transition
systems and define robust abstractions. We highlight some
similarities and subtle differences of the new abstraction relation with several variants of simulation relations in the
literature. Section 3 presents the main results of the paper
on construction of sound and approximately complete robust
abstractions for discrete-time nonlinear control systems. A
numerical example is used to illustrate the effectiveness of
robust abstractions in Section 4. The paper is concluded in
Section 5.
Notation: Let f be a (binary) relation from A to B, i.e.,
f is a subset of the Cartesian product A × B. For each a ∈
A, f (a) denotes the set {b : b ∈ B such that (a, b) ∈ f }; for
each b ∈ B, f −1 (b) denotes the set {a : a ∈ A, (a, b) ∈ f };
for A0 ⊆ A, f (A0 ) = ∪a∈A0 f (a); and for B 0 ⊆ B, f −1 (B) =
∪b∈B 0 f −1 (B). Let g be a relation from A to B and f be a
relation from B to C. The composition of f and g, denoted
by f ◦ g, is a relation from A to C defined by

where
• Q is the set of states;
• A is the set of actions;
• R ⊆ Q × A × Q is the transition relation;
• Π is the set of atomic propositions;
• L : Q → 2Π is the labelling function.
Consider the transition system T above. For each action a ∈ A and q ∈ Q, the a-successor of q, denoted by
PostT (q, a), is defined by

PostT (q, a) = q 0 : q 0 ∈ Q s.t. (q, a, q 0 ) ∈ R .
For each q ∈ Q, the set of admissible actions for q, denoted
by AT (q), is defined by
AT (q) = {a : PostT (q, a) 6= ∅} .
In this paper, we assume that all transition systems have no
terminal states in the sense that AT (q) 6= ∅ for all q ∈ Q.
An execution of T is an infinite alternating sequence of
states and actions
ρ = q0 a0 q1 a1 q2 a2 · · · ,
where q0 is some initial state and (qi , ai , qi+1 ) ∈ R for all
i ≥ 0. The path resulting from the execution ρ above is
Path(ρ) = q0 q1 q2 · · · .
The trace of the execution ρ is defined by
Trace(ρ) = L(q0 )L(q1 )L(q2 ) · · · .
A control strategy for a transition system T is a partial function s : (q0 , q1 , · · · , qi ) 7→ ai that maps the state history to
the next action. An s-controlled execution of a transition
system T is an execution of T , where for each i ≥ 0, the
action ai is chosen according to the control strategy s; scontrolled paths and traces are defined in a similar fashion.

2.2

Uncertainty transition systems

Definition 2. A transition relation ∆ ⊆ Q × A × Q is
called an uncertain transition relation for T = (Q, A, R, Π, L),
if the following two conditions hold:
(i) R ∩ ∆ = ∅;
(ii) for each (q, a, q 0 ) ∈ ∆, there exists some (q, a, q 00 ) ∈ R.

f ◦ g = {(a, c) : ∃b ∈ B s.t. (a, b) ∈ g and (b, c) ∈ f } .
For two sets A, B ⊆ Rn ,
A + B = {c : ∃a ∈ A, ∃b ∈ B s.t. a + b = c}
and A\B = {a : a ∈ A, a 6∈ B}. For a ∈ Rn and B ⊆ Rn ,
a + B = {a} + B. Let |·| denote the infinity norm in Rn and
B denote the unit closed ball in infinity norm centred at the
origin, i.e. B = {x ∈ Rn : |x| ≤ 1}. The dimension of B will
be clear from the context.

2.

TRANSITION SYSTEMS AND ROBUST
ABSTRACTIONS

2.1

Transition systems

Definition 1. A transition system is a tuple
T = (Q, A, R, Π, L),

Definition 3. An uncertain transition system consisting
of T = (Q, A, R, Π, L) as a nominal transition system and ∆
as an uncertain transition relation for T , denoted by T ⊕ ∆,
is defined by
T ⊕ ∆ = (Q, A, R ∪ ∆, Π, L).
It is clear from the above definition that, while ∆ introduces additional transitions for the transition system T , it
does not add more admissible actions for any state. In other
words, for all q ∈ Q, AT (q) = AT ⊕∆ (q).
Since an uncertain transition system is simply a transition system with additional transitions introduced by some
uncertain transition relation, the execution (path, trace),
control strategy, and controlled execution (path, trace) for
an uncertain transition system are defined in the same way
as for a nominal transition system.

2.3

Robust abstractions

We first define a notion of abstraction between transition
systems for control synthesis.
Definition 4. For two transition systems
T1 = (Q1 , A1 , R1 , Π, L1 )
and
T2 = (Q2 , A2 , R2 , Π, L2 ),
a relation α ⊆ Q1 × Q2 is said to be an abstraction from T1
to T2 , if the following conditions are satisfied:
(i) for all q1 ∈ Q1 , there exists q2 ∈ Q2 such that (q1 , q2 ) ∈
α (i.e., α(q1 ) 6= ∅);
(ii) for all (q1 , q2 ) ∈ α and a2 ∈ AT2 (q2 ), there exists a1 ∈
AT1 (q1 ) such that
α(PostT1 (q, a1 )) ⊆ PostT2 (q2 , a2 );

(1)

−1

for all q ∈ α (q2 );
(iii) for all (q1 , q2 ) ∈ α, L2 (q2 ) ⊆ L1 (q1 ).
If such a relation α exists, we say that T2 abstracts T1 and
write T1 α T2 or simply T1  T2 .
We then define robust abstractions as abstractions of uncertain transition systems.
Definition 5. Let ∆ be an uncertain transition relation
for T1 . If there exists an abstraction α from T1 ⊕ ∆ to T2 ,
i.e., T1 ⊕ ∆ α T2 , we say that α is a ∆-robust abstraction
from T1 to T2 and T2 ∆-robustly abstracts T1 . With a slight
abuse of terminology, we sometimes also say that T2 is a
∆-robust abstraction of T1 .
Remark 1. We highlight several differences between the
notation of abstraction proposed in Definition 4 and other
similar system relations in the literature. Apart from the
obvious distinction that, in Definition 4, an explicit model
of the uncertainty is considered (following [24]), the abstraction defined by Definition 4 differs from several variants of
simulation relations in the literature as elaborated below:
Finite abstractions with robustness margins: This notion
of abstractions introduced in [13, 14] is defined by introducing two positive parameters (γ1 , γ2 ), which define the extra
transitions to be added to the abstractions to ensure robustness. Suppose there is a metric d defined on Q1 . Then
finite abstractions with robustness margins (γ1 , γ2 ) amount
to defining

abstraction relation on a general Kripke structure, whereas
the work in [13, 14] defines concrete abstractions from ordinary differential/difference equations with inputs to finite
transition systems.
Feedback refinement relations [18, 19]: Similar to [13, 14],
the abstraction relation considered in [18, 19] also requires
that, for each (q1 , q2 ) ∈ α, the admissible actions for each
q2 is a subset of the admissible actions for q1 . In Definition
4, for each (q1 , q2 ) ∈ α, it is not required that AT2 (q2 ) ⊆
AT1 (q1 ), i.e., the admissible actions for q1 do not have to
be a subset of the admissible actions for q2 . This difference
enables us to formulate and prove the approximate completeness results later in this paper (Section 3.3). Note that,
when AT2 (q2 ) ⊆ AT1 (q1 ), condition (1) can be simplified to:
for each (q1 , q2 ) ∈ α and every a ∈ AT2 (q2 ),
α(PostT1 (q1 , a)) ⊆ PostT2 (q2 , a).

In other words, the same action a used by q2 is assumed
to be available (and used) for all q1 ∈ α−1 (q2 ), because
AT2 (q2 ) ⊆ AT1 (q1 ).
Alternating simulations [16,25]: The notion of alternating
simulations [16, 25] stipulates that, for each (q1 , q2 ) ∈ α and
every a2 ∈ AT2 (q2 ), there exists a1 ∈ AT2 (q1 ) such that,
for every q10 ∈ PostT1 (q1 , a1 ), there exists some state q20 ∈
PostT2 (q2 , a2 ) such that (q10 , q20 ) ∈ α. In other words, for
each (q1 , q2 ) ∈ α and every a2 ∈ AT2 (q2 ), there exists a1 ∈
AT1 (q1 ) such that
α(q10 ) ∩ PostT2 (q2 , a2 ) 6= ∅,

for all
∈ PostT1 (q1 , a1 ), as articulated in [18, 19]. Clearly,
(3) is a weaker condition than (1) or (2), unless α is singlevalued. Furthermore, and more importantly, (3) does not
stipulate the use of the same action a1 for all q ∈ α−1 (q2 ),
i.e., a1 may depend on q (concrete states corresponding to
q2 ). A consequence of the latter is that, to implement the
controller, one needs knowledge of the concrete state rather
than the abstract (symbolic) state alone.
We use a simple example to illustrate the differences discussed above.
Example 1. Consider three transition systems
Ti = (Qi , Ai , Ri , Π, Li ),

q∈α−1 (q2 )

⊆ PostT2 (q2 , a2 )
is essentially the over-approximation (of transitions) condition in [13, 14]. The main difference lies in that Definition 4
does not assume that a metric is defined on Q1 and the uncertainty model is not restricted to that defined by level sets
of the distance function. Furthermore, here we define the

i = 1, 2, 3,

where Q1 = {x0 , x1 , x2 }, Q2 = Q3 = {q0 , q1 }, A1 = {a, b},
A2 = A3 = {1, 2, 3}, Π = {Initial, Goal}, L1 (x0 ) = L1 (x1 ) =
L2 (q0 ) = L3 (q0 ) = {Initial}, and L1 (x2 ) = L2 (q1 ) = L3 (q1 ) =
{Goal}. The transition relations are shown in Figure 1.

x2

a

d(q1 , q) ≤ γ1 , d(q10 , q 0 ) ≤ γ2 }\R1 .

q∈α−1 (q2 )

(3)

q10

∆ = {(q, a, q 0 ) : ∃(q1 , a, q10 ) ∈ R1 s.t.
To establish T1 ⊕ ∆ α T2 , condition (1), which can be
equivalently written as
[
[
α(PostT1 ⊕∆ (q, a1 )) = α(
PostT1 ⊕∆ (q, a1 ))

(2)

b
a

x0

2
a

q1

3

2

b

1

q0

3

1 3

2 3

x1

q1

1

q0

Figure 1: Transition systems T1 (left), T2 (middle),
and T3 (right).
Define an abstraction relation from T1 to T2 by
α = {(x0 , q0 ), (x1 , q0 ), (x2 , q1 )} .
Then it can be easily verified that (3) is satisfied and α is an
alternating simulation from T1 to T2 . In fact, we can check

that, for (x0 , q0 ) ∈ α, and action 1 ∈ A2 , there exists a ∈ A1
such that
α(PostT1 (x0 , a)) = α({x0 }) = {q0 } = PostT2 (q0 , 1),
which implies (3). Similarly, for (x0 , q0 ) ∈ α, and action
2 ∈ A2 , there exists b ∈ A1 such that

(i) For all q1 ∈ Q, α3 (q1 ) is non-empty, because α1 (q1 ) is
non-empty and α2 (q2 ) is non-empty for any q2 ∈ Q2 .
(ii) For any (q1 , q3 ) ∈ α3 , there exists q2 ∈ Q2 such that
(q1 , q2 ) ∈ α1 and (q2 , q3 ) ∈ α2 . For any q3 ∈ AT3 (q3 ),
there exists a2 ∈ AT2 (q2 ) such that

α(PostT1 (x0 , b)) = α({x2 }) = {q1 } = PostT2 (q0 , 2),

α2 (PostT2 (q, a2 )) ⊆ PostT3 (q3 , a3 ),

which also implies (3). For (x2 , q1 ) ∈ α, and action 3 ∈ A2 ,
there exists a ∈ A1 such that

for all q ∈ α2−1 (q3 ). For a2 ∈ AT2 (q2 ), there exists
a1 ∈ AT1 (q1 ) such that

α(PostT1 (x2 , a)) = α({x2 }) = {q1 } ⊆ {q0 , q1 } = PostT2 (q1 , 3),
which implies (3). The rest can be checked in a similar fashion.
Suppose that one needs to design a control strategy for T1
such that all controlled executions of T1 starting from the
’Initial’ set will eventually reach the ’Goal’ set. Then, while
one can find such a control strategy for T2 , to implement
this strategy on T1 , however, T1 needs to be able to discriminate x0 and x1 and choose the appropriate actions (b for
x0 and a for x1 ). This is not the case if only symbolic state
information from the abstraction is available.
Note that, according to Definition 4, we do not have T1 α
T2 because, for (x0 , q0 ) ∈ α and action 1 ∈ A2 , we have
[
α(PostT1 (x, a)) = α({x0 } , {x2 })

α1 (PostT1 (q, a1 )) ⊆ PostT2 (q2 , a2 ),
for all q ∈ α1−1 (q2 ). It follows that
[
α3 (PostT1 (q, a1 ))
q∈α−1
3 (q3 )

=
⊆

α(PostT1 (x, b)) = α({x1 } , {x2 })
= {q0 , q1 } 6⊆ {q0 } = PostT2 (q0 , 1),

Thus, (1) does not hold for either action a or b.
We can check that T1 α T3 . Because the set of actions
in T2 (and T3 ) is not a subset of the actions of T1 (in fact
there are more actions in T2 and T3 than T1 ), α does not
provide an abstraction relation from T1 to T2 or from T1 to
T3 in the strict sense of the notions of simulation relations
considered in [13, 14, 18, 19].
To consider a robust abstraction for T1 , let ∆ = {(x2 , a, x1 )}.
Then it can be verified that the transition system T3 is also
a ∆-robust abstraction of T1 .
We will state some immediate results that follow from
Definition 4.
Proposition 1. Let T be a transition system and ∆ be
an uncertain transition relation for T . Then T  T ⊕ ∆.
Proof. Let T = (Q, A, R, Π, L). It is straightforward to
check by Definitions 2 and 4 that the identity relation from
Q to Q defines a ∆-robust abstraction from T to T ⊕ ∆.
Setting ∆ = ∅, a special case of Proposition 1 asserts that
T  T for any transition system. It is also straightforward
to verify that abstraction relations are transitive in the following sense.
Proposition 2. Let Ti (i = 1, 2, 3) be transition systems
and ∆ be an uncertain transition relation for T1 . If T1 α1
T2 and T2 α2 T3 , then T1 α2 ◦α1 T3 .
Proof. Let α3 = α2 ◦ α1 . We verify that conditions (i)–
(iii) of Definition 4 are satisfied:

[

α2 (PostT2 (q, a2 ))

q∈α−1
2 (q2 )

⊆ PostT3 (q3 , a3 ).
(iii) For any (q1 , q3 ) ∈ α3 , there exists q2 ∈ Q2 such that
(q1 , q2 ) ∈ α1 and (q2 , q3 ) ∈ α2 . Hence
L3 (q3 ) ⊆ L2 (q2 ) ⊆ L1 (q1 ).

= {q0 , q1 } 6⊆ {q0 } = PostT2 (q0 , 1),

x∈α−1 (q0 )

α2 ◦ α1 (PostT1 (q, a1 ))

q∈α−1
3 (q3 )

x∈α−1 (q0 )

[

[

2.4

Soundness of abstractions

In this section, we prove that abstractions given by Definition 4 are sound in the sense of preserving realizability of
linear-time properties.
A linear-time (LT) property [6] over a set of atomic propositions Π is a subset of (2Π )ω , which is the set of all infinite
words over the alphabet 2Π , defined by
n
o
(2Π )ω = A0 A1 A2 · · · : Ai ∈ 2Π , i ≥ 0 .
A particular class of LT properties can be conveniently specified by linear temporal logic (LTL [15]). This logic consists
of propositional logic operators (e.g., true, false, negation
(¬), disjunction (∨), conjunction (∧) and implication (→)),
and temporal operators (e.g., next ( ), always (2), eventually (3), until (U) and weak until (W)).
The syntax of LTL over a set of atomic propositions Π is
defined inductively follows:
• true and false are LTL formulae;
• an atomic proposition π ∈ Π is an LTL formula;
• if ϕ and ψ are LTL formulas, then ¬ϕ, ϕ ∨ ϕ, ϕ, and
ϕUϕ are LTL formulas.
The semantics of LTL is defined on infinite words over the
alphabet 2Π . Given a sequence σ = A0 A1 A2 · · · in 2Π , we
define σ, i  ϕ, meaning that σ satisfies an LTL formula ϕ
at position i, inductively as follows:
• σ, i  true;
• σ, i  π if and only if π ∈ Ai ;
• σ, i  ¬ϕ if and only if σ, i 2 ϕ;
• σ, i  ϕ1 ∨ ϕ2 if and only if σ, i  ϕ1 or σ, i  ϕ2 ;
• σ, i  ϕ if and only if σ, i + 1  ϕ;
• σ, i  ϕ1 Uϕ2 if and only if there exists j ≥ i such that
σ, j  ϕ2 and σ, k  ϕ1 for all i ≤ k < j;

We write σ  ϕ, and say σ satisfies ϕ, if σ, 0  ϕ. An
execution ρ of a transition system T is said to satisfy an
LTL formula ϕ, written as ρ  ϕ, if and only if its trace
Trace(ρ)  ϕ. Given a control strategy s for T , if all scontrolled executions of T satisfy ϕ, we write (T , s)  ϕ.
If such a control strategy s exists, we also say that ϕ is
realizable for T .
Remark 1. For technical reasons, we assume that all
LTL formulas have been transformed into positive normal
form [6, Chapter 5], where all negations appear only in front
of the atomic propositions and only the following operators are allowed ∧, ∨, , U, and W (defined by ϕWψ =
(ϕUψ)∨2ϕ. We further assume that all negations of atomic
propositions are replaced by new atomic propositions.
Definition 6. Given an abstraction relation α from T1
to T2 and a control strategy µi for Ti (i = 1, 2), µ1 is called
α-implementation of µ2 , if, for each n ≥ 0,
un = µ1 (x0 , x1 , x2 , · · · , xn )
is chosen according to
an = µ2 (q0 , q1 , q2 , · · · , qn )
in such a way (as guaranteed by Definition 4 for T1 α T2 )
that
α(PostT1 (x, un )) ⊆ PostT2 (qn , an )
for all x ∈ α

−1

(qn ), where qn ∈ α(xn ).

3.

ROBUST DECIDABILITY OF DISCRETETIME CONTROL SYNTHESIS

In this section, we investigate robust abstractions of discretetime nonlinear systems modelled by nonlinear difference equations with inputs. We establish computational procedures
for constructing sound and approximately complete robust
abstractions for this class of control systems under very mild
conditions.

3.1

Perturbed discrete-time control systems as
uncertain transition systems

A discrete-time control system is modelled by a difference
equation of the form
x(t + 1) = f (x(t), u(t)),
n

m

(4)
n

m

where x(t) ∈ X ⊆ R , u(t) ∈ U ⊆ R , and f : R × R →
Rn .
A solution to (4) is an alternating sequence of states and
control inputs of the form
x(0)u(0)x(1)u(1)x(2)u(2) · · · ,
such that (4) is satisfied.
A control strategy for (4) is a partial function
σ : (x(0), · · · , x(t)) 7→ u(t)
for all t = 0, 1, 2, · · · , which maps the state history up to
time t to the control input u(t) at time t.

We end this section by stating a soundness result for abstractions.

Definition 7. The discrete-time control system (4) can
be written as a transition system of the form

Theorem 1. Suppose that α is an abstraction from T1 to
T2 , i.e., T1 α T2 and and let ϕ be an LTL formula. If
there exists a control strategy µ2 for T2 such that (T2 , µ2 ) 
ϕ, then there exists a control strategy µ1 , which is an αimplementation of µ2 , for T1 such that (T1 , µ1 )  ϕ.

S = (QS , AS , RS , Π, LS )

Proof. Let
T1 = (Q1 , A1 , R1 , Π, L1 )
and
T2 = (Q2 , A2 , R2 , Π, L2 ).
We show that, by Definitions 4 and 6, a µ1 -controlled path
of T1 always leads to a µ2 -controlled path of T2 . Suppose
we start with xk ∈ Q1 and let qk be arbitrarily chosen from
α(xk ), where k ≥ 0. Suppose ak = µ2 (q0 , q1 , q2 , · · · , qk )
and uk = µ1 (x0 , x1 , x2 , · · · , xk ). Since α(PostT1 (xk , uk )) ⊆
PostT2 (qk , ak ), we know that for any qk+1 ∈ α(xk+1 ) and
xk+1 ∈ PostT1 (xk , uk ), we have qk+1 ∈ PostT2 (qk , ak ). This
implies that (qk , ak , qk+1 ) is a valid transition in T2 and
therefore, by induction, q0 q1 q2 · · · is a µ2 -controlled path of
T2 , if x0 x1 x2 · · · is a µ1 -controlled path of T1 . Furthermore,
by Definitions 4, we have L2 (qk ) ⊆ L1 (xk ) for all k ≥ 0.
Since the trace of q0 q1 q2 · · · satisfies ϕ, we know that the
trace of x0 , x1 , x2 · · · also satisfies ϕ.
Based on the proof, it is clear that an abstraction relation preserves not only temporal logic specifications but
also linear-time properties in general, because we essentially
proved that the controlled traces of T1 are included in the
controlled traces of T2 (in fact, trace inclusion is equivalent
to preservation of LT properties [6, Theorem 3.15]).

(5)

by defining
• QS = X ∪ {X c };
• AS = U ;
• (x, u, x0 ) ∈ RS if and only if one of the following holds:
(i) x0 = f (x, u) and x, x0 ∈ X; (ii) x0 = X c and
f (x, u) 6∈ X; (iii) x0 = x = X c ;
• Π is a set of atomic propositions on QS and in ∈ Π;
• LS : QS → 2Π is a labelling function satisfying in ∈
LS (q) for q 6= X c and in 6∈ LS (X c ).
The state X c and label in are introduced to precisely encode
if an out-of-domain transition takes place.
We now introduce an uncertainty model for system (4).
Definition 8. Consider system (4) subject to uncertainties of the form
x(t + 1) = f (x(t), u(t)) + w(t),

(6)

where w(t) ∈ δB for some δ ≥ 0. Define ∆δ to consist of
transitions (x, u, x0 ) 6∈ RS such that one of the following
holds: (i) x0 ∈ f (x, u) + δB and x, x0 ∈ X; (ii) x0 = X c and
f (x, u) + w 6∈ X for some w ∈ δB.
Clearly, S ⊕ ∆δ defined together by Definitions 7 and 8
exactly models (6) as summarized in the following proposition.
Proposition 3. Each solution of (6) that stays in X is
an execution of S ⊕∆δ . Conversely, each execution of S ⊕∆δ
that stays in X is also a solution of (6).

Proof. This is straightforward to verify. Denote
ρ = x(0)u(0)x(1)u(1)x(2)u(2) · · · .
If ρ is a solution of (6) such that x(t) ∈ X for all t ≥ 0. Then
there exists w(0)w(1) · · · such that x(t + 1) = f (x(t), u(t)) +
w(t), where w(t) ∈ δB for all t ≥ 0, which implies that
(x(t), u(t), x(t + 1)) ∈ RS ∪ ∆δ . Thus ρ is also an execution
of S ⊕∆δ . Now suppose that ρ is an execution of S ⊕∆δ such
that x(t) ∈ X for all t ≥ 0. Then x(t + 1) = f (x(t), u(t)) +
w(t), where w(t) ∈ δB for all t ≥ 0. This shows that ρ is a
solution of (6).
Because of this proposition, in the sequel, when proving
soundness results, we always assume that out-of-domain solutions and paths are taken care of by enforcing the solutions
and paths to stay in the domain through a safety specification, i.e., by including 2(in) in the specification.

3.2

Soundness of robust abstractions for discretetime control systems

Corollary 1. Suppose there exists a transition system
T such that S ⊕ ∆δ α T , where S and ∆δ are defined by
Definitions 7 and 8. Let ϕ be an LTL formula over Π. If
there exists a control strategy µ for T such that (T , µ) 
ϕ, then there exists a control strategy κ, which is an αimplementation of µ, for S ⊕ ∆δ such that (S ⊕ ∆δ , κ)  ϕ.
Proof. It follows directly from Theorem 1.

x̂(k + 1)
= x(k + 1) + e(k + 1)
= f (x(k), u(k)) + e(k + 1)
= f (x̂(k), u(k)) + (f (x(k), u(k)) − f (x̂(k), u(k))) + e(k + 1).
Since f is L-Lipschitz continuous in both arguments on the
compact set (X + εB) × U , the above equation shows that

It is interesting to note that (S ⊕ ∆δ , κ)  ϕ implies that
solutions of (4) robustly satisfy ϕ in terms of not only additive disturbances modelled by (6), but also other types of
uncertainties such as measurement errors. To illustrate this,
consider a scenario where the controller κ is implemented on
a system with measurement errors. We assume that this error is bounded, i.e., for each x(t) ∈ Rn , its measurement is
given by
x̂(t) = x(t) + e(t),

Proof. We have Ŝ ⊕ ∆δ α T . The goal is to show
that, despite the measurement errors, κ-controlled traces
of S are a subset of the κ-controlled traces of (Ŝ, ∆) and
therefore satisfies ϕ. Starting from x(0), let x̂(0) be the
measurement taken for x(0). Suppose that an action u(0) =
κ(x̂(0)) = µ(q0 ) is chosen by κ, where q0 ∈ α(x̂(0)). Let
L1 be the labelling function for T . Then L1 (q0 ) ⊆ L̂(x̂(0))
by the definition of the robust abstraction. Since L̂ is the
ˆ + εB, it follows that
ε-strengthening of L and x(0) ∈ x(0)
L1 (q0 ) ⊆ L̂(x̂(0)) ⊆ L(x(0)).
We suppose by induction that L1 (qk ) ⊆ L(x(k)) holds for
some k ≥ 0, where qk ∈ α(x̂(k)) and x̂(k) ∈ x(k) + εB.
The action at time k is given by u(k) = κ(x̂(0), · · · , x̂(k)),
which implements ak = µ(q0 , · · · , qk ) in the sense of Definition 6. The next state under u(k) is given by x(k + 1) =
f (x(k), u(k)), whose measurement is x̂(k + 1) = x(k + 1) +
e(k + 1) ∈ x(k + 1) + εB. Hence L1 (qk+1 ) ⊆ L̂(x̂(k + 1))
implies L1 (qk+1 ) ⊆ L̂(x̂(k + 1))L(x(k + 1)). Thus, L(qk ) ⊆
L(x(k)) for all k ≥ 0.
We show that (qk , ak , qk+1 ) is a valid transition in T . Note
that

x̂(k + 1) ∈ f (x̂(k), u(k)) + (L + 1)εB ⊆ f (x̂(k), u(k)) + δB,
because (L + 1)ε ≤ δ. Hence, by the choice of u(k) by κ
(which is an α-implementation of µ), we have
qk+1 ∈ α(x̂(k + 1))
⊆ α(f (x̂(k), u(k)) + δB)
⊆ α(PostŜ⊕∆ (x̂(k), u(k)))

(7)

where e(t) ∈ εB for some ε > 0. To make the control strategy κ for (4) robust to measurement errors like (7), we can
simply strengthen the labeling function L of S as follows.
A labelling function L̂ : Rn → 2Π is said to be the εstrengthening of another labelling function L : Rn → 2Π ,
if π ∈ L̂(x) if and only if π ∈ L(y) for all y ∈ x + εB.
The remaining technical results of the paper rely on the
following assumption.
Assumption 1. The function f : Rn × Rm is locally Lipschitz continuous in both arguments. The sets X and U are
compact.
The above assumption on f is very mild and is satisfied
as long as the function f : Rn × Rm is differentiable with
respect to both variables.
Proposition 4. Let Ŝ = (Q, A, R, Π, L̂), which is obtained from S in Definition 7 by replacing L with its εstrengthening L̂. Suppose that the assumptions of Corollary
1 hold with Ŝ in place of S. Then (S, κ)  ϕ, subject to measurement errors described in (7), provided that (L + 1)ε ≤ δ,
where L is the uniform Lipschitz constant for both variables
of f on the compact set (X + εB) × U .

⊆ PostT (qk , ak ),
where x̂(k) ∈ α−1 (qk ), which shows that (qk , ak , qk+1 ) is
a valid transition in T and therefore q0 q1 q2 · · · is a valid
path for T . Since the trace of this path satisfies ϕ and
L1 (qk ) ⊆ L(x(k)) for all k ≥ 0, it follows that the trace of
x(0)x(1)x(2) · · · also satisfies ϕ.
Remark 2. The soundness result above states that to
cope with measurement errors, we only need to choose δ
sufficiently large such that (L + 1)ε ≤ δ and strengthen the
labelling function by a factor of ε. This condition simplifies the two robustness margins (γ1 , γ2 ) considered in the
work [13, 14] and also does not require that the abstraction
relation to be non-deterministic in order to be robust with
respect to measurement errors as stated in [19, Section VI.6].

3.3

Approximate completeness of robust abstractions for discrete-time control systems

In this section, we show that, under Assumption 1, computing robust abstractions for the discrete-time control system (4) is approximately complete, in the sense that, for
arbitrary numbers 0 ≤ δ1 < δ2 , we can find a finite transition system T such that S ⊕ ∆δ1  T  S ⊕ ∆δ2 , where S
and ∆δi (i = 1, 2) are defined in Definitions 7 and 8. This

result is made precise by the following theorem, which we
present as the main result of the paper.
Theorem 2. For any numbers 0 ≤ δ1 < δ2 , let ∆δi (i =
1, 2) be given by Definition 8 with δ = δi . For any numbers
0 ≤ ε1 < ε2 , let LSi (i = 1, 2) be the εi -strengthening of LS .
Let
Si = (QS , AS , RS ∪ ∆δi , Π, LSi ),

i = 1, 2.

Then there exists a finite transition system T such that
S1  T  S2 .

(8)

To prove Theorem 2, we need the following lemma on overapproximation of the reachable set of a box in Rn under a
nonlinear map.
Lemma 1. Fix any δ > 0, any box (also called an interval
or a hyperrectangle) [x] ⊆ Rn , and any u ∈ U . For all ε > 0,
there exists a finitely terminated algorithm to compute an
over-approximation of the reachable set of [x] under (6), i.e.,
the set

Algorithm 1 Computation of an over-approximation of
Reach(6) ([x], u) (Lemma 1)
Input: [x], δ, ε > 0, the Lipschitz constant L for f (·, u), and
a centred convergent inclusion function [fu ] for f (·, u)
1: List ← [x]
2: Y ← ∅
3: while List 6= ∅ do
4:
[y] ← F irst(List)
5:
List ← List \ {[x]}
ε
then
6:
if w([y]) ≤ 2L
7:
[z] ← [fu ]([y]) + δB
8:
Y ← Y ∪ {[z]}
9:
else
10:
{Lef t[y], Right[y]} = Bisect([y])
11:
List ← List ∪ {Lef t[y], Right[y]}
12: Y ← ∪[z]∈Y [z]
\ (6) ([x], u)
13: return Y = Reach

Proof of Theorem 2. The proof is constructive and we
construct a finite transition system

Reach(6) ([x], u) = f ([x], u) + δB,

T = (QT , AT , RT , Π, LT )

such that
\ (6) ([x], u) ⊆ Reach(6) ([x], u) + εB,
Reach(6) ([x], u) ⊆ Reach
\ (6) ([x], u) is the computed over-approximation
where Reach
given as a union of boxes.
Proof. This is a well-known result in interval analysis,
known as outer approximation of the image set of a function.
It can be proved, for example, using the results in [11, Chapter 3]. Here we include a proof for completeness. Let IRn
denote the set of all boxes in Rn . Let [fu ] : IRn → IRm be a
convergent inclusion function [11] of f (·, u), which satisfies
the following two conditions:
• f ([y], u) ⊆ [fu ]([y]) for all [y] ∈ IRn ;
• limw([y])→0 w([fu ]([y])) = 0,
where w([y]) is the width of [y], given by max1≤i≤n {yi −yi } if
we write [y] = [y1 ]×· · ·×[yn ] ⊆ Rn and [yi ] = [y i , y i ] ⊆ R for
i = 1, · · · , n. Without loss of generality, assume that ε < 1.
Because f is L-Lipschitz continuous on [x] for some L > 0,
we can find an inclusion function such that w([fu ]([y])) ≤
Lw([y]) for any subintervals of [x]. We mince the interval [x]
into subintervals such that the largest width of among these
ε
subintervals is smaller than 2L
. For each such interval [y], we
evaluate [fu ]([y]) and obtain the interval [z] = [fu ]([y]) + δB.
Let Y denote the collection of all such intervals1 and let Y
be its union. We claim that
\ (6) ([x], u)
Y = Reach
satisfies the requirement of this lemma. This is clearly true
because, for each interval [z] = [fu ]([y])+δB, we have f ([y])+
δB ⊆ [z] and the distance from [z] to the true reachable set
Reach(6) ([x], u) is bounded by w([fu ]([y])) ≤ L · w([y]) ≤ 2ε .
The proof for Lemma 1 is also summarized in pseudo code
format in Algorithm 1.
1
Such a collection Y is called a non-regular paving of Rn ,
which can be regularized [11, Chapter 3] to reduce the number of boxes and hence reduce complexity, but this is not
necessary for our purpose.

as follows.
For a positive integer k, let Zk denote the k-dimensional
integer lattice, i.e., the set of all k-tuples of integers. For
parameters η > 0 and µ > 0 (to be chosen later), define
[Rn ]η = ηZn , [Rm ]µ = µZm ,

where µZk = µz : z ∈ Zk (for k = n, m). Define a relation α from QS to [Rn ]η ∪ {X c } by


x
(x, q) : q = ηb c, x ∈ X ∪ {(X c , X c )} ,
η
where b·c is the floor function (i.e., bxc = (bx1 c, · · · , bxn c)
and bxi c gives the largest integer
).
n less than or equal to xi o
Let QT be α(QS ) and AT =

a : ∃u ∈ AS s.t. a = µb µu c

(which are both non-empty by definition and are finite because X and U are compact). Note that this gives a deterministic relation in the sense that α(x) is single-valued for
all x. It is straightforward to verify that
α−1 (α(B)) ⊆ B + ηB,
n

(9)

c

for any set B ⊆ R ∪ X , with the slight abuse of notation
that X c + x = X c for any x ∈ Rn .
We next construct RT . For each q ∈ QT and a ∈ AT ,
denote by
[
ReachS1 (α−1 (q), a) =
PostS2 (x, a).
x∈α−1 (q)

We let (q, a, q 0 ) be included in RT if and only if
\ S1 (α−1 (q), a)),
q 0 ∈ α(Reach
i.e.,
\ S1 (α−1 (q), a)),
PostT (q, a) = α(Reach

(10)

\ S1 (α−1 (q), a) is computed from Lemma 1 by
where Reach
setting [x] = α−1 (q), u = a, and δ = δ1 . In particular, we set

\ (6) ([x], u), if Reach
\ (6) ([x], u) ⊆
\ S1 (α−1 (q), a) = Reach
Reach
X, and
\ (6) ([x], u) ∪ {X c },
\ S1 (α−1 (q), a) = Reach
Reach
\ (6) ([x], u) 6⊆ X.
if Reach
Then it follows from Lemma 1 that
[
α(
PostS1 (x, a)) ⊆ α(ReachS1 (α−1 (q), a))

ε1 +ε2
]B
2

2
⊆ x + ε2 B, we have π ∈ LS (y) for all y ∈ q + ε1 +ε
B
2
and π ∈ LT (q). Hence, (13) holds. If π ∈ LT (q), then
2
B by the definition of LT .
π ∈ LS (y) for all y ∈ q + ε1 +ε
2
2
Since x+ε1 B ⊆ q+(η+ε1 )B ⊆ q+ ε1 +ε
B, we have π ∈ LS (y)
2
for all y ∈ x + ε1 B and π ∈ LS1 (x). Hence, (14) holds.
We have verified S1  T  S2 by checking all the conditions of Definition 4. The main steps of the proof are also
summarized in pseudo code format in Algorithm 2.

x∈α−1 (q)

\ S1 (α−1 (q), a))
⊆ α(Reach
= PostT (q, a),
which verifies condition (ii) of Definition 4 for S1 α T .
Consider α−1 as a relation from QT to QS . Then for each
x ∈ QS and u ∈ AS , we can choose a = µb µu c ∈ AT such
that
[
α−1 (
PostT (q, a)) = α−1 (PostT (q, a))
q∈α(x)

\ S1 (α−1 (q), a)))
⊆ α−1 (α(Reach
\ S1 (α−1 (q), a) + ηB
⊆ Reach
⊆ ReachS1 (α−1 (q), a) + (η + ε)B.
where we used (10), (9), and Lemma 1. We claim that, if
we can choose η, µ, and ε sufficiently small such that
δ1 + L(η + µ) + η + ε ≤ δ2 ,

(11)

then
ReachS1 (α−1 (q), a) + (η + ε)B ⊆ PostS2 (x, u).

(12)

Note that α−1 (q) ⊆ x + ηB and a ∈ u + µB. We first assume
that X c 6∈ ReachS1 (α−1 (q), a). Without loss of generality,
we can assume that η ≤ 1 and µ ≤ 1. Because f is Lipschitz
continuous in both arguments on the compact set (X + B) ×
(U +B) (we use L to indicate the uniform Lipschitz constant
for both variables on this set), it follows that
ReachS1 (α−1 (q), a) ⊆ f (x, u) + [δ1 + L(η + µ)]B.
Combining the displayed equations above, we obtain
[
α−1 (
PostT (q, a)) ⊆ f (x, u) + δ2 B
q∈α(x)

= PostS2 (x, u),
which verifies condition
S (ii) of Definition 4 for T α S2 ,
because X c ∈ α−1 ( q∈α(x) PostT (q, a)) would also imply
X c ∈ PostS2 (x, u).
Now we define LT . For each q ∈ QT , define
π ∈ LT (q)
2
B. Choose η
if and only if π ∈ LS (x) for all x ∈ q + ε1 +ε
2
ε1 +ε2
sufficiently small such that η + 2 < ε2 . This is possible
because ε2 > ε1 . To verify condition (iii) of Definition 4 for
S1 α T and T α−1 S2 , we need to check that

LS2 (x) ⊆ LT (q)

(13)

LT (q) ⊆ LS1 (x)

(14)

and

for all (x, q) ∈ α. Fix any (x, q) ∈ α. If π ∈ LS2 (x), then
2
B ⊆ x + [η +
π ∈ LS (y) for all y ∈ x + ε2 B. Since q + ε1 +ε
2

Algorithm 2 Computation of an approximately complete
robust abstraction T for S (Theorem 2)
Input: S = (QS , AS , RS , Π, LS ), numbers 0 ≤ δ1 < δ2 and
0 ≤ ε1 < ε 2
1: Set LSi be the εi -strengthening of LS (i = 1, 2)
2: Set ∆δi according to Definition 8 (i = 1, 2)
3: Set Si = (QS , AS , RS ∪ ∆δi , Π, LSi ) (i = 1, 2)
4: Choose rational numbers η ∈ (0, 1) and ε ∈ (0, 1) such
2
that δ1 + L(η + µ) + η + ε ≤ δ2 and η + ε1 +ε
< ε2 , where
2
L is the uniform Lipschitz constant of f on the compact
set (X + B)
o
n × (U + B)

5: Set QT = x ∈ [Rn ]η : ∃x ∈ QS s.t. x = ηb uη c ∪ {X c }
n
o
6: Set AT = a ∈ [Rm ]µ : ∃u ∈ AS s.t. a = µb µu c
7: for all q ∈ QT do
8:
LT (q) ← ∅
9:
for all π ∈ Π do
2
B then
10:
if π ∈ LS (x) for all x ∈ q + ε1 +ε
2
11:
LT (q) ← LT (q) ∪ {π}
12: RT ← ∅
13: for all q ∈ QT do
14:
for all a ∈ AT do
\ (6) (α−1 (q), a)) then
15:
if q 0 ∈ α(Reach
16:
RT ← RT ∪ {(q, a, q 0 )}
17: return T = (QT , AT , RT , Π, LT )

Remark 3. While the disturbance sets are so chosen for
simplicity of presentation, they do not have to be of the
form δB. In fact, if we choose two arbitrary sets W1 and
W2 in place of δ1 B and δ2 B in Definition 8 such that there
exists ε > 0 such that W1 + εB ⊆ W2 , then a completeness
result similar to Theorem 2 can be stated. Furthermore, δ
can be a vector in Rn instead of a scalar, in which case δi B
becomes a hyperrectangle and the condition 0 ≤ δ1 < δ2 is
a componentwise inequality.
Remark 4. In the proof of Theorem 2, we in fact construct a single-valued abstraction relation α. While the main
results of the paper are presented for the case where α can
be multi-valued, it appears, in view of the proof of Theorem
2, that for practice purposes, α may always be chosen to
be deterministic, while still preserving robustness (see also
Remark 2).
Finally, we would like to point out that Theorem 2 shows
that there exists an approximately complete abstraction procedure for discrete-time nonlinear control systems of the
form (4) in the sense that, if a specification ϕ is realizable
for S2 (namely, a δ2 -perturbation of S), then there is a robust abstraction T of S1 , which is a δ1 -perturbation of S,
such that ϕ is realizable for T and hence it is also realizable for S1 . Note that S1 and S2 can be made arbitrarily

close by choosing δ2 close to δ1 and ε2 close to ε1 . Since
the proof of above theorem is constructive, we can algorithmically synthesize a control strategy for S1 by computing
T first and then solving a discrete synthesis problem for T
with the specification ϕ. We summarize this in the following
corollary.

specification. Furthermore, Theorem 2 implies that, for
any 0.05 ≤ δ1 < δ2 , by further refining the abstraction,
we should be able to assert that either the specification is
robustly realizable with a disturbance of size δ1 or the specification is not realizable with a disturbance of size δ2 .

Corollary 2. Let S1 , S2 , and ϕ be as defined in Theorem 2. There is a decision procedure to answer one of the
following two questions:
(i) there exists a control strategy κ (and one can algorithmically construct it) such that (S1 , κ)  ϕ;
(ii) ϕ is not realizable for S2 .

4.5
4
3.5
3

AN EXAMPLE
y position

4.

We use a simple motion planning example to illustrate
our results. Consider a vehicle steering problem, where the
dynamics of the vehicle are given by the so-called bicycle
model [5]. The same example is used for illustration of
abstraction-based control design in [19, 20, 25]. The model
is given by

  
u1 cos(α + x3 )/ cos(α)
ẋ1
ẋ2  =  u1 sin(α + x3 )/ cos(α) 
ẋ3
u1 tan(u2 )

1.5
1
0.5
0

7.5

8

8.5

9

10

Figure 2: A simulated trajectory from a nominal
abstraction that satisfies the specification.

where
y position

AI = [7.6, 0.4, π/2]T ,

4.5

4.5

4

4

3.5

3.5

3

3

2.5

2.5

2

2

AO1 = [8.2, 8.4] × [0, 3.6] × [−π, π],
AO2 = [8.4, 9.4] × [3.4, 3.6] × [−π, π],

1.5

1.5

1

1

AO3 = [9.4, 10] × [2.4, 2.6] × [−π, π].

0.5

0.5

To design a control strategy to realize this specification,
we discretize the model using a sampling time step τ = 0.3.
We first consider the case with no disturbance, i.e., δ = 0.
Using the discretization parameters η = 0.2 and µ = 0.3,
the resulting nominal abstraction consists of 12,880 states
and 3,023,040 transitions. The computation time was 7.3s
for computing the abstraction and 8.6s for solving the synthesis problem on a 2.2GHz Intel Core i7 processor. A feasible trajectory is shown in Figure 4. To design a robust
control strategy, we consider an additive disturbance of size
δ = 0.05 on the right-hand side of the system. We compute a robust abstraction by setting δ1 = 0.05 and η = 0.05.
The resulting robust abstraction consists of 782, 691 states
and 1, 727, 548, 752 transitions. The computation time was
2, 327s for abstraction and 2, 289s for synthesis on the same
processor. A feasible trajectory is shown in Figure 4. Using
the same controller, a simulated trajectory with an additive disturbance of size δ = 0.15 is shown to violate the

9.5

x position

ϕ = AI ∧ (¬AO ) ∧ ♦AG ,

AG = [9, 9.6] × [0, 0.6] × [−π, π],
AO = AO1 ∪ AO2 ∪ AO3 ,

2

y position

where (x1 , x2 , x3 ) = (x, y, θ) and (u1 , u2 ) = (v, ϕ). The
constant b = 1 is the wheel base and a = 0.5 is the distance
between centre of mass and rear wheels. The states consist
of the coordinates of the centre of the mass (x, y) and the
heading angle θ. The controls consist of the wheel speed
v and the steering angle ϕ. The variable α is the angle of
velocity depending on ϕ.
Let X = [7, 10]×[0, 4.5]×[−π, π] and U = [−1, 1]×[−1, 1].
Consider a workspace and a specification given by

2.5

0

7.5

8

8.5

x position

9

9.5

10

0

7.5

8

8.5

x position

9

9.5

10

Figure 3: A valid trajectory (left) obtained from a
robust abstraction with δ = 0.05 and a failed trajectory (right) with disturbance size δ = 0.15.

5.

CONCLUSIONS AND DISCUSSIONS

We proposed a computational framework for designing robust abstractions for control synthesis. It is shown that robust abstractions are not only sound in the sense that they
preserve robust satisfaction of linear-time properties, but
also approximately complete in the sense that, given a concrete discrete-time control system and an arbitrarily small
perturbation of this system, there exists a finite transition
system that robustly abstracts the concrete system and is

abstracted by the perturbed system at the same time. Consequently, the existence of controllers for a general discretetime nonlinear control system and linear-time specifications
is robustly decidable: if a specification is robustly realizable,
there is a decision procedure to find a (potentially less) robust control strategy.
It is interesting to note that the connection between robustness and decidability appeared in different contexts. Recently, the notion of δ-decidability for satisfiability over the
reals [8] and δ-reachability analysis [12] have been proposed
to turn otherwise undecidable problems into decidable ones.
A notion of “robustness implies decidability” was proposed
in early work in [7] for verifying bounded properties for polynomial hybrid automaton and in [4] for reachability analysis
of several simple models of hybrid systems. Finally, the early
work in [2] showed that robust stability is decidable for linear
systems in the context of output feedback stabilization. In
this sense, the current work can serve as an example of “robustness implies decidability” in the context of linear-time
logic control synthesis for nonlinear systems.

6.

ACKNOWLEDGMENTS

This research was supported in part by NSERC Canada
and the University of Waterloo. The author would like
to thank Necmiye Ozay and Yinan Li for stimulating discussions on related topics and the anonymous reviewers for
helpful comments and suggestions.

7.

REFERENCES

[1] R. Alur, T. A. Henzinger, G. Lafferriere, and G. J.
Pappas. Discrete abstractions of hybrid systems.
Proceedings of the IEEE, 88(7):971–984, 2000.
[2] B. Anderson, N. Bose, and E. Jury. Output feedback
stabilization and related problems-solution via
decision methods. IEEE Transactions on Automatic
control, 20(1):53–66, 1975.
[3] D. Angeli et al. A lyapunov approach to incremental
stability properties. IEEE Transactions on Automatic
Control, 47(3):410–421, 2002.
[4] E. Asarin and A. Bouajjani. Perturbed turing
machines and hybrid systems. In Proc. of LICS, pages
269–278. IEEE, 2001.
[5] K. J. Aström and R. M. Murray. Feedback Systems:
An Introduction for Scientists and Engineers.
Princeton University Press, 2010.
[6] C. Baier and J.-P. Katoen. Principles of Model
Checking. MIT Press, 2008.
[7] M. Fränzle. What will be eventually true of
polynomial hybrid automata? In Proc. of TACS,
pages 340–359. Springer, 2001.
[8] S. Gao, J. Avigad, and E. M. Clarke. δ-complete
decision procedures for satisfiability over the reals. In
Proc. of IJCAR, pages 286–300. Springer, 2012.
[9] A. Girard. Controller synthesis for safety and
reachability via approximate bisimulation.
Automatica, 48(5):947–953, 2012.
[10] A. Girard, G. Pola, and P. Tabuada. Approximately
bisimilar symbolic models for incrementally stable
switched systems. IEEE Trans. on Automatic Control,
55:116–126, 2010.
[11] L. Jaulin. Applied Interval Analysis. Springer Science
& Business Media, 2001.

[12] S. Kong, S. Gao, W. Chen, and E. Clarke. dreach:
δ-reachability analysis for hybrid systems. In Proc. of
TACAS, pages 200–205. Springer, 2015.
[13] J. Liu and N. Ozay. Abstraction, discretization, and
robustness in temporal logic control of dynamical
systems. In Proc. of HSCC, pages 293–302, 2014.
[14] J. Liu and N. Ozay. Finite abstractions with
robustness margins for temporal logic-based control
synthesis. Nonlinear Analysis: Hybrid Systems,
22:1–15, 2016.
[15] A. Pnueli. The temporal logic of programs. In Proc. of
FOCS, pages 46–57. IEEE, 1977.
[16] G. Pola, A. Girard, and P. Tabuada. Approximately
bisimilar symbolic models for nonlinear control
systems. Automatica, 44(10):2508–2516, 2008.
[17] G. Reissig. Computing abstractions of nonlinear
systems. IEEE Trans. Automatic Control,
56:2583–2598, 2011.
[18] G. Reissig and M. Rungger. Feedback refinement
relations for symbolic controller synthesis. In Proc. of
CDC, pages 88–94. IEEE, 2014.
[19] G. Reissig, A. Weber, and M. Rungger. Feedback
Refinement Relations for the Synthesis of Symbolic
Controllers. IEEE Transactions on Automatic Control,
to appear, 2016.
[20] M. Rungger and M. Zamani. Scots: A tool for the
synthesis of symbolic controllers. In Proc. of HSCC,
pages 99–104. ACM, 2016.
[21] P. Tabuada. Verification and Control of Hybrid
Systems: A Symbolic Approach. Springer, 2009.
[22] P. Tabuada and G. J. Pappas. Linear time logic
control of discrete-time linear systems. IEEE Trans.
on Automatic Control, 51(12):1862–1877, 2006.
[23] Y. Tazaki and J. Imura. Discrete abstractions of
nonlinear systems based on error propagation analysis.
IEEE Trans. Automatic Control, 57:550–564, 2012.
[24] U. Topcu, N. Ozay, J. Liu, and R. M. Murray. On
synthesizing robust discrete controllers under
modeling uncertainty. In Proc. of HSCC, pages 85–94.
ACM, 2012.
[25] M. Zamani, G. Pola, M. Mazo, and P. Tabuada.
Symbolic models for nonlinear control systems
without stability assumptions. IEEE Transactions on
Automatic Control, 57(7):1804–1809, 2012.

