Finite Uniform Bisimulations for Linear Systems with Finite
Input Alphabets

arXiv:1510.04209v1 [math.OC] 14 Oct 2015

Donglei Fan and Danielle C. Tarraf∗

Abstract
We consider a class of systems over finite alphabets, namely discrete-time systems with linear dynamics and a finite input alphabet. We formulate a notion of finite uniform bisimulation, and motivate and
propose a notion of regular finite uniform bisimulation. We derive sufficient conditions for the existence
of finite uniform bisimulations, and propose and analyze algorithms to compute finite uniform bisimulations when the sufficient conditions are satisfied. We investigate the necessary conditions, and conclude
with a set of illustrative examples.
Index Terms— finite uniform bisimulations, systems over finite alphabets, abstractions.

1

Introduction

The past decade has witnessed much interest in finite state approximations of hybrid systems for both analysis
and control design. Multiple complementary approaches have been developed and used [8, 10, 16, 23, 24]
including qualitative models and l-complete approximations [11–13], approximating automata [2–4], exact
or approximate bisimulation and simulation abstractions [6, 18], and ρ/µ approximations [20–22].
In particular, the existence of “equivalent" finite state representations of systems with infinite memory
has been a problem of academic interest, and continues to be so. Typically, this equivalence is captured by
the existence of a bisimulation relation between the original system and the finite memory model, a concept
originally introduced in the context of concurrent processes [15]. For instance in [9], the authors show that
if a hybrid transition system is O-minimal, then it has a finite bisimulation quotient. In [1], by interpreting
the trajectories of linear systems as O-minimal language structures, the authors present instances of linear
systems which admit finite bisimulation quotients. In [26], the authors provide an algorithm for finding finite
bisimulations for piecewise affine systems, and show that it can be applied to linear systems in a dead-lock free
manner. In [19], the authors show that certain controllable linear systems admit finite bisimulations. In [6]
the authors propose an algorithm, based on polyhedral Lyapunov functions, to generate finite bisimulations
for switched linear systems with stable subsystems.
Concurrently, bisimulation has been explored in a more traditional systems setting. Particularly in
[25], the author discusses the connection between bisimulation relations and classical notions of state space
equivalence and equality of external behavior in systems theory. Specifically, he shows that a bisimulation
relation between two linear time-invariant (LTI) systems exists if and only if their transfer matrices are
identical.
In this paper, we revisit the question of existence of finite state equivalent models (a preliminary version
of this work appeared in [5]), focusing on a special class of systems over finite alphabets, namely systems
with linear dynamics and finite input alphabets. This class of systems provides potential models of simple
practical systems where the actuation involves multi-level switching. For this class of systems:
1. We formalize the notion of finite uniform bisimulation and discuss its connections to the existing
literature, and we propose a new notion of regular finite uniform bisimulation.
2. We derive sufficient conditions for the existence of finite uniform bisimulations.
∗ The authors are with the Department of Electrical & Computer Engineering Department at Johns Hopkins University,
Baltimore, MD, 21218 (dfan4@jhu.edu, dtarraf@jhu.edu).

1

3. We propose and analyze constructive algorithms for computing finite uniform bisimulations when the
sufficient conditions are satisfied.
4. We explore the question of necessity and derive a set of necessary conditions, highlighting the relevance
of the regularity property of finite uniform bisimulations.
5. We provide a set of examples, thereby illustrating how existence of finite uniform bisimulations can be
exploited to derive an “equivalent" deterministic finite state machine model for the system.
Paper Organization: We formulate the notion of finite uniform bisimulation and propose that of regular
finite uniform bisimulation in Section 2. We describe the class of systems of interest, pose our problem, and
place our work in the context of existing literature in Section 3. We state our main analytical results in
Section 4 and present the corresponding constructive algorithms in Section 5. We present a full derivation
of the analytical results and an analysis of our constructive algorithms in Section 6. We present a set of
illustrative examples in Section 7 and conclude with directions for future work in Section 8.
Notation: We briefly summarize our notation here and, for completeness, we provide a review of all
relevant concepts in the Appendix. We use N to denote the non-negative integers, Z+ to denote the positive
integers, Q to denote the rationals, R to denote the reals, and C to denote the complex numbers. For a set
A ⊂ Rn , we use |A| to denote its cardinality (which could be infinite), diam(A) to denote its diameter, Ac
to denote its complement, cl(A) to denote its closure, int(A) to denote its interior, and ∂A to denote its
boundary. A pair W and V of disjoint, nonempty, open sets in Rn is a disconnection of A if W ∩ A =
6 ∅,
V ∩ A 6= ∅ and A ⊂ W ∪ V, and we say A is not connected if there is a disconnection of A.
For
v ∈ Rn , we use kvk1 to denote its 1-norm. We use Br (v) to denote the open ball centered at v with
radius r. For a square matrix A, we use kAk1 to denote its 1-induced norm and ρ(A) to denote its spectral
radius. For sets S, R ⊂ Rn , a matrix H ∈ Rn×n and a vector v ∈ Rn , we use HS to denote the set
{z ∈ Rn |z = Hx, for some x ∈ S}, use v + S to denote the set {z ∈ Rn |z = v + x, for some x ∈ S}, and use
S + R to denote the set {x + r|x ∈ S, r ∈ R}. We use ∼ to denote an equivalence relation, x ∼ y to denote
that x is equivalent to y, x  y to denote that x is not equivalent to y, and [x] to denote the equivalence
class of x. For completeness, we provide detailed definitions of all our notation in the Appendix.

2
2.1

Finite Uniform Bisimulations
Proposed Notions

We begin by defining the notion of finite uniform bisimulation, which is simply an equivalence relation that
satisfies certain desired properties:
Definition 1. Consider a discrete-time system
xt+1 = f (xt , ut )

(1)

where t ∈ N is the time index, xt ∈ Rn is the state, ut ∈ U is the input, f : Rn × U → Rn is given, and
input alphabet U represents the collection of possible values of the input. Given a set S ⊂ Rn , we say
an equivalence relation ∼⊂ S × S is a finite uniform bisimulation on S if the following two conditions are
satisfied:
(i) For any x, x0 ∈ S and any u ∈ U, if x ∼ x0 , then
f (x, u) ∼ f (x0 , u)

(2)

(ii) For x ∈ S with [x] = {y ∈ S|y ∼ x}, we have
1 < |{[x]|x ∈ S}| < ∞

(3)

Essentially (2) requires that each equivalence class transition into another equivalence class under any
input, and (3) requires that there be a finite number of equivalence classes while avoiding the trivial instance
of a single equivalence class.
We define a finite uniform bisimulation to be regular if the equivalence classes have a specific topological
structure:
2

Definition 2. Given a finite uniform bisimulation ∼ on S of system (1), we say ∼ is regular if for all x ∈ S,
[x] = {y ∈ S|y ∼ x} consists of open sets in Rn and possibly their boundary points.
We are interested in regular finite uniform bisimulations because we wish to avoid certain “pathological"
finite uniform bisimulations, as will become clear when we discuss the necessary conditions for the existence
of finite uniform bisimulations in Section 4.2.

2.2

Deterministic Finite State Bisimulation Models

Given a finite uniform bisimulation ∼ on S of system (1), it is straightforward to construct a deterministic
finite state machine (DFM) that is bisimilar to the original system when the latter is restricted to evolve on
S. Indeed:
Definition 3. Given a system (1) denoted by P and a finite uniform bisimulation ∼ on S of P , consider the
DFM P̂ defined by
qt+1 = f∼ (qt , ut ),
(4)
where t ∈ N is the time index, qt ∈ Q is the state, ut ∈ U is the input, Q = {[x]|x ∈ S} (essentially Q is
the finite quotient set of S under equivalence relation ∼), U is the input alphabet of system (1), and state
transition function f∼ : Q × U → Q is defined as
f∼ (q, u) = [f (x, u)], ∀ x ∈ q.

