Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

1

Optimized State Space Grids for Abstractions
Alexander Weber, Matthias Rungger and Gunther Reissig

arXiv:1711.01637v1 [math.OC] 5 Nov 2017

Abstract
The practical impact of abstraction-based controller synthesis methods is currently limited by the immense
computational effort for obtaining abstractions. In this note we focus on a recently proposed method to compute abstractions whose state space is a cover of the state space of the plant by congruent hyper-intervals. The
problem of how to choose the size of the hyper-intervals so as to obtain computable and useful abstractions is
unsolved. This note provides a twofold contribution towards a solution. Firstly, we present a functional to predict the computational effort for the abstraction to be computed. Secondly, we propose a method for choosing
the aspect ratio of the hyper-intervals when their volume is fixed. More precisely, we propose to choose the
aspect ratio so as to minimize a predicted number of transitions of the abstraction to be computed, in order
to reduce the computational effort. To this end, we derive a functional to predict the number of transitions in
dependence of the aspect ratio. The functional is to be minimized subject to suitable constraints. We characterize the unique solvability of the respective optimization problem and prove that it transforms, under appropriate assumptions, into an equivalent convex problem with strictly convex objective. The latter problem
can then be globally solved using standard numerical methods. We demonstrate our approach on an example.
Index Terms
Discrete abstraction, symbolic control, automated synthesis, Djoković-London functional; MSC: Primary,
93B51; Secondary, 93B52, 93C10, 93C30, 93C55, 93C57, 93C65

I. Introduction
The concept of abstraction-based controller synthesis is a fully automated procedure to design
feedback controllers that enforce predefined, possibly complex, specifications on nonlinear control
systems [1], [2]. The procedure comprises three steps [2]. The first step is to transfer the actual control
system (“plant”) together with the predefined specification to an auxiliary control system, known
as abstraction or symbolic model , and an auxiliary specification. In the second step, the auxiliary
control problem is solved. The last step is to refine the obtained controller (“abstract controller”) to
a controller for the actual control problem. The practical impact of the approach is currently limited
by the immense computational effort for the first step, i.e., for obtaining abstractions.
Various methods to reduce the computational effort of this procedure exist in literature, e.g. [3]–
[10]. The methods in [3]–[6] merge the first and second step in previous scheme in order to compute
the abstraction only partially. The methods in [6]–[8] locally refine symbolic models to reduce the
number of required abstract states. In [9], [10] the state space of the plant is not discretized but finite
sequences of inputs are used as abstract states.
This paper is the first to establish a reduction method for abstractions that are based on feedback
refinement relations [1], [11]. Moreover, for the first time, a functional is presented that predicts the
required computational resources for the abstraction to be computed.
Abstractions based on feedback refinement relations can be constructed for plants whose dynamics
are governed by nonlinear differential equations subject to perturbations. Moreover, in contrast to
G. Reissig and A. Weber are with the University of the Federal Armed Forces Munich, Dept. Aerospace Eng., Chair of Control
Eng. (LRT-15), D-85577 Neubiberg (Munich), Germany, http://www.reiszig.de/gunther/, a.weber@unibw.de
M. Rungger is with the Hybrid Control Systems Group at the Department of Electrical and Computer Engineering at the
Technical University of Munich, Germany, matthias.rungger@tum.de
This work has been supported by the German Research Foundation (DFG) under grants no. RE 1249/3-2 and RE 1249/4-1.
This is the accepted version of a paper published in IEEE Trans. Automat. Control, vol. 62, no. 11, pp. 5816-5821, 2017,
DOI:10.1109/TAC.2016.2642794.

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

2

other system relations, the induced controllers for the actual control problem merely consist of the
abstract controller and a static quantizer [1].
The scheme for computing such an abstraction is as follows. First, the n-dimensional real state
space of the plant is discretized by means of a cover to obtain the states of the abstraction, where the
vast majority of the elements of the cover are translated copies of the hyper-interval
 η1 η1 


− 2 , 2 × . . . × − η2n , η2n , η1 , . . . , ηn > 0,
(1)
which are aligned on a uniform grid. Second, attainable sets of the sets in the cover are overapproximated by hyper-intervals to obtain the transitions in the abstraction.
The goal of this work is to provide a heuristic for choosing η1 , . . . , ηn in (1) so as to reduce the
memory and time consumption when computing abstractions for which the volume η1 ·η2 . . . ηn of (1)
is predefined. The key idea here is the minimization of the expected number of transitions. As a first
step towards this goal, we propose to use the functional

Yn 1 
Xn
Ai,j ηj
(2)
E(η) =
pi +
i=1 ηi
j=1

to estimate the number of transitions per abstract state and input symbol in dependence of η =
(η1 , . . . , ηn ) in (1). Here, the nonnegative n × n-matrix A and the n-dimensional nonnegative vector
p depend on the particular plant dynamics and on bounds on disturbances.
In the next step we study the minimization of (2) subject to a constraint that prescribes the volume
of (1). For this, in general, non-convex optimization problem, we characterize the existence of a unique
solution. To this end, we eliminate non-convexity by suitably transforming (2) and show that under
appropriate assumptions the auxiliary optimization problem has strictly convex objective and can be
globally solved by standard numerical methods. These results then allow us to establish the requested
heuristic. We finally demonstrate our approach on an example.
Our results on the functional in (2) recover and extend previous results for the special case p = 0,
which plays a part in diagonal scaling of nonnegative matrices into doubly stochastic form [12], [13].
Some of our results have been announced in [14].