(5)

We say that P̂ is uniformly bisimilar to P .
Note that since ∼ is a finite uniform bisimulation, it follows from (2) that f∼ is well-defined.

3

Problem Setup and Formulation

3.1

Systems of Interest & Problem Statement

We first introduce the specific class of systems (1) that we will study in this paper. Consider a discrete-time
dynamical system described by
xt+1 = Axt + But ,
(6)
where t ∈ N is the time index, xt ∈ Rn is the state, ut ∈ U is the input, and A ∈ Rn×n and B ∈ Rn×m are
given. We enforce that the input ut can only take finitely many values in U ⊂ Rm (that is, |U| < ∞).
For this class of systems, we are interested in questions of existence and construction of finite uniform
bisimulations on a subset S of the state space Rn . Particularly, in order for the bisimulation relation to yield
a meaningful “equivalent" DFM, we require the set S be an invariant set of the system:
N
Definition 4. A set S ⊂ Rn is an invariant set of system (6) if for any input sequence {ut }∞
t=0 ∈ U

x0 ∈ S ⇒ xt ∈ S, for all t ∈ N.

(7)

We are now ready to state the first problem of interest:
Problem 1. Given system (6), under what conditions on A, B, U does there exist a finite uniform bisimulation
∼ on some invariant set S of system (6)?
When Problem 1 has an affirmative answer, another set of problems naturally follows:
Problem 2. Given a system (6) that admits a finite uniform bisimulation on some invariant set S, under
what conditions on A, B, U can an arbitrarily large number of equivalence classes be generated by a finite
uniform bisimulation?
Note that we seek (and propose) both analytical and constructive, algorithmic solutions to the above
problems.

3

3.2

Comparison with Existing Work on Finite Bisimulations

Before presenting our main results, we briefly discuss the similarities and differences between the current
problem of interest and some of the previous developments on finite bisimulations:
• Our definition of finite uniform bisimulation is stronger than that of finite bisimulation used in some
of the literature, of which we pick [19] as a representative paper. In particular in that setting, the
definition requires that if two states are bisimilar (x ∼ y) and x transitions to x0 under input u, then
there exists an input u0 such that y transition to y 0 under u0 and y 0 ∼ y. Note that u and u0 need not
be the same, and thus a finite bisimulation as in [19] is not necessarily a finite uniform bisimulation.
We will use Example 1 in Section 7 to illustrate this difference.
• Our definition of finite uniform bisimulation is in accordance with the definitions of finite bisimulation
introduced in [6, 9]. However, the sufficient conditions for existence of finite bisimulations derived
in [9] concern linear vector fields, and as such correspond to special cases of (6) where B is the zero
matrix, whereas the present contribution addresses the more general case where B is nonzero. Likewise,
the dynamics of the system of interest in [6] are different, as the authors study systems of the form
xt+1 = Aσ(t) xt , where σ(t) is the switching signal and is considered to be the input.
• Finally, the finite input alphabet setup is unique in the literature, in contrast to typically studied
setups where the input signal takes arbitrary instantaneous values in Euclidean space, or else the input
signal is of certain form such as polynomial, exponential or sinusoidal as in [1].

4
4.1

Statement of Main Results
Sufficient Conditions and Construction

We begin by defining a set that will be useful for formulating a sufficient condition for the existence of finite
uniform bisimulations.
Definition 5. Given system (6), define set A as
A = {α ∈ Rn |α =

t
X

At−τ Buτ , u(·) ∈ U, t ∈ N}.

(8)

τ =0

Essentially, A is the collection of forced responses of system (6). Now, we are ready to propose a sufficient
condition for the existence of finite uniform bisimulations on some invariant subset of the state space.
Theorem 1. Given system (6) with 0 ∈ U, assume that A has all eigenvalues within the unit disc. If cl(A)
is not connected, then there exists a finite uniform bisimulation on a subset of Rn that is an invariant set of
system (6).
When the conditions in Theorem 1 are satisfied, we also propose an algorithm for computing finite uniform
bisimulations. To keep the flow of presentation, we present this algorithm in the following section (Algorithm
1 in Section 5). We show that Algorithm 1 is guaranteed to generate a finite uniform bisimulation when the
sufficient condition is satisfied.
Theorem 2. Given system (6), and let the hypothesis in Theorem 1 hold, then Algorithm 1 terminates, and
returns X1 , X2 such that X1 , X2 afford a finite uniform bisimulation on an invariant set S, namely S = X1 ∪X2 ,
of system (6).
Next, we continue to study Problem 2. It turns out that additional assumptions are needed to guarantee
the existence of arbitrarily many equivalence classes, as we shall see in Section 7 Example 2. In order to
describe such conditions, we first define a relevant collection of subsets of the state space Rn : Given system
(6), let U = {u1 , u2 , . . . , uq } for q ∈ Z+ and define sets {Sj1 }qj=1 as follows
Sj1 = Buj + cl(AA),

j = 1, 2, . . . , q.

(9)

We can now propose a sufficient condition for the existence of an arbitrarily large number of equivalence
classes.
4

Theorem 3. Given system (6) with 0 ∈ U and |U| > 1, assume that A has all eigenvalues within the unit disc.
If A is invertible, and {Sj1 }qj=1 (9) are disjoint, then for any z ∈ Z+ there is a finite uniform bisimulation ∼
of system (6) such that the number of equivalence classes associated with ∼ is greater than z.
We also propose an algorithm, which is an extension of Algorithm 1, to compute many equivalence classes.
Corollary 1. Given system (6), and let the hypothesis in Theorem 3 hold, then for any z ∈ Z+ , Algorithm
2 (see Section 5) terminates, and returns a finite uniform bisimulation ∼ that has more than z equivalence
classes.
Remark 1. These equivalence classes computed by Algorithm 2 can also be made arbitrarily fine, that is to
say, the diameter of each equivalence class can be made arbitrarily small (see Section 6.3).

4.2

Necessary Conditions for the Existence of Finite Uniform Bisimulations

Next, we investigate necessary conditions for the existence of finite uniform bisimulations. We quickly realize
that system (6) may admit “pathological" finite uniform bisimulations: If A, B, U have entries in Q, then the
partition Qn and Rn \ Qn affords a finite uniform bisimulation of system (6). This motivates us to study
regular finite uniform bisimulations. We propose a necessary condition for the existence of regular finite
uniform bisimulations.
Theorem 4. Given system (6) with 0 ∈ U. If ∼ is a regular finite uniform bisimulation on an invariant set
S of system (6), 0 ∈ int([0]), and [0] is bounded, then ρ(A) ≤ 1.
Remark 2. Theorem 4 states that under certain assumptions, there do not exist regular finite uniform
bisimulations for Schur unstable systems (6). This justifies why we study Schur stable systems in Theorem
1.
We point out that the condition “[0] is bounded" in Theorem 4 cannot be dropped (see Example 3 in
Section 7). However, the condition “[0] is bounded" in Theorem 4 can be dropped for scalar systems, where
we restrict our attention to instances of (6) described by
xt+1 = axt + but

(10)

where xt ∈ R, ut ∈ U, and a, b ∈ R. U is a finite subset of R.
Corollary 2. Given system (10) with 0 ∈ U. If ∼ is a regular finite uniform bisimulation on an invariant set
S of system (10) and 0 ∈ int([0]), then |a| ≤ 1.

5

Constructive Algorithms