II. Preliminaries
1) Notation: R, R+ and Z denote the sets of real numbers, nonnegative real numbers, and integers,
respectively. [a, b], ]a, b[, [a, b[, and ]a, b] denote closed, open and half-open, respectively, intervals
with end points a and b. [a; b], ]a; b[, [a; b[, and ]a; b] stand for discrete intervals, e.g. [a; b] = [a, b] ∩ Z,
[1; 4[ = {1, 2, 3}, and [0; 0[ = ∅. In Rn , the relations <, ≤, ≥, > are defined component-wise, e.g., a < b
iff ai < bi for all i ∈ [1; n]. For x ∈ Rn we define |x| = (|x1 |, . . . , |xn |). For a, b ∈ (R∪{∞, −∞})n , a ≤ b,
the closed hyper-interval Ja, bK is defined by Ja,P
bK = Rn ∩ ([a1 , b1 ] × · · · × [an , bn ]). h·|·i stands for the
standard Euclidean inner product, i.e., hx|yi = ni=1 xi yi . k·kp stands for the usual p-norm, p ∈ [1, ∞].
f : A ⇒ B denotes a set-valued map of A into B, whereas f : A → B denotes an ordinary map; see
[15]. If f is set-valued, then f is strict if f (a) 6= ∅ for every a. We identify set-valued maps f : A ⇒ B
with binary relations on A × B, i.e., (a, b) ∈ f iff b ∈ f (a). f ◦ g denotes the composition of f and g,
(f ◦ g)(x) = f (g(x)).
We denote the vector (1, . . . , 1) ∈ Rk by 1 and the identity map X → X : x 7→ x by id. The
dimension k and the domain of definition X respectively will always be clear from the context. A
cover of a set X is a set of subsets of X whose union equals X.
n×n
2) nonnegative matrices: A matrix A is nonnegative if A ∈ R+
and it is essentially nonnegative
n×n
n×n
if A ∈ R
and Ai,j ≥ 0 whenever i 6= j. A matrix A ∈ R
is irreducible if for any r, s ∈ [1; n],
r 6= s there exist distinct indices i1 , . . . , im ∈ [1; n] satisfying i1 = r, im = s and Aik ,ik+1 > 0 for all
k ∈ [1; m[. Otherwise, A is reducible.

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

3

III. Computation of abstractions
This section gives a brief exposition of the method to compute abstractions from [1]. We consider
control systems governed by nonlinear differential inclusions of the form
˙ ∈ f (ξ(t), u) + J−w, wK ,
ξ(t)

(3)

where f : Rn × Ū → Rn , Ū ⊆ Rm is nonempty, f (·, u) is locally Lipschitz for all u ∈ Ū , and w ∈ Rn+ is
a component-wise bound on perturbations to the dynamics of the control system. For τ > 0 a solution
of (3) on [0, τ ] with (constant) input u ∈ Ū is an absolutely continuous function ξ : [0, τ ] → Rn that
fulfills (3) for almost every t ∈ [0, τ ] [16].
We formalize sampled versions of control systems (3) in a notion of system as given below.
III.1 Definition. A system is a triple (X, U, F ), where X and U are nonempty sets and F : X × U ⇒
X.
We call the sets X and U the state and input alphabet, respectively. The map F is called the
transition function.
III.2 Definition. Let S = (X, U, F ) be a system and τ > 0. We say that S is the sampled system
associated with the control system (3) and the sampling time τ , if X = Rn , U = Ū and the following
holds: x1 ∈ F (x0 , u) iff there exists a solution ξ of (3) on [0, τ ] with input u so that ξ(0) = x0 and
ξ(τ ) = x1 .
We relate two systems to each other by feedback refinement relations. We introduce this concept
as follows.
For a system S = (X, U, F ) and x ∈ X let
US (x) = {u ∈ U | F (x, u) 6= ∅}.
III.3 Definition. Let Si = (Xi , Ui , Fi ), i ∈ {1, 2} be two systems such that U2 ⊆ U1 . A feedback
refinement relation from S1 to S2 is a strict relation Q ⊆ X1 × X2 satisfying
(i) US2 (x2 ) ⊆ US1 (x1 ),
(ii) u ∈ US2 (x2 ) =⇒ Q(F1 (x1 , u)) ⊆ F2 (x2 , u)
for all (x1 , x2 ) ∈ Q.
We write S1 4Q S2 if Q is a feedback refinement relation from S1 to S2 . If S1 4Q S2 we say that
S2 is an abstraction for S1 .
A feedback refinement relation Q from S1 to S2 associates states of S1 with states of S2 and imposes
conditions on the images of the transition functions at associated states. The relation Q also serves
as an interface to be added to the abstract controller in order to refine it into a controller for the
actual plant. We refer the reader to [1] for a formal definition of the closed loop, the details of the
synthesis procedure, and in particular, for a proof of the fact that the refined controller actually
solves the control problem for the plant S1 . The framework also allows for bounded measurement
errors P : Rn ⇒ Rn of the form
P (x) = x + J−z, zK

(4)

for some z ∈ Rn+ which are taken care of by simply requiring S1 4Q◦P S2 rather than S1 4Q S2 [1,
Sec. VI.B].
In what follows, we discuss the computation of abstractions S2 = (X2 , F2 , U2 ) satisfying S1 4Q◦P S2 ,
for a sampled system S1 associated with (3), where we restrict our attention to abstractions whose
state alphabet X2 is a cover of the state alphabet of S1 . The elements of X2 are nonempty, closed
hyper-intervals, which we call cells. We divide X2 into two subsets, which we interpret as “real”

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

4

quantizer symbols and overflow symbols, respectively. See [17, Sec. III.A]. We let the former subset,
subsequently denoted by X̄2 , consist of congruent cells that are aligned on the uniform grid
ηZn = {c ∈ Rn | ∃k∈Zn ∀i∈[1;n] ci = ki ηi }

(5)

with grid parameter η ∈ (R+ \ {0})n , i.e.,
x2 ∈ X̄2 ⇒ ∃c∈ηZn x2 = c + J−η/2, η/2K .

(6)

The computation of the map F2 on X̄2 × U2 will be based on overapproximating the attainable sets
of the cells in X̄2 under the flow of (3). For that purpose, we will define growth bounds below. Growth
bounds have been introduced in [1, Sec. VIII.A], where their important features are also discussed.
We denote by ϕ the general solution of the unperturbed control system associated with (3). More
formally, if x0 ∈ Rn , u ∈ Ū , then ϕ(t, x0 , u) is the value at time t of the solution of the initial value
problem ẋ = f (x, u), x(0) = x0 .
III.4 Definition. Let τ > 0, K ⊆ Rn , and Ū ′ ⊆ Ū . A map β : Rn+ × Ū ′ → Rn+ is a growth bound on
K, Ū ′ associated with τ and (3) if
(i) β(r, u) ≥ β(r ′ , u) whenever r ≥ r ′ and u ∈ Ū ′ ,
(ii) [0, τ ] × K × Ū ′ ⊆ dom ϕ and if ξ is a solution of (3) on [0, τ ] with input u ∈ Ū ′ and ξ(0), p ∈ K
then |ξ(τ ) − ϕ(τ, p, u)| ≤ β(|ξ(0) − p|, u).
Explicit growth bounds of the form
β(r, u) = eL(u)τ r + v(u),

(7)

where v(u) ∈ Rn+ and the matrix L(u) ∈ Rn×n is essentially nonnegative, can be computed under
mild assumptions [1]. The next result, which extends [1, Th. VIII.4] to the case of multiple growth
bounds, is the key to the computation of abstractions.
III.5 Theorem. Let S1 = (X1 , U1 , F1 ) be the sampled system associated with (3) and sampling time
τ > 0, and let P be given by (4). Let S2 = (X2 , U2 , F2 ) be a system, where X2 is a cover of X1 by
nonempty, closed hyper-intervals and U2 ⊆ U1 . Consider a subset X̄2 ⊆ X2 that satisfies (6), and for
any x2 ∈ X̄2 let βx2 be a growth bound on P (x2 ), U2 associated with τ and (3). Suppose that F2 is
given by
(i) F2 (x2 , u) = ∅ whenever x2 ∈ X2 \ X̄2 , u ∈ U2 , and
(ii) for x2 ∈ X̄2 , x′2 ∈ X2 and u ∈ U2 we have
x′2 ∈ F2 (x2 , u) ⇐⇒ (c + J−r ′ , r ′K) ∩ P (x′2 ) 6= ∅,

(8)

with r ′ = βx2 (η/2 + z, u), x2 = c̄ + J−η/2, η/2K, and
c = ϕ(τ, c̄, u).

(9)

Then we have S1 4Q◦P S2 , with Q ⊆ X1 × X2 defined by (x1 , x2 ) ∈ Q iff x1 ∈ x2 .
Theorem III.5 leads to constructive means to compute abstractions basically as follows. For every
cell x2 = c̄ + J−η/2, η/2K ∈ X̄2 and input symbol u ∈ U2
1) compute c = ϕ(τ, c̄, u) and r ′ = βx2 (η/2 + z, u),
2) determine all cells c′ + J−η/2, η/2K ∈ X2 that satisfy
(c + J−r ′ , r ′K) ∩ (c′ + J−η/2 − z, η/2 + zK) 6= ∅,
and define F2 (x2 , u) as the set of all such cells.
Proof of Theorem III.5. We have to verify (i),(ii) in Definition III.3 with Q ◦ P in place of Q. To see
(i) let (x1 , x2 ) ∈ Q ◦ P and u ∈ US2 (x2 ). Then, F2 (x2 , u) 6= ∅ and x2 ∈ X̄2 by the assumptions on u
and F2 . By our assumption on the growth bound βx2 it follows F1 (x1 , u) 6= ∅, thus u ∈ US1 (x1 ).

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

5

To see (ii) in Definition III.3, let (x1 , x2 ) ∈ Q ◦ P , u ∈ US2 (x2 ) and x′2 ∈ (Q ◦ P )(F1 (x1 , u)). It follows
that F1 (x1 , u) ∩ P (x′2 ) 6= ∅. Indeed, x′2 ∈ (Q ◦ P )(x′1 ) for some x′1 ∈ F1 (x1 , u), thus (x′1 , P (x′2)) ∈ Q, so
x′1 ∈ P (x′2 ). Next, from x1 ∈ P (x2 ) and the properties of βx2 it follows that F1 (x1 , u) ⊆ ϕ(τ, c̄, u) +
J−r ′ , r ′ K, where x2 = c̄+J−η/2, η/2K and r ′ = βx2 (η/2+z, u). Thus, (ϕ(τ, c̄, u)+J−r ′ , r ′K)∩P (x′2 ) 6= ∅,
and by the properties of F2 , we conclude x′2 ∈ F2 (x2 , u).
IV. Estimation of the size of abstractions
The size of an abstraction S2 = (X2 , U2 , F2 ) that is obtained by Theorem III.5 is given by the
number of transitions. To obtain a prediction on this size, we will disregard overflow symbols by
assuming X̄2 = X2 , and in addition, we will assume c in (8) is a random vector uniformly distributed
on the cells. Then, the following theorem shows that the function E : (R+ \ {0})n → R+ given by (2)
n×n
with A ∈ R+
, p ∈ Rn+ provides a prediction on the cardinality of F2 (x2 , u) for fixed (x2 , u) ∈ X̄2 ×U2
in dependence of the grid parameter η.
The key property of the functional E is that it also provides an accurate prediction when actually
computing abstractions. (See Section VI.)
IV.1 Theorem. Assume the hypotheses of Theorem III.5 with X̄2 = X2 . Let (x2 , u) ∈ X2 × U2 and
let β := βx2 in Theorem III.5 be of the form (7), where v(u) ≥ 0 and L(u) is essentially nonnegative.
For c in (8) assume in place of (9) that c is an n-dimensional vector of independent random variables
ci , i ∈ [1; n] each of which is uniformly distributed on some interval of length ηi . Then the expected
value of the number of cells in F2 (x2 , u) is given by E(η) in (2) with
A = id +eL(u)τ

and

p = 2(Az + v(u)).

(10)

Proof. The number of elements in F2 (x, u) for x = c̄ + J−η/2, η/2K is given by
Nηn (c, r ′ ) = |{p ∈ ηZn | p ∈ c + J−r ′ , r ′ K}|

(11)

with the random vector c and r ′ = r + eL(u)τ r + v(u) where r = η/2 + z. Here, |X| stands for the
cardinality of the set X. We have 2r ′ = 2r + 2(eL(u)τ r + v(u)) = p + Aη. The proof is therefore
completed by the next lemma.
IV.2 Lemma. Consider the grid ηZn in (5) with η ∈ Rn , η > 0. Let r ∈ Rn+ and let ci , i ∈ [1; n] be
n independent random variables, where each ci is uniformly distributed on some
Qn interval of length ηi .
n
Then the expected value of the number Nη (c, r) defined in (11) is given by i=1 2ri /ηi .
Q
Proof. Note that Nηn (c, r) = ni=1 Nη1i (ci , ri ) and since the ci are mutually independent, the expected
value of Nηn (c, r) is given as the product of the expected values of Nη1i (ci , ri ). Moreover, Nη1i (ci , ri ) =
N11 (ci /ηi , ri /ηi ) and N11 (x + 1, η̂) = N11 (x, η̂) for every x ∈ R and η̂ ∈ R+ . Hence, it suffices to consider
N11 (ĉ, η̂) with ĉ being uniformly distributed on [0, 1] and η̂ ∈ R+ . The expected value of N11 (ĉ, η̂) is
given by 2η̂. Indeed, if η̂ = k + ε with k ∈ Z+ and ε ∈ [0, 1/2[, then we obtain
Z 1
N11 (x, η̂) dx = (2k + 1)ε + 2k(1 − 2ε) + (2k + 1)ε = 2η̂
0

by separating the integration interval into [0, ε], [ε, 1 − ε] and [1 − ε, 1]. The case ε ∈ [1/2, 1[ is
similar.
V. Minimization of the size of abstractions
Theorem IV.1 motivates the following on the computation of abstractions in the special case that
the growth bounds in Theorem III.5 coincide and do not depend on the input symbol, i.e., βx2 (r, u) =
βx′2 (r, u′ ) for any (x2 , u), (x′2 , u′) ∈ X̄2 × U2 , and any r ∈ Rn+ : Consider the abstractions for S1 that
have cells of volume exp(γ), γ ∈ R, and input alphabet U2 . Among those abstractions, the abstraction

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

6

with the least expected size has cells that are aligned according grid parameter η, where η is a solution
of the optimization problem
Yn
ξi .
(12)
min E(ξ) subject to exp(γ) =
i=1

ξ>0

Unfortunately, the optimization problem (12) is non-convex if n ≥ 2, and non-convex problems are
notoriously difficult to solve.
The main results of this work, which are presented in this section, include a characterization of
existence and uniqueness of η, and the means to numerically compute η, so that the just motivated
heuristic to reduce the computational effort becomes applicable. We will also investigate the generalization of (12) to the case of arbitrary growth bounds.
To establish aforementioned characterization we first bypass non-convexity. To this end, consider a
transformation of (12):
min g(x) subject to x ∈ Vγ ,
(13)
x

where g(x) = E(exp(x)) and

Vs = {v ∈ Rn | v1 + . . . + vn = s}

(14)

for s ∈ R. Here and subsequently, the exponential exp is taken component-wise whenever the argument
is a vector. The result below lists the outstanding properties of g.
n×n
V.1 Theorem. Let n ≥ 2, A ∈ R+
, p ∈ Rn+ and γ ∈ R, and let E, g and V be defined as in (2)
and above. Then g is convex. Moreover, if all diagonal entries of A are positive and A or A1 1p is
irreducible then the assertions below hold.
(i) g is strictly convex on Vγ . To be more precise, g ′′ (x)h2 > 0 for all x ∈ Vγ and h ∈ V0 \ {0}.
(ii) Let µ be the smallest nonzero entry of A and p, c = (n − 1)−1 . Then x ∈ Vγ implies

g(x) ≥ µn exp(−|γ|c) exp(ckxk∞ ).

(15)

The above result implies that the optimization problem (13) is convex. Moreover, since (15) implies
g(x) → ∞ as kxk∞ → ∞, x ∈ Vγ , the problem (13) has a unique solution under the hypotheses of
Theorem V.1 [18, 4.3.3], and thus, so has (12). Our result also shows that standard numerical methods
will converge globally when applied to (13), e.g. [18, Sec. 14.5], and some will do so even if (13) is
supplemented with a finite number of constraints of the form ai ≤ xi or xi ≤ ai , ai ∈ R [19, Th. 1].
For completeness, we remark that global convergence can also be ensured if g is strongly convex on
Vγ , a property established in [14, Th. 3] for irreducible A. However, the property is not implied under
the rather mild hypotheses of Theorem V.1, which are satisfied, in particular, if every component of
the state is subject to some measurement error, i.e., if z > 0 in (10), regardless of the dynamics of
the plant S1 under investigation. Finally, we note that checking irreducibility (for n ≥ 2) is equivalent
to finding strongly connected components in directed graphs [21, Th. 2.2.7], so irreducibility can be
checked with linear time algorithms [20].
Proof of Theorem
has been established in [14, Th. 3]. We first prove (i). Define
P V.1. Convexity of g P
Ri (x) = pi + nj=1 Ai,j exj and G(x) = ni=1 ln Ri (x) to see that
−γ

g(x) = e

n
Y

Ri (x) = exp(G(x) − γ)

i=1

for every x ∈ Vγ . It follows that g ′′ (x)h2 = g(x) (G′ (x)h)2 + g(x)G′′ (x)h2 and that (G′ (x)h)2 + G′′ (x)h2
equals
!2
n
n
X
X
Ri′ (x)h
Ri′′ (x)h2 Ri (x) − (Ri′ (x)h)2
(16)
+
Ri (x)
(Ri (x))2
i=1
i=1

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

(i)

7

1/2

(i)

(i)

for all x ∈ Vγ and all h ∈ V0 . Define vectors a(i) , b(i) ∈ Rn+1 by bn+1 = pi , an+1 = 0, bj = (Ai,j exj )1/2
(i)
(i)
and aj = bj hj for every j ≤ n. Then b(i) is not a zero vector for any i ∈ [1; n]. Use (16) to see that
g(x)−1 g ′′ (x)h2 equals
n
n
X
a(i) b(i) 2 X ka(i) k22 ·kb(i) k22 − a(i) b(i)
+
kb(i) k22
kb(i) k42
i=1
i=1

2

.

(17)

Now assume g ′′ (x)h2 = 0 for some h ∈ V0 and let us show that h = 0. Indeed, we deduce from (17)
and Cauchy’s inequality that for all i ∈ [1; n] there exists λi ∈ R such that a(i) = λi b(i) . This equation
implies a) λi = 0 whenever pi > 0, b) λi = hi for any i as Ai,i > 0, and therefore c) hi = hj
whenever Ai,j > 0. Next, assume
that h has two nonzero components hr , hs such that hr 6= hs . By the

irreducibility of A or A1 p1 there exist distinct indices i1 , . . . , im ∈ [1; n + 1] such that r = i1 , s = im
and at least one of the following cases occurs:
1) n + 1 ∈
/ {i1 , . . . , im } and Aik ,ik+1 > 0 for all k ≤ m − 1,
2) pr > 0,
3) m ≥ 3, pim−1 > 0 and Aik ,ik+1 > 0 for all k ≤ m − 2.
The remarks a), b), c) above will exclude each of the three cases. Indeed, the first case is impossible
as it implies hr = hs . The second case implies hr = 0, so cannot occur either. For the same reason, the
third case is impossible as him−1 = 0 and hr =
the nonzero entries of h coincide.
im−1 . Consequently,
Pn
Ph
n
However, as (17) vanishes, we conclude 0 = i=1 λi = i=1 hi , and so h = 0.
Now we prove (ii). We begin with deriving an inequality that we use in the second part of the proof.
To this end, note first that by our assumptions the following property holds for all r ∈ [1; n] and all
s ∈ [1; n], or for all r ∈ [1; n] and s = n + 1: There exists a subset of indices
 {i1 , . . . , im } ⊆ [1; n + 1]