First, we present an algorithm for computing finite uniform bisimulations when the conditions in Theorem
1 are satisfied.
We begin by introducing the notation of binary partitions of the finite input set U with |U| > 1: A pair
(U1 , U2 ) is a binary partition of U if U1 , U2 are nonempty, disjoint subsets of U, and U1 ∪U2 = U. The order of
U1 , U2 is not relevant: (U1 , U2 ) is the same as (U2 , U1 ). Since U is a finite set, there are finitely many distinct
(i)
(i)
binary partitions of U. We use {(U1 , U2 ) : i = 1, . . . , r} to denote the collection of all binary partitions of
q!
1
2
q−1
represents the quantity “q choose
U. Here r = (Cq + Cq + · · · + Cq )/2, where q = |U|, and Cqj = j!(q−j)!
j". Now we are ready to present the following algorithm to compute finite uniform bisimulations of system
(6).

5

Algorithm 1 Computing a Finite Uniform Bisimulation

17:
18:
19:
20:

Input: Matrix A, B, set U
Compute: h = max{kBuk1 : u ∈ U}
Choose:  such that 0 <  < 1 − ρ(A).
Compute: Matrix T , invertible, such that kT −1 AT k1 ≤ ρ(A) + .
(i)
(i)
Compute: All binary partitions of U: (U1 , U2 ), i = 1, . . . , r.
−1
k1 kT k1
Compute: κ = 2kT
1−ρ(A)−
k ← 1.
loop
Compute: lk = hkAk k1
i ← 1.
while i ≤ r do
(i)
(i)
Compute: C1 = {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 ∈ U1 , u2 , . . . , uk ∈ U}
(i)
(i)
C2 = {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 ∈ U2 , u2 , . . . , uk ∈ U}
(i)
(i)
(i)
Compute: dk = min{kα − βk1 : α ∈ C1 , β ∈ C2 }
(i)
if dk ≥ κlk then
ĩ ← i, k̃ ← k.
Exit the loop
end if
i ← i + 1.
end while
k ← k + 1.
end loop

21:

Compute: S = {x ∈ Rn : kT −1 xk1 <

22:
23:

Compute: X1 = C1 + S, X2 = C2 + S
Return: X1 , X2

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:

12:
13:
14:
15:
16:

(ĩ)

(ĩ)

d
k̃
2kT k1 }

(ĩ)

Remark 3. In the preceding algorithm, one approach to compute matrix T involves Schur’s triangularization
of matrix A (pp. 79, [7]). We refer interested readers to [7] on the specifics of computing matrix T such that
kT −1 AT k1 ≤ ρ(A) +  is satisfied.
Remark 4. Here we explain why Algorithm 1 returns two equivalence classes. We first point out that if
the conditions in Theorem 1 are satisfied, the number of equivalence classes generated by a finite uniform
bisimulation could be greater than two, which is the case in Example 4 in Section 7. However, for certain
systems (see Example 2 in Section 7), two, and only two equivalence classes can be generated based on the
analytical result stated in Theorem 1. Therefore Algorithm 1 returns two equivalence classes, since it is
capable of computing finite uniform bisimulations for any system that satisfies the conditions in Theorem 1.
As we shall see next, we propose another algorithm in case more equivalence classes are desired.
Next, we present a second algorithm, which is an extended version of Algorithm 1, to generate an
arbitrarily large number of equivalence classes when the conditions in Theorem 3 are satisfied.

6

Algorithm 2 Computing a Finite Uniform Bisimulation with Many Equivalence Classes

1:
2:
3:
4:
5:
6:
7:
8:

Input: Matrix A, B, set U = {u(1) , u(2) , . . . , u(q) }, integer z: Lower bound of the number of equivalence
classes.
Compute: h = max{kBuk1 : u ∈ U}
Choose:  such that 0 <  < 1 − ρ(A).
Compute: Matrix T , invertible, such that kT −1 AT k1 ≤ ρ(A) + .
k1 kT −1 k1
Compute: κ = 2kT
1−ρ(A)−
k ← 1.
loop
Compute: lk = hkAk k1
(k)
Compute: C1 = {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 = u(1) , u2 , . . . , uk ∈ U}
(k)

= {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 = u(2) , u2 , . . . , uk ∈ U}

C2

..
.
(k)

Cq
9:
10:
11:
12:
13:
14:
15:
16:

= {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 = u(q) , u2 , . . . , uk ∈ U}
(i)

(i)

Compute: dk = min{kα − βk1 : α ∈ Cv , β ∈ Cw , w 6= v, 1 ≤ w, v ≤ q}
if dk ≥ κlk then
k̃ ← k.
Exit the loop
end if
k ← k + 1.
end loop
d
Compute: S = {x ∈ Rn : kT −1 xk1 < 2kTk̃k1 }

(k̃)
(k̃)
(k̃)
Compute: X¯1 = C1 + S, X¯2 = C2 + S, . . . , X¯q = Cq + S
η+1
Choose: η ∈ Z+ such that q
> z.
η
19: Compute: An enumeration {u1 , u2 , . . . , uq η } of the set U η , where uj = (u1j , . . . , uj ).
20: Compute: Xk = Bu1 + ABu2 + · · · + Aη−1 Buη + Aη X̄i , 1 ≤ k ≤ q η+1 , where (u1 , . . . , uη ) = uj for
some 1 ≤ j ≤ q η , and 1 ≤ i ≤ q.
21: Return: X1 , . . . , Xq η+1

17:
18:

As we shall see in the derivation of Theorem 3 in Section 6, we claim that the sets X1 , . . . , Xqη+1 returned
η+1

by Algorithm 2 afford a finite uniform bisimulation on ∪qk=1 Xk of system (6).

6
6.1

Derivation of Main Results
Derivation of Theorem 1

We first introduce several Lemmas which will be instrumental in this derivation of Theorem 1.
Lemma 1. Given system (6), if matrix A has all eigenvalues within the unit disc, then cl(A) is compact.
P∞
Proof. If A ∈ Rn×n has all eigenvalues within the unit disc, then τ =0 kAτ k1 converges (pp. 298, [7]). Since
U is finite, max{kBuk1 : u ∈ U} is also finite. Combining these two facts, and applying triangle inequality,
we conclude that A is bounded and therefore cl(A) is bounded. Since cl(A) is closed and bounded in Rn ,
cl(A) is compact.
Next, we study the structure of set A as defined in (8). By the definition of A and 0 ∈ U, and recall (9),
we have
q
[
Sj1 = cl(A).
(11)
j=1

7

Generally, for any k ∈ Z+ , let {u1 , u2 , . . . , uqk } be an enumeration of the set U k , where uj = (u1j , . . . , ukj ),
k

u1j , . . . , ukj ∈ U, we define sets {Sjk }qj=1 as follows
Sjk = Bu1j + ABu2j + · · · + Ak−1 Bukj + cl(Ak A),

j = 1, 2, . . . , q k .

(12)

We also have
k

q
[

Sjk = cl(A).

(13)

j=1

Now we introduce the following Lemma.
Lemma 2. Given system (6), assume that A has all eigenvalues within the unit disc. If open sets W and V
∗
is a disconnection of cl(A), then there exists k ∗ ∈ Z+ such that for all j ∈ {1, . . . , q k },
∗

Sjk ∩ W 6= ∅

∗

Sjk ⊂ W

⇒

(14)

Proof. We show this Lemma by contradiction. We first assume that for all k ∈ Z+ , there is j(k) ∈ {1, . . . , q k }
k
k
k
k
∩W =
6 ∅ and Sj(k)
∩V =
6 ∅. For each k, choose wk ∈ Sj(k)
∩ W and vk ∈ Sj(k)
∩ V. Then
such that Sj(k)
∞
we have constructed two sequences {wk }∞
and
{v
}
.
k k=1
k=1
∞
Since {wk }∞
k=1 ⊂ cl(A), {vk }k=1 ⊂ cl(A) and cl(A) is compact (by Lemma 1), there exists a subsequence
∞
{wkl }∞
l=1 that converges to a point in cl(A). Similarly, there also exists a subsequence of {vkl }l=1 that
∞
converges to a point in cl(A). By relabeling, we have found two sequences {wkp }∞
and
{v
}
such
that
kp p=1
p=1
lim wkp = w,

p→∞

lim vkp = v

and

(15)

p→∞

where w, v ∈ cl(A).
By the construction of Sjk (12), we see that for any j, diam(Sjk ) ≤ kAk k1 diam(A). Since A has all
eigenvalues within the unit disc, lim Ak = 0n×n (pp.298, [7]). By boundedness of set A, diam(A) is finite.
k→∞

k

k

p
p
Therefore diam(Sjk ) goes to 0 as k tends to infinity. Note that wkp ∈ Sj(k
and vkp ∈ Sj(k
, and kp ≥ p,
p)
p)
therefore limp→∞ kwkp − vkp k1 = 0. Combine with (15), we have limp→∞ wkp = limp→∞ vkp = w, where
w ∈ cl(A). Without loss of generality, let w ∈ W. Since W is open, there exist  > 0 such that the open
ball B (w) ⊂ W. Since W ∩ V = ∅, {vkp }∞
p=1 ∩ B (w) = ∅. Therefore kvkp − wk1 ≥  for all p. This is a
contradiction with limp→∞ vkp = w. Therefore (14) holds.

Next, we introduce another Lemma which is based on Lemma 2.
Lemma 3. Given system (6), assume that A has all eigenvalues within the unit disc. If open sets W and V
is a disconnection of cl(A), then there exist open sets W 0 and V 0 in Rn such that the pair W 0 and V 0 is also
a disconnection of cl(A), and for all j ∈ {1, . . . , q}
Sj1 ∩ W 0 6= ∅

Sj1 ⊂ W 0

⇒

(16)

Proof. By Lemma 2 , (14) holds, and we only need to consider the case when k ∗ ≥ 2.
Define a function f : Rn → Rn as :f (x) = Ax. Clearly f is continuous. For any set S, use f −1 (S) to
denote the set f −1 (S) = {x ∈ Rn |f (x) ∈ S}.
∗

k∗

For {Sjk }qj=1 as constructed in (12), let u be an element of U, then define an index set J as
∗

J = {j ∈ {1, . . . , q k } : u1j = u},
then |J | = q k

∗

−1

. Define sets

∗

∗

S̃jk = −Bu + Sjk , j ∈ J .
∗

∗

(17)

For any j ∈ J , by (14), either S̃jk ⊂ −Bu + W or S̃jk ⊂ −Bu + V. Write W 0 = f −1 (−Bu + W) and
∗
∗
V 0 = f −1 (−Bu + V), then either f −1 (S̃jk ) ⊂ W 0 or f −1 (S̃jk ) ⊂ V 0 .

8

For each j ∈ J , by (12), (17), and the compactness of cl(A), we have
∗

S̃jk = A(Bu2j + · · · + Ak
∗

for some (u2j , . . . , ukj ) ∈ U k
that

∗

−1

∗

−2

∗

Bukj + cl(Ak

∗

−1

A))

. Consequently, we can determine one and only one j 0 ∈ {1, . . . , q k
∗

Sjk0

−1

∗

⊂ f −1 (S̃jk ).

We also observe that
[

∗

∗

−1

} such
(18)

(u2j , u3j , . . . , ukj ) = U k

∗

−1

.

(19)

j∈J

Recall (13), (18), we see that
∗

cl(A) =

−1
q k[

∗

Sjk0

−1

⊂

j 0 =1

[

∗

f −1 (S̃jk ) ⊂ W 0 ∪ V 0 .

(20)

j∈J

It is clear that W 0 and V 0 are disjoint open sets. Therefore (14) holds for k ∗ − 1 and W 0 , V 0 . Repeat this
argument k ∗ − 1 times, we conclude that (16) holds.
Finally, we provide the proof of Theorem 1.
Proof. (of Theorem 1) Since cl(A) is not connected, let W and V be a disconnection of cl(A). Then by
Lemma 3, (16) holds. We propose an equivalence relation on A. Since A is an invariant set of system (6),
the proof is complete if we can show that this equivalence relation satisfies (2) and (3).
Given open sets W 0 and V 0 that satisfy (16), let X1 = A ∩ W 0 and X2 = A ∩ V 0 . Define an equivalence
relation ∼ as
x ∼ x0 ⇔ x ∈ Xi and x0 ∈ Xi for some i ∈ {1, 2}.
For any x, x0 ∈ A, any uj ∈ U, if x ∼ x0 , then Ax + Buj ∈ Sj1 and Ax0 + Buj ∈ Sj1 . By (16), we see that
Ax + Buj ∼ Ax0 + Buj . Therefore (2) is satisfied. Since 1 < 2 < ∞, (3) is also satisfied. This completes the
proof.

6.2

Derivation of Theorem 2

In this section, we derive Theorem 2. We first show that Algorithm 1 terminates, and then show that the
equivalence classes X1 , X2 returned by Algorithm 1 afford a finite uniform bisimulation on X1 ∪ X2 .
Proof. (of Theorem 2) Given system (6), since matrix A has all eigenvalues within the unit disc, and cl(A)
is not connected, by Lemma 3, there is a disconnection of cl(A), W and V, such that for all j ∈ {1, . . . , q}
Sj1 ∩ W 6= ∅

⇒

Sj1 ⊂ W

(21)

where q = |U|. Let U1∗ = {uj ∈ U|Sj1 ∩ W 6= ∅}, and U2∗ = U \ U1∗ . Recall (11), we see that U1∗ is nonempty,
otherwise cl(A) ∩ W = ∅, which contradicts with W and V being a disconnection of cl(A). U2∗ is also
nonempty, otherwise cl(A) ⊂ W, then cl(A) ∩ V = ∅, which draws a contradiction. We also observe that
|U| > 1, otherwise U = 0 by assumption, and cl(A) = 0 is connected. Therefore the binary partitions of U
are well-defined. Since U1∗ and U2∗ are nonempty, disjoint subsets of U, and U1∗ ∪ U2∗ = U, there is a binary
(i∗ )
(i∗ )
partition of U, (U1 , U2 ), such that
(i∗ )

(U1

(i∗ )

, U2

) = (U1∗ , U2∗ )

where i∗ is an integer between 1 and r.
Since for any k ∈ Z+ ,
(i)
(i)
(i)
dk = min{kα − βk1 : α ∈ C1 , β ∈ C2 },

9

(22)

(23)

(i∗ )

we claim that dk

(23) is uniformly bounded away from zero, that is: There exists d > 0 such that
(i∗ )

dk

≥ d,

for all

To see this claim, we define two sets G1 , G2 by
[
G1 =
Sj1 ,

k ∈ Z+ .

[

G2 =

j∈U1∗

(24)

Sj1 .

(25)

j∈U2∗

By the definition of U1∗ , we see that G1 ⊂ W. Recall (11) and that W and V is a disconnection of cl(A),
we see that G2 ⊂ V. Because V and W are disjoint, G1 and G2 are also disjoint. Since G1 is a finite union
of closed sets, G1 is closed. By Lemma 1, cl(A) is bounded, and therefore G1 is bounded. We see that G1 is
closed, bounded, and therefore compact. Similarly, G2 is also compact. By an observation in analysis: The
distance between two disjoint compact sets is positive (pp. 18, [17]), we have
d = inf{kα − βk1 : α ∈ G1 , β ∈ G2 } > 0.
Since

(i)

(i)

(i)

(i)

(26)

C1 = {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 ∈ U1 , u2 , . . . , uk ∈ U}
C2 = {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 ∈ U2 , u2 , . . . , uk ∈ U}

(27)

and recall (9), (22), and (25), we observe that: For all k ∈ Z+ ,
(i∗ )

C1

(i∗ )

⊂ G1 ,

C2

⊂ G2 .

(28)

∗

(i )

Recall (23), we have dk ≥ d > 0 for all k ∈ Z+ .
Since matrix A is Schur stable, we see that lk = hkAk k1 → 0 as k → ∞. Consequently, there exists
∗
k ∈ Z+ such that
2kT k1 kT −1 k1
(i∗ )
lk∗ .
dk∗ ≥ κlk∗ =
1 − ρ(A) − 
Now we see that the loop in Algorithm 1 terminates, and returns two sets X1 , X2 :
(ĩ)

X1 = C1 + S,

(29)

(ĩ)

X2 = C2 + S.
For the second part of this derivation, we show that X1 ∪ X2 is an invariant set of system (6), and that
X1 , X2 afford a finite uniform bisimulation on X1 ∪ X2 .
For any x ∈ X1 ∪ X2 , by (27) and (29), there exist (u1 , . . . , uk̃ ) ∈ U k̃ and s ∈ S such that
x = Bu1 + ABu2 + · · · + Ak̃−1 Buk̃ + s.

(30)

Ax + Bu = (Bu + ABu1 + · · · + Ak̃−1 Buk̃−1 ) + (Ak̃ Buk̃ + As).

(31)

Then for any u ∈ U,

Recall kT −1 AT k1 ≤ ρ(A) + , κ =

2kT k1 kT −1 k1
1−ρ(A)− ,

and h = max{kBuk1 : u ∈ U}, we observe that

kT −1 (Ak̃ Buk̃ + As)k1
≤ kT −1 Ak̃ Buk̃ k1 + kT −1 Ask1
≤ kT −1 k1 kAk̃ k1 kBuk̃ k1 + k(T −1 AT )T −1 sk1
≤ kT −1 k1 lk̃ + k(T −1 AT )k1 kT −1 sk1
(ĩ)

< kT −1 k1

d
1 − ρ(A) −  (ĩ)
dk̃ + (ρ(A) + ) k̃
−1
2kT k1 kT k1
2kT k1

(ĩ)

=

dk̃

2kT k1

.

10

Therefore (Ak̃ Buk̃ + As) ∈ S. By (27), we observe that (Bu + ABu1 + · · · + Ak̃−1 Buk̃−1 ) ∈ C1ĩ ∪ C2ĩ , therefore,
we have
Ax + Bu ∈ X1 ∪ X2 .
(32)
We conclude that X1 ∪ X2 is an invariant set of system (6).
Next, we show X1 ∩ X2 = ∅. We show by contradiction: Assume z ∈ X1 ∩ X2 , then by (29), there exist
c1 ∈ C1ĩ , c2 ∈ C2ĩ , s1 ∈ S, and s2 ∈ S such that z = c1 + s1 , and z = c2 + s2 , and recall S = {x ∈ Rn :
(ĩ)

kT −1 xk1 < dk̃ /(2kT k1 )}, we have
kc1 − c2 k1 ≤ kc1 − zk1 + kz − c2 k1
= ks1 k1 + ks2 k1
= kT (T −1 s1 )k1 + kT (T −1 s2 )k1
≤ kT k1 (kT −1 s1 k1 + kT −1 s2 k1 )
(ĩ)

< dk̃ .
(ĩ)

But by (23), we have kc1 − c2 k1 ≥ dk̃ , which draws a contradiction. Therefore X1 ∩ X2 = ∅.
Now we are ready to define an equivalence relation ∼ on X1 ∪ X2 as:
x ∼ x0 ⇔ x ∈ Xi and x0 ∈ Xi for some i ∈ {1, 2}.
We show that ∼ is a finite uniform bisimulation on X1 ∪X2 . For any x, x0 ∈ X1 ∪X2 , and any u ∈ U, if x ∼ x0 ,
we consider two cases: If u ∈ U1ĩ , recall (27), (29), and (31), we see that Ax + Bu ∈ X1 and Ax0 + Bu ∈ X1 ,
therefore Ax + Bu ∼ Ax0 + Bu. Similarly, if u ∈ U2ĩ , then Ax + Bu ∈ X2 and Ax0 + Bu ∈ X2 , therefore
Ax + Bu ∼ Ax0 + Bu. Since (U1ĩ , U2ĩ ) is a binary partition of U, we see that (2) is satisfied.
Since {[x]|x ∈ X1 ∪ X2 } = {X1 , X2 }, we have |{[x]|x ∈ X1 ∪ X2 }| = 2, and (3) is satisfied. Therefore ∼ is
a finite uniform bisimulation on X1 ∪ X2 . This completes the proof.

6.3

Derivation of Theorem 3 & Corollary 1

Proof. To show Theorem 3 and Corollary 1, it suffices to show that Algorithm 2 terminates, and that the
sets X1 , . . . , Xqη+1 :
Xk = Bu1 + ABu2 + · · · + Aη−1 Buη + Aη X̄i , 1 ≤ k ≤ q η+1 ,
(33)
η+1

q
returned by Algorithm 2 afford a finite uniform bisimulation ∼ on ∪k=1
Xk of system (6). By Algorithm 2,
η+1
the number of equivalence classes q
is guaranteed to be greater than z.
By assumption, {Sj1 }qj=1 (9) are disjoint. By Lemma 1, Sj1 is also compact for all j ∈ {1, . . . , q}. Since
the distance between two disjoint compact sets is positive, we have
1
min{d(Sw
, Sv1 ) : w 6= v, 1 ≤ w, v ≤ q} > 0.

Recall

(k)

= {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 = u(1) , u2 , . . . , uk ∈ U},

(k)

= {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 = u(2) , u2 , . . . , uk ∈ U},

C1
C2

..
.

(34)

Cq(k) = {Bu1 + ABu2 + · · · + Ak−1 Buk : u1 = u(q) , u2 , . . . , uk ∈ U},
(k)

we observe that Cj
α∈

(i)
Cv , β

∈

(i)
Cw , w

(34) is a subset of Sj1 for any j ∈ {1, . . . , q} and any k ∈ Z+ , therefore dk = min{kα−βk1 :
6= v, 1 ≤ w, v ≤ q} is uniformly bounded away from zero:
1
dk ≥ min{d(Sw
, Sv1 ) : w 6= v, 1 ≤ w, v ≤ q} > 0, ∀ k ∈ Z+ .

Since lk tends to zero as k tends to infinity, we see that Algorithm 2 terminates.
11

(35)

Recall
(k̃)
X¯1 = C1 + S,
(k̃)
X¯2 = C2 + S,
..
.

(36)

X¯q = Cq(k̃) + S,
we observe that X¯1 , . . . , X¯q afford a finite uniform bisimulation on ∪qj=1 X̄j of system (6) by the derivation
of Theorem 2. We will use this observation to show that sets X1 , . . . , Xqη+1 (33) also afford a finite uniform
bisimulation.
η+1
We first show that ∪qk=1 Xk is an invariant set of system (6). For any x ∈ Xk , by (33), we can write
x = Bu1 + ABu2 + · · · + Aη−1 Buη + Aη x̄
for some (u1 , . . . , uη ) ∈ U η and some x̄ ∈ X̄i with 1 ≤ i ≤ q. Then for any u ∈ U,
Ax + Bu = Bu + ABu1 + A2 Bu2 + · · · + Aη−1 Buη−1 + Aη (Ax̄ + Buη ).
Since ∪qj=1 X̄j is an invariant set of system (6), we have (Ax̄ + Buη ) ∈ X̄j for some 1 ≤ j ≤ q. Recall (33),
η+1

we see that (Ax + Bu) ∈ Xk for some 1 ≤ k ≤ q η+1 , and therefore ∪qk=1 Xk is an invariant set of system (6).
Next, we use an inductive approach to show that the sets Xk , k = 1, . . . , q η+1 (36) are disjoint. Write
U = {u(1) , . . . , u(q) }, we observe that the q 2 sets Bu(i) + AX̄j , i = 1, . . . , q, j = 1, . . . , q are disjoint.
Indeed, consider any Bu(i1 ) + AX̄j 1 and Bu(i2 ) + AX̄j 2 with (i1 , j 1 ) 6= (i2 , j 2 ). If i1 = i2 , then j 1 6=
j 2 . Since X¯1 , . . . , X¯q are disjoint, we have X̄j 1 ∩ X̄j 2 = ∅. Since A is invertible by assumption, we have
AX̄j 1 ∩ AX̄j 2 = ∅, and therefore (Bu(i1 ) + AX̄j 1 ) ∩ (Bu(i2 ) + AX̄j 2 ) = ∅. If i1 6= i2 , from the second part of
the derivation of Theorem 2 (equation (30) through (32)) and the construction of X̄j (34), (36), we see that
(Bu(i1 ) + AX̄j 1 ) ⊂ X̄i1 and (Bu(i2 ) + AX̄j 2 ) ⊂ X̄i2 . Since X¯1 , . . . , X¯q are disjoint, we have X̄i1 ∩ X̄i2 = ∅,
and therefore (Bu(i1 ) + AX̄j 1 ) ∩ (Bu(i2 ) + AX̄j 2 ) = ∅. We conclude that the sets Bu(i) + AX̄j , i = 1, . . . , q,
j = 1, . . . , q are disjoint, where U = {u(1) , . . . , u(q) }.
For the ease of exposition, we use Xj1 , j = 1, . . . , q 2 to denote the q 2 disjoint sets Bu(i) +AX̄j , i = 1, . . . , q,
j = 1, . . . , q. We observe that the q 3 sets Bu(i) + AXj1 , i = 1, . . . , q, j = 1, . . . , q 2 are also disjoint. Indeed,
consider any Bu(i1 ) + AXj11 and Bu(i2 ) + AXj12 with (i1 , j 1 ) 6= (i2 , j 2 ). If i1 = i2 , then j 1 6= j 2 . Since
Xj1 , j = 1, . . . , q 2 are disjoint, we have Xj11 ∩ Xj12 = ∅. Since A is invertible by assumption, we have
AXj11 ∩ AXj12 = ∅, and therefore (Bu(i1 ) + AXj11 ) ∩ (Bu(i2 ) + AXj12 ) = ∅. If i1 6= i2 , by the preceding
paragraph, we see that Xj11 ⊂ X̄l for some 1 ≤ l ≤ q, and therefore
(Bu(i1 ) + AXj11 ) ⊂ (Bu(i1 ) + AX̄l ) ⊂ X̄i1 .
Similarly, we see that (Bu(i2 ) + AXj12 ) ⊂ X̄i2 . Since X¯1 , . . . , X¯q are disjoint, we have X̄i1 ∩ X̄i2 = ∅, and
therefore (Bu(i1 ) + AXj11 ) ∩ (Bu(i2 ) + AXj12 ) = ∅. We conclude that the sets Bu(i) + AXj1 , i = 1, . . . , q,
j = 1, . . . , q 2 are disjoint.
Repeating this argument η times, we conclude that the q η+1 sets Xk , k = 1, . . . , q η+1 (36) are disjoint.
η+1
Next, we define an equivalence relation ∼ on ∪qk=1 Xk as
x ∼ y ⇐⇒ x ∈ Xk and y ∈ Xk for some 1 ≤ k ≤ q η+1 .
We claim that ∼ is a finite uniform bisimulation. Indeed, for any 1 ≤ k ≤ q η+1 , by (33), write Xk as
Xk = Bu1 + ABu2 + · · · + Aη−1 Buη + Aη X̄i . Then for any u ∈ U, AXk + Bu = Bu + ABu1 + A2 Bu2 + · · · +
Aη−1 Buη−1 + Aη (AX̄i + Buη ). Since (AX̄i + Buη ) ⊂ X̄j for some 1 ≤ j ≤ q, we have
(AXk + Bu) ⊂ (Bu + ABu1 + A2 Bu2 + · · · + Aη−1 Buη−1 + Aη X̄j ) = Xk0
for some 1 ≤ k 0 ≤ q η+1 . Therefore (2) is satisfied. Since q η+1 is finite, (3) is also satisfied. This completes
the proof of Theorem 3 and Corollary 1.
12

Lastly, we comment on the fact that the diameter of the equivalence classes Xk can be made arbitrarily
small. For any 1 ≤ k ≤ q η+1 , we have
(k̃)

diam(Xk ) ≤ kAη k1 diam(Ci

+ S) ≤ kAη k1 (diam(A) + diam(S))

Since A is Schur-stable, diam(A) is finite, and kAη k1 can be made arbitrarily small by choosing η large
enough. diam(S) is finite by construction, and we conclude that diam(Xk ) can be made arbitrarily small by
choosing η sufficiently large.

6.4

Derivation of Necessary Conditions

Proof. (of Theorem 4) We will prove by contradiction. Assume ρ(A) > 1, let Av = λv with |λ| > 1, kvk1 = 1,
λ ∈ C, v ∈ Cn . And for any w ∈ Cn , we use Re(w) to denote the real part of w. Define a set O as
O = {α ∈ R+ |Re(γv) ∈ [0], for all |γ| ≤ α, γ ∈ C}.

(37)

We show that O is non-empty and bounded in the following. Write v = [v1 v2 . . . vn ]T , where v1 , . . . , vn ∈ C
and |v1 | + · · · + |vn | = 1. For any γ ∈ C, we have |Re(γvi )| ≤ |γkvi |, therefore
kRe(γv)k1 =

n
X

|Re(γvi )| ≤ |γ|

i=1

n
X

|vi | = |γ|.

i=1

Since Br (0) ⊂ [0] for some r > 0 by assumption, for all γ with |γ| ≤ r/2, Re(γv) ∈ Br (0). Therefore
r/2 ∈ O, and O is nonempty.
Next, we show that O is bounded. Since [0] is bounded by assumption, let [0] ⊂ Bσ (0) for some σ > 0.
Since v = [v1 v2 . . . vn ]T 6= 0n×1 , let |vk | > 0 for some 1 ≤ k ≤ n. Write vk as vk = |vk |eiφ for some
φ ∈ [0, 2π). Assume O is unbounded, then there exist α ∈ O with |α| > 2σ/|vk |. Let γ = (2σ/|vk |)ei(−φ) ,
then |γ| < α. By the definition of O (37), we have Re(γv) ∈ [0]. Observe that
kRe(γv)k1 ≥ |Re(γvk )| = |Re(

2σ i(−φ)
e
|vk |eiφ )| = |Re(2σ)| = 2σ.
|vk |

Therefore Re(γv) ∈
/ Bσ (0), and consequently Re(γv) ∈
/ [0], which draws a contradiction. Therefore O is
bounded.
Next, we define β = sup O. Since O is non-empty and bounded, we have 0 < β < ∞. Then for any
 > 0, there is 0 ≤ δ <  such that Re(κv) ∈
/ [0] for some κ ∈ C and |κ| = β + δ. Choose  = ( |λ|−1
2 )β, and
κ
let κ0 = λ , then
|κ|
β+δ
β+
β + (|λ| − 1)β
|κ0 | =
=
<
<
= β.
|λ|
|λ|
|λ|
|λ|
Therefore |κ0 | < β. Since β = sup O, there exists α ∈ O such that α > |κ0 |. By (37), we see that Re(κ0 v) ∈ [0],
or equivalently Re(κ0 v) ∼ 0. Since ∼ is a finite uniform bisimulation, by (2) and letting the input u be zero,
we have ARe(κ0 v) ∼ 0. We observe that
ARe(κ0 v) = Re(Aκ0 v) = Re(κ0 (Av)) = Re(κ0 λv) = Re(κv),
therefore Re(κv) ∼ 0 ,which draws a contradiction. We conclude that the assumption ρ(A) > 1 is false, and
therefore ρ(A) ≤ 1.
Proof. (of Corollary 2) We will prove by contradiction. Assume |a| > 1, and use [0] to denote the equivalence
class [0] = {x ∈ S|x ∼ 0}. By the assumption Br (0) ⊂ [0] for some r > 0, define β as
β = sup{x ∈ S|[0, x] ⊂ [0]},

(38)

where [0, x] is the closed interval between 0 and x. Since int([0]) is nonempty, there is  such that [0, ) ⊂ [0],
therefore the supremum is well defined, and β > 0.
13

First, we consider the case β < ∞. Clearly [0, β) ⊂ [0]. By the definition of β, we have that for any
 > 0, there is 0 ≤ δ <  such that
β+δ ∈
/ [0].
(39)
Let  = (a2 − 1)β > 0, and let δ denote the nonnegative number that satisfy (39). We observe that
z=

β+δ
< β,
a2

therefore z ∼ 0. Since ∼ is a finite uniform bisimulation, when the input is 0 we have az ∼ 0, and a2 z ∼ 0.
This draws a contradiction with (39).
For the case β = ∞, let β 0 = inf{x ∈ S|[x, 0] ⊂ [0]}, then β 0 > −∞, otherwise for any x ∈ R, x ∈ [0],
which implies R = [0] and there is only one equivalence class. Next, for any  > 0, there is 0 ≤ δ <  such
that β 0 − δ ∈
/ [0]. Choose  = (1 − a2 )β 0 and z = (β 0 − δ)/a2 , then the preceding argument follows.

7

Illustrative Examples

In this section, we present a set of illustrative examples: In Example 1, we illustrate the difference between
the notion of finite uniform bisimulation and the notion of finite bisimulation stated in [19]; in Example
2, we show that additional assumptions, besides the conditions in Theorem 1, are needed to guarantee the
existence of arbitrarily many equivalence classes; in Example 3, we show that the condition “[0] is bounded"
in Theorem 4 cannot be dropped; in Example 4, we illustrate the analytical result in Theorem 1, discuss
how to construct a DFM approximation of the original system, and apply Algorithm 2 to construct many
equivalence classes.
Example 1. (Example 2.14, [19]) Consider system

2
0
A =  −1 −7
0
4

(6) with parameters



1 2
−1
11  , B =  1 1 
1 1
6

According to [19], a finite bisimulation with eight equivalence classes {q1 , . . . , q8 } is constructed. If we
choose x = [1 − 2 − 3]T ∈ q1 , x0 = [8, −18, −24]T ∈ q1 and let input u = [0 60]T , then Ax + Bu =
[125 40 34]T ∈ q2 , and Ax0 + Bu = [160 − 86 − 156]T ∈ q1 . Therefore this finite bisimulation is not a “finite
uniform bisimulation" as defined in Definition 1.
Example 2. Consider system (6) with parameters


0.5 0
A=
,
0 0
and


U=

1
0


B=

1
0

0
1


(40)

   
  
0
0
0
,
,
,
1
−1
0

We calculate, and plot cl(A):
cl(A) = {(x, y) ∈ R2 |x = 0, −2 ≤ y ≤ 2} ∪ {(x, y) ∈ R2 |x = 1, −1 ≤ y ≤ 1}

14

(41)

Figure 1: 2 and only 2 equivalence classes.
In the above figure, W and V represents a disconnection of cl(A). We see that both cl(A) ∩ W and
cl(A) ∩ V are connected. Therefore, we cannot apply the analytical result in Theorem 1 to generate more
than two equivalence classes, because such result relies on the disconnectedness of an invariant set.
Example 3. Given system (6) with parameters: A = diag({2, 0.5}) (a diagonal matrix with diagonal entries
2 and 0.5), B is the identity matrix, and U = {[0 0]T }. Let X1 = {(x, y) ∈ R2 : 1 < |y| < 2}, and
X2 = {(x, y) ∈ R2 : |y| < 1}, then we see that X1 , X2 afford a regular finite uniform bisimulation on X1 ∪ X2 ,
which is an invariant set, and Br (0) ⊂ [0] for r = 0.5, and ρ(A) = 2 > 1.
Example 4. Consider system (6) with parameters:




0.25 −0.15
1 0
A=
, B=
(42)
0
0.1
0 1
and
  
   
  
1
−1
0
0
0
U=
,
,
,
,
0
0
1
−1
0
Since A is diagonalizable, we have


(1/4)n (1/10)n − (1/4)n
An =
, n = 0, 1, 2, · · ·
0
(1/10)n
and we can show that cl(A) is a subset of:
[
1 1
4 4
{(±1, ±1), (0, 0)} + {(x, y) : x ∈ [− , ], y ∈ [− , ]}
9 9
9 9
Therefore cl(A) is not connected.
By the derivation of Theorem 1, we find a finite uniform bisimulation ∼ on an invariant set of this system:

Figure 2: 2-d finite uniform bisimulation example.
15

X1 , . . . , X5 shown in Figure 2 afford a finite uniform bisimulation ∼ on an invariant set S = ∪5i=1 Xi of
system (6). The points a, b, c, d are given by:
22 10
10 10
4 1
4 1
, ), b = ( , − ), c = ( , ), d = ( , − )
9 9
9
9
9 9
9 9
and Figure 2 is symmetric with respect to the origin. Particularly, the set S is the convex hull of points:
{a, b, −a, −b}.
Given ∼, we can construct a DFM that is uniformly bisimilar to the original system. Particularly, we
associate each equivalence class Xi to a discrete state qi of the DFM, i = 1, . . . , 5. The state transitions
of the DFM can be determined based on (5): For instance, if the current state of the DFM is q1 , and the
current input is [0 1]T , then the next state of the DFM is q3 .
Since this example also satisfies the conditions in Theorem 3, we can also use Algorithm 2 to generate a
finite uniform bisimulation with an arbitrarily large number of equivalence classes. In particular, we generate
two finite uniform bisimulations with 5 equivalence classes, and 25 equivalence classes respectively.
a=(

(a) 5 equivalence classes.

(c) 25 equivalence classes.

(b) Zoom in on 1 equivalence class.

(d) Zoom in on 1 equivalence class.

Figure 3: Finite uniform bisimulations with many equivalence classes.
In the above, Figure 3a shows the 5 equivalence classes generated by Algorithm 2, and Figure 3b shows
one particular equivalence class (the boxed rectangular area in Figure 3a). Similarly Figure 3c shows the
25 equivalence classes, and Figure 3d shows one particular equivalence class. As shown in Figure 3b and
Figure 3d, an equivalence class computed by Algorithm 2 is the union of all the polytopes (in this case
parallelograms). This is in accordance with the construction of the equivalence classes.

8

Conclusions

In this paper we propose notions of finite uniform bisimulation and regular finite uniform bisimulation. We
then present a sufficient condition for the existence of finite uniform bisimulations: If the forced response of a
Schur stable system is not connected, then the system admits a finite uniform bisimulation. In this case, we
construct an algorithm to compute finite uniform bisimulations. Furthermore, we discuss the existence and
construction of an arbitrarily large number of equivalence classes. We also present a necessary condition for
the existence of regular finite uniform bisimulation. Future works include closing the gap between necessary
conditions and sufficient conditions, and extending the current result to systems with more general dynamics.
16

9

Appendix

For the sake of completeness, we review here relevant mathematical concepts and notation, beginning with
the concept of equivalence relations [14]. Given a set A, a subset ∼ of A × A is called a relation on A. With
some slight abuse of notation, we write a ∼ b, read a is equivalent to b, to mean that (a, b) is an element of
the relation ∼. A relation ∼ on A is an equivalence relation if for any a, b, c ∈ A, we have:
(i) a ∼ a (reflexive),
(ii) If a ∼ b, then b ∼ a (symmetric),
(iii) If a ∼ b and b ∼ c, then a ∼ c (transitive).
An equivalence relation ∼ on a set A can be used to partition A into equivalence classes. We use [x] to
denote the equivalence class of x, defined as [x] = {y ∈ A|y ∼ x}. Note that this indeed defines a partition
as the following properties are satisfied:
(i) [x] 6= ∅, ∀x ∈ A,
(ii) [x] =
6 [y] ⇒ [x] ∩ [y] = ∅,
[
(iii)
[x] = A.
x∈A

Next, we review relevant concepts in analysis. A point x ∈ Rn consists of an n−tuple of real numbers
x = (x1 , x2 , . . . , xn ). For the purpose of illustration, we use the 1-norm to review relevant concepts. The 1norm of x is denoted by kxk1 and is defined as kxk1 = (|x1 |+· · ·+|xn |). The distance between two points x and
y is then simply kx − yk1 . Given a set A in Rn , the diameter of A is defined as diam(A) = sup{ky − xk1 : x ∈
A, y ∈ A}. The open ball in Rn centered at x and of radius r is defined by Br (x) = {y ∈ Rn : ky − xk1 < r}.
Given a set A in Rn , a point x is a closure point of A if for every r > 0, the ball Br (x) contains a point of
A. Similarly, a point x is a limit point of A if for every r > 0, the ball Br (x) contains a point of A that is
distinct from x. The closure of A, cl(A), consists of all closure points of A. A point x ∈ A is an interior
point of A if there exists r > 0 such that Br (x) ⊂ A. The interior of A, int(A), consists of all interior points
of A. A boundary point of A is a point which is in cl(A) but not in int(A). The boundary of A, ∂A, consists
of all boundary points of A.
Lastly, we review the notion of spectral radius of a square matrix. Given a square matrix A, the spectral
radius of A is the nonnegative real number ρ(A) = max{|λ| : λ is an eigenvalue of A}. Given a square
matrix A, the 1-induced norm of A is defined as kAk1 = max kAxk1 . Recall that induced norms satisfy
kxk1 =1

the sub-multiplicative property: kABk1 ≤ kAk1 kBk1 .

10

Acknowledgments

This research was supported by NSF CAREER award 0954601 and AFOSR Young Investigator award
FA9550-11-1-0118.

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, July 2000.
[2] A. Chutinan and B. H. Krogh. Computing approximating automata for a class of hybrid systems.
Mathematical and Computer Modelling of Dynamical Systems, 6(1):30–50, 2000.
[3] A. Chutinan and B. H. Krogh. Verification of infinite-state dynamic systems using approximate quotient
transition systems. IEEE Transactions on Automatic Control, 46(9):1401–1410, 2001.
[4] J. E. R. Cury, B. H. Krogh, and T. Niinomi. Synthesis of supervisory controllers for hybrid systems
based on approximating automata. IEEE Transactions on Automatic Control, 43(4):564–568, 1998.
17

[5] D. Fan and D. C. Tarraf. On existence of finite uniform bisimulations for linear systems with finite input
alphabets. Proceedings of the 54th IEEE International Conference on Control and Decision, December
2015. To appear.
[6] E. A. Gol, X. Ding, M. Lazar, and C. Belta. Finite bisimulations for switched linear systems. IEEE
Transactions on Automatic Control, 59(12):3122–3134, 2014.
[7] R. A. Horn and C. R. Johnson. Matrix Analysis. Cambridge University Press, 1990.
[8] M. Kloetzer and C. Belta. A fully automated framework for control of linear systems from temporal
logic specifications. IEEE Transactions on Automatic Control, 53(1):287–297, February 2008.
[9] G. Lafferriere, G. J. Pappas, and S. Sastry. O-minimal hybrid systems. Mathematics of Control, Signals
and Systems, 13(1):1–21, 2000.
[10] J. Liu, N. Ozay, U. Topcu, and R. M. Murray. Synthesis of reactive switching protocols from temporal
logic specifications. IEEE Transactions on Automatic Control, 58(7):1771–1785, 2013.
[11] J. Lunze. Qualitative modeling of linear dynamical systems with quantized state measurements. Automatica, 30:417–431, 1994.
[12] T. Moor and J. Raisch. Supervisory control of hybrid systems whithin a behavioral framework. Systems
& Control Letters, Special Issue on Hybrid Control Systems, 38:157–166, 1999.
[13] T. Moor, J. Raisch, and S. D. O’Young. Discrete supervisory control of hybrid systems by l-complete
approximations. Discrete Event Dynamic Systems: Theory and Applications, 12:83–107, 2002.
[14] W. K. Nicholson. Introduction to Abstract Algebra. Wiley, 2012.
[15] D. Park. Concurrency and automata on infinite sequences. In Proceedings of the Fifth GI Conference
on Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167–183.
Springer-Verlag, 1981.
[16] G. Reißig. Computing abstractions of nonlinear systems. IEEE Transactions on Automatic Control,
56(11):2583–2598, November 2011.
[17] E. M. Stein and R. Shakarchi. Real analysis: measure theory, integration, and Hilbert spaces. Princeton
University Press, 2009.
[18] P. Tabuada. Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, 2009.
[19] P. Tabuada and G. J. Pappas. Linear time logic control of discrete-time linear systems. IEEE Transactions on Automatic Control, 51(12):1862–1877, 2006.
[20] D. C. Tarraf. A control-oriented notion of finite state approximation. IEEE Transactions on Automatic
Control, 57(12):3197–3202, 2012.
[21] D. C. Tarraf. An input-output construction of finite state ρ/µ approximations for control design. IEEE
Transactions on Automatic Control, Special Issue on Control of Cyber-Physical Systems, 59(12):3164–
3177, Dec 2014.
[22] D. C. Tarraf, A. Megretski, and M. A. Dahleh. Finite approximations of switched homogeneous systems
for controller synthesis. IEEE Transactions on Automatic Control, 56(5):1140–1145, May 2011.
[23] K. Tsumura. Approximation of discrete time linear systems via bit length of memory. In Proceedings of
the 17th International Symposium on Mathematical Theory of Networks and Systems, pages 1066–1072,
Kyoto, Japan, July 2006.
[24] K. Tsumura. A lower bound of the necessary bit length of memory for approximation of discrete time
systems. In Proceedings of the 46th IEEE Conference on Decision and Control, pages 2241–2246, New
Orleans, LA, U.S.A., December 2007.
18

[25] A. J. van der Schaft. Equivalence of dynamical systems by bisimulation. IEEE Transactions on Automatic Control, 49(12):2160–2172, 2004.
[26] B. Yordanov, J. Tumová, I. Cerná, J. Barnat, and C. Belta. Temporal logic control of discrete-time
piecewise affine systems. IEEE Transactions on Automatic Control, 57(6):1491–1504, 2012.

19