Ap
such that (r, s) = (i1 , im ) and Ãik ,ik+1 > 0 for all k ∈ [1; m[, where Ã = 0 1 . Now fix (r, s) satisfying
previous condition with the subset of indices P := {i1 , . . . , im }. Let x ∈ Rn and set xn+1 := 0 to see
that
n
 Y
 m−1
Y
−γ
g(x) ≥ e
Ãj,j exp(xj )
Ãik ,ik+1 exp(xik+1 )
j=1
j ∈P
/ \{im }

≥µ

n

Y
j∈P

exp(−xj )

k=1

m
Y

exp(xik ) = µn exp(xs − xr ).

k=2

For the second part of the proof let q ∈ [1; n] such that kxk∞ = |xq | and observe xq −γ = −
So, for some s ∈ {q, n + 1} we have
n
Y

exp(xs − xr ) = exp((n − 1)xs ) exp(xq − γ).

(18)
Pn

r=1,r6=q

xr .

(19)

r=1
r6=q

Therefore, (µ−n g(x))n−1 is not less than (19) by applying (18) to each factor of the product in (19).
This implies (15) if xq ≥ 0. If xq < 0 and if (18) holds for s = n + 1 then (15) follows obviously. If
xq < 0 and if (18) holds for all r, s ∈ [1; n] then take the inverse on both sides of (19) with s = q, and
use (18) with r and q in place of s and r, respectively, to see that (µ−n g(x))n−1 ≥ exp(γ − nxq ). So,
the proof is easily completed.
The announced characterization related to (12) is as follows.
V.2 Theorem. Let γ ∈ R and E be defined as in (2) with A having
 positive diagonal. Then the
optimization problem (12) has a unique minimum point iff A or A1 1p is irreducible.

The proof of above theorem requires the next lemma. Below, A⊤ denotes the transpose of a matrix
A.

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

V.3 Lemma. Let n ≥ 2, let A ∈ Rn×n , p ∈ Rn+ . Assume that both A and Ã =
Then P̃ ÃP̃ ⊤ equals


X 0 0
 Z Y p̄
1 1 1

8

A p
1 1



are reducible.

(20)

where P̃ = ( P0 01 ) ∈ R(n+1)×(n+1) , P ∈ Rn×n is a permutation matrix, X ∈ Rn1 ×n1 , Y ∈ Rn2 ×n2 ,
Z ∈ Rn2 ×n1 , n1 , n2 ∈ [1; n[, n1 + n2 = n and p̄ ∈ Rn+2 .
B 0 ), where B ∈
Proof. There exists a permutation matrix T ∈ R(n+1)×(n+1) such that T ÃT ⊤ = ( D
C
m1 ×m1
m2 ×m2
m2 ×m1
R
,C ∈R
,D ∈R
, m1 , m2 ∈ [1; n] and m1 + m2 = n + 1. This fact may be seen
by using [21, Th. 2.2.7] to establish the equivalence of the definition of irreducibility in Section II
and [21, Def. 2.1.2] for n ≥ 2. Next, as the last row of Ã contains only nonzero entries, we conclude
that the nonzero entries of p are contained in a column of C. Hence, we may assume without loss of
generality that the nonzero entries of p are contained in the last column of C, i.e., that T = ( P0 01 ),
where P ∈ Rn×n is a permutation matrix. Then, observe that the upper left n × n submatrix of T ÃT ⊤
equals P AP ⊤ and the first m1 entries of the last column of T ÃT ⊤ vanish. So, as A is reducible, we
0
may redefine P to be such that P AP ⊤ = ( X
Z Y ), which completes the proof.
n×n
Below, we denote E by EA,p whenever clarity requires to specify A ∈ R+
and p ∈ Rn+ in the
definition (2) of E.

Proof of Theorem V.2. Sufficiency has already been established in the remark following the statement
of Theorem V.1. To prove necessity, assume that both matrices in the statement are reducible. Note
that EA,p (x) = EP AP ⊤ ,P p(P x) for any permutation
matrix P ∈ Rn×n and x ∈ (R+ \ {0})n . Therefore,

A p
assume without loss of generality that 1 1 is of the form (20). For x ∈ Rn let x(1) = (x1 , . . . , xn1 )
and x(2) = (xn1 +1 , . . . , xn ), i.e., x = (x(1) , x(2) ). Then
E(x) =

n1
n2
Y
Y
(Xx(1) )i (Zx(1) + Y x(2) + p̄)i
i=1

(21)

i=1

for any x ∈ (R+ \ {0})n . Now, assume x is a solution of (12) and set ξλ = (λ−n2 /n1 x(1) , λx(2) ) for every
λ > 0. It follows that ξλ is a feasible point of (12), for all λ > 0. Next, if Zx(1) 6= 0 or p̄ 6= 0 we obtain
using (21) that
E(x) > EX,0 (x(1) ) · EY,0 (x(2) ).
(22)
However, E(ξλ ) converges to the right hand side of (22) as λ → ∞, which contradicts the choice of x.
If Zx(1) = 0 and p̄ = 0 then E(x) = E(ξλ ) for any λ, so any ξλ is a solution of (12) for any λ > 0.
Finally, we consider the general situation in Theorems III.5 and IV.1, where the growth bounds
depend on the cell and the input symbol. In this case, the computation of an abstraction with finite X̄2
and finite U2 requires a sequence of growth bounds (βj )j∈J indexed by some finite set J. In particular,
for any i = (j, u) ∈ J × U2 there are an essentially nonnegative matrix L(i) ∈ Rn×n and v (i) ∈ Rn+
such that βj (r, u) is given by the right hand side of (7) with L(i) and v (i) in place of L(u) and v(u),
respectively, for all r ∈ Rn+ . Therefore, we obtain by generalizing (12) the following heuristic to reduce
the size of abstractions that have cells of volume exp(γ), γ ∈ R: Pick the grid parameter to solve
Yn
e
ξi ,
(23)
subject to exp(γ) =
min E(ξ)
i=1

ξ>0

e : (R+ \ {0})n → R+ is given by
where E

e
E(ξ)
=

X

i∈I

EA(i) ,p(i) (ξ).

(24)

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

9

Here, A(i) and p(i) are defined analogously to A and p in (10), i.e., A(i) = id + exp(L(i) τ ), p(i) =
2(A(i) z + v (i) ).
Theorem V.4 below provides sufficient conditions for (23) to possess a unique solution. To facilitate
the practical verification of the conditions we will formulate them in terms of L(i) and v (i) rather than
in terms of A(i) and p(i) . Moreover, Theorem V.4 will imply that (23) can be solved numerically by
e
solving (13) with e
g (x) := E(exp(x))
in place of g(x).

V.4 Theorem. Let γ ∈ R, τ > 0, z ∈ Rn+ , and let I be a finite set. For every i ∈ I define A(i) =
id + exp(L(i) τ ), p(i) = 2(A(i) z + v (i) ), where L(i) ∈ Rn×n is essentially nonnegative, and v (i) ∈ Rn+ . Let
e and e
V, E
g be defined as in (14), (24) and above. For some i ∈ I suppose that L(i) or

 (i)
L
z + L(i) z + v (i)
(25)
1
1
is irreducible. Then (23) possesses a unique solution. Moreover, ge ′′ (x)h2 > 0 for all x ∈ Vγ and
h ∈ V0 \ {0}, and e
g (x) → ∞ as kxk∞ → ∞, x ∈ Vγ .
The proof of Theorem V.4 requires the result below.

V.5 Lemma. Let p ∈ Rn+ and let L ∈ Rn×n be essentially nonnegative. We have the following:
(i) L is irreducible iff exp(Lt) is irreducible for every t > 0.
p
is irreducible for every t > 0.
(ii) If L is reducible, then L1 p1 is irreducible iff exp(Lt)
1
1

Proof. Necessity in (i) follows from [22, Rem. I.7.9] and [21, Th. 2.2.7] by establishing the equivalence
between the definition of irreducibility in [22, Sec. I.7.4] and ours. Sufficiency in (i) follows from an
evaluation of the exponential series.
To verify the necessary condition in (ii), first note that
(Li,j 6= 0, t > 0) ⇒ exp(Lt)i,j ≥ 0

(26)

if L is nonnegative. To see that (26) also holds for essentially nonnegative matrices, choose c > 0
such that L +c id is nonnegative. Then
 (26) holds since exp(Lt) = exp((L + c id)t) exp(−ct). Thus,
Lt p
p
arises
from
B
=
A = exp(Lt)
1 1 by adding nonnegative values to the entries of B. Consequently,
1
1
the irreducibility of B passes over to A.

To prove sufficiency, assume that both L and L̃ = L1 1p are reducible. By Lemma V.3 there exist
permutation matrices P and P̃ satisfying the following: P̃ L̃P̃ ⊤ is of the form (20) and P exp(L)P ⊤ =
′ 0
exp(P LP ⊤ ) = X
X ′ , Y ′ , Z ′ are matrices of the same dimensions as X, Y , Z in (20),
Z ′ Y ′ , where

p
is reducible by [21, Th. 2.2.7] as it can be transformed by P̃ to the
respectively. Hence, exp(L)
1
1
′
′
′
form (20) with X , Y , Z in place of X, Y , Z, respectively.

Proof of Theorem V.4. As (26) holds for L(i) in place of L, we may prove the theorem assuming
exp(L(i) τ )z in place of L(i) z in (25). Thus, by Lemma V.5 one of the matrices in the statement of
Theorem V.1 with A(i) , p(i) in place of A, p, respectively, is irreducible. Moreover, A(i) has positive
diagonal [22, Th. I.7.4]. Now apply Theorem V.1 to A(i) and p(i) in place of A and p to see that a(x) :=
EA(i) ,p(i) (exp(x)) satisfies a′′ (x)h2 > 0 for all x ∈ Vγ and h ∈ V0 \{0}, and a(x) → ∞ as kxk∞ → ∞, x ∈
Vγ . Moreover, every summand in e
g is convex and positive. So, as a is a summand in ge the assertions on e
g
hold. Hence, (13) with e
g in place of g possesses a unique solution [18, 4.3.3], and thus, so does (23).
VI. Numerical example
To demonstrate the benefits of the presented results, we consider the control system of a double
pendulum that is mounted on a cart as investigated in [23]. The dynamics of this system can be
decomposed into the motion of the two poles and the motion of the cart, which are coupled by the
acceleration of the cart. Here, we consider only the motion of the poles. Specifically, we consider the

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

6·1010

10

ç
æ

5·1010

æ
ç
æ
ç
æ
ç

4·1010

æ
ç
æ
ç

10

3·10

æ
ç

æ
ç

æ
ç

æ
ç

æ
ç

æ
ç

æ
ç

æ
ç

æ
ç

2·1010
1·1010

0

118
118
118
118

118
129
113
113

k1
k2
k3
117 117 116 116 116 115 115 114 114 138 161 184 208 k4
143 157 175 198 221 251 285 329 378 313 269 235 208
108 103 98 92 87 82 77 72 67 67 67 67 67
108 103 98 92 87 82 77 72 67 67 67 67 67

Figure 1.
Predicted (•) and actual (◦) number of transitions in abstractions based on the grid parameters
((π/2 + 0.1)/k1 , 2π/k2 , 11.4/k3 , 11.4/k4 ) for the system S1 considered in Section VI.

equations of motion given in [23, Tab. 2], rewritten as a first order system (3) with n = 4, Ū = R, and
x = (φ1 , φ2 , φ̇1 , φ̇2 ) in the notation of [23]. Specifically, x1 and x2 denotes the angle formed by the inner
and outer, respectively, pole and the vertical ray, and x3 and x4 denote the corresponding angular
velocities. The control input u is the acceleration of the cart. See also [23, Fig. 1]. We additionally
model uncertainties in friction forces in the links by virtue of w = (0, 0, 0.018, 0.028) in (3).
We aim at steering the state of the system from the stable equilibrium point (π, π, 0, 0) to an ellipsoid
centered at the lower unstable equilibrium point x0 = (π, 0, 0, 0) given by {x ∈ R4 | (x − x0 )⊤ V (x − x0 ) ≤ 1}
where
 0.247 0.153 −0.023 −0.026 
0.153 0.106 0.026 −0.023
.
V = −0.023
0.026
8.24
3.893
−0.026 −0.023 3.893

1.922

We assume measurement errors (4) with z = (b, b, 2b, 2b), b = 2π/214 which are motivated by 14-bit
quantized measurements of the angles. Additionally, we require the state x ∈ R4 of the system not to
leave X̄ = [π/2, π + 0.1] × [0, 2π] × [−5.7, 5.7] × [−5.7, 5.7] and we identify x and x + (0, 2πk, 0, 0) for
any k ∈ Z. The latter means that we do not impose restrictions on the outer angle.
We shall solve this control task for the sampled system S1 associated with (3) and sampling time
τ = 0.01 using the synthesis procedure outlined in Sections I and III, in which we focus on the
computation of abstractions. Using Theorem III.5, we will compute two abstractions S2 = (X2 , U2 , F2 )
and S2′ = (X2′ , U2′ , F2′ ) for S1 , where S2 is based on a naive choice of the grid parameter, and the grid
parameter for S2′ is chosen using the results in Section V.
We begin with the details to S2 . We let U2 consist of 5 elements equally spaced on 9.81 · [−3.5, 3.5].
Next, we let X̄2 in Theorem III.5 be a cover of X̄ and let X2 be a grid of the form (5) with grid
parameter
2π 11.4 11.4
η = ( π/2+0.1
, 118
, 118 , 118 ) ≈ (0.014, 0.053, 0.097, 0.097).
118

η is a naive choice as each component of X̄ is subdivided into 118 intervals of equal length. Then
X̄2 consists of about 194·106 cells. The transition function F2 is computed according to Theorem
III.5, where the required growth bounds are obtained by methods presented in [1]. The computation
of S2 requires 206GB RAM and 2.5h cpu time. S2 contains about 55.7·109 transitions and 54.6·109
transitions have been predicted by means of (24). All computations in this section are run on a single
thread of an Intel Xeon E5-2687W (3.1 GHz).
In contrast, for S2′ we let U2′ = U2 but choose the grid parameter as the solution of (23) under the
constraint that the cells of X2′ have the same volume as those of X2 and the additional constraints
ξi ≤ 0.17, i ∈ [1; 4],
2π 11.4 11.4
, 378
, 67 , 67 ) ≈ (0.015, 0.017, 0.17, 0.17)
η ′ = ( π/2+0.1
114

Weber, Rungger and Reissig

Optimized State Space Grids for Abstractions

11

and define X2′ in the same way as X2 , with η ′ in place of η. The computation of S2′ requires 134GB
RAM and 73 min cpu time. S2′ contains about 30.3·109 transitions and the prediction has been 30.0·109
transitions.
In summary, the number of transitions, computational time and memory consumption is reduced
by 46%, 51% and 35%, respectively, compared to a naive choice of the aspect ratio. Moreover, in
contrast to the auxiliary control problem for S2 , the one for S2′ is solvable, due to a reduced number
of spurious transitions.
The success of our method to reduce the size of abstractions depends to a great extend on
the accuracy by which the functional in (23) predicts the number of transitions. That accuracy is
illustrated in Fig. 1 for a number of additional abstractions for S1 with varying grid parameters. It
turns out that the prediction possesses an error of less than 2%.
References
[1] G. Reissig, A. Weber, and M. Rungger, “Feedback refinement relations for the synthesis of symbolic controllers,” IEEE
Trans. Automat. Control, vol. 62, no. 4, pp. 1781–1796, Apr. 2017, DOI:10.1109/TAC.2016.2593947, arXiv:1503.03715.
[2] P. Tabuada, Verification and control of hybrid systems. New York: Springer, 2009.
[3] M. Rungger and O. Stursberg, “On-the-fly model abstraction for controller synthesis,” in American Control Conference
(ACC), 2012, pp. 2645–2650.
[4] M. Rungger, M. Mazo, and P. Tabuada, “Specification-guided controller synthesis for linear systems and safe linear-time
temporal logic,” in Proc. 16th Intl. Conf. Hybrid Systems: Computation and Control (HSCC), Philadelphia, PA, U.S.A.,
Apr. 8-11, 2013. ACM, 2013, pp. 333–342.
[5] G. Pola, A. Borri, and M. D. Di Benedetto, “Integrated design of symbolic controllers for nonlinear systems,” IEEE Trans.
Automat. Control, vol. 57, no. 2, pp. 534–539, 2012.
[6] A. Girard, G. Gössler, and S. Mouelhi, “Safety controller synthesis for incrementally stable switched systems using multiscale
symbolic models,” IEEE Transactions on Automatic Control, vol. 61, no. 6, pp. 1537–1549, June 2016.
[7] Y. Tazaki and J. Imura, “Discrete-state abstractions of nonlinear systems using multi-resolution quantizer,” in Proc. 12th
Intl. Conf. Hybrid Systems: Computation and Control (HSCC), San Francisco, U.S.A., Apr. 13-15, 2009, ser. Lect. Notes
Computer Science, R. Majumdar and P. Tabuada, Eds., vol. 5469. Springer, 2009, pp. 351–365.
[8] S. Mouelhi, A. Girard, and G. Gössler, “Cosyma: A tool for controller synthesis using multi-scale abstractions,” in Proc.
16th Intl. Conf. Hybrid Systems: Computation and Control (HSCC), Philadelphia, PA, U.S.A., Apr. 8-11, 2013. New
York, NY, USA: ACM, 2013, pp. 83–88.
[9] E. Le Corronc, A. Girard, and G. Goessler, “Mode sequences as symbolic states in abstractions of incrementally stable
switched systems,” in Proc. 52th IEEE Conf. Decision and Control (CDC), Florence, Italy, 10-13 Dec. 2013. New York:
IEEE, 2013, pp. 3225–3230.
[10] M. Zamani, I. Tkachev, and A. Abate, “Bisimilar symbolic models for stochastic control systems without state-space
discretization,” in Proc. 17th Intl. Conf. Hybrid Systems: Computation and Control (HSCC), Berlin, Germany, Apr. 15-17,
2014. New York, NY, USA: ACM, 2014, pp. 41–50.
[11] G. Reissig and M. Rungger, “Feedback refinement relations for symbolic controller synthesis,” in Proc. IEEE Conf.
Decision and Control (CDC), Los Angeles, CA, U.S.A., 15-17 Dec. 2014. New York: IEEE, 2014, pp. 88–94.
[12] D. Ž. Djoković, “Note on nonnegative matrices,” Proc. Amer. Math. Soc., vol. 25, pp. 80–82, 1970.
[13] D. London, “On matrices with a doubly stochastic pattern,” J. Math. Anal. Appl., vol. 34, pp. 648–652, 1971.
[14] M. Rungger, A. Weber, and G. Reissig, “State space grids for low complexity abstractions,” in Proc. IEEE Conf. Decision
and Control (CDC), Osaka, Japan, 15-18 Dec. 2015. New York: IEEE, 2015, pp. 6139–6146.
[15] R. T. Rockafellar and R. J.-B. Wets, Variational analysis, ser. Grundlehren der Mathematischen Wissenschaften. Berlin:
Springer-Verlag, 1998, vol. 317, 3rd corr printing 2009.
[16] A. F. Filippov, Differential equations with discontinuous righthand sides, ser. Mathematics and its Applications (Soviet
Series). Kluwer Academic Publishers Group, Dordrecht, 1988, vol. 18, translated from the Russian.
[17] G. Reißig, “Computing abstractions of nonlinear systems,” IEEE Trans. Automat. Control, vol. 56, no. 11, pp. 2583–2598,
Nov. 2011.
[18] J. M. Ortega and W. C. Rheinboldt, Iterative solution of nonlinear equations in several variables, ser. Classics in Applied
Mathematics. Philadelphia, PA: Society for Industrial and Applied Mathematics (SIAM), 2000, vol. 30, reprint of the 1970
original.
[19] M. V. Solodov, “Global convergence of an SQP method without boundedness assumptions on any of the iterative sequences,”
Math. Programming, vol. 118, no. 1, Ser. A, pp. 1–12, 2009.
[20] R. Tarjan, “Depth first search and linear graph algorithms,” SIAM Journal on Computing, 1972.
[21] A. Berman and R. J. Plemmons, Nonnegative matrices in the mathematical sciences, ser. Classics in Applied Mathematics.
Philadelphia, PA: Society for Industrial and Applied Mathematics (SIAM), 1994, vol. 9, revised reprint of the 1979 original.
[22] T. Kato, A short introduction to perturbation theory for linear operators. New York: Springer-Verlag, 1982.
[23] K. Graichen, M. Treuer, and M. Zeitz, “Swing-up of the double pendulum on a cart by feedforward and feedback control
with experimental validation,” Automatica J. IFAC, vol. 43, no. 1, pp. 63–71, 2007.

