Output Feedback Controller Design with Symbolic Observers
for Cyber-physical Systems
Masashi Mizoguchi

Toshimitsu Ushio

Graduate School of Engineering Science
Osaka University
Osaka, Japan
mizoguchi@hopf.sys.es.osaka-u.ac.jp
ushio@sys.es.osaka-u.ac.jp

In this paper, we design a symbolic output feedback controller of a cyber-physical system (CPS).
The physical plant is modeled by an infinite transition system. We consider the situation that a finite
abstracted system of the physical plant, called a c-abstracted system, is given. There exists an approximate alternating simulation relation from the c-abstracted system to the physical plant. A desired
behavior of the c-abstracted system is also given, and we have a symbolic state feedback controller
of the physical plant. We consider the case where some states of the plant are not measured. Then,
to estimate the states with abstracted outputs measured by sensors, we introduce a finite abstracted
system of the physical plant, called an o-abstracted system, such that there exists an approximate
simulation relation. The relation guarantees that an observer designed based on the state of the oabstracted system estimates the current state of the plant. We construct a symbolic output feedback
controller by composing these systems. By a relation-based approach, we proved that the controlled
system approximately exhibits the desired behavior.

1

Introduction

Over the past few decades, the control of hybrid systems has been studied [13]. It is a main issue in
hybrid systems to find an algorithmic procedure for designing a finite symbolic controller. The physical
plant has real-valued variables, and its model is an infinite-state system that has too many uncertainties.
Then, finite state abstraction is introduced in verification and synthesis problems of hybrid systems [22].
The behavior of a finite system can be regarded as a process. A simulation / bisimulation relation is a key
notion that evaluates correctness between two processes [14]. If there exists a simulation / bisimulation
relation, the abstracted plant correctly describes the behavior of the physical plant. But, these relations
are often too restrictive in terms of the abstraction because the state set of a hybrid system is infinite [2].
Recently, approximate abstraction is considered with approximate simulation / bisimulation relations.
These relations are evaluated by Lyapunov-like functions called simulation / bisimulation functions [10,
11, 12, 16, 21].
Another key concept between two processes is an alternating simulation relation proposed in [1].
This notion is used not only in multi-agent systems and game automata but also to describe a relationship
between a feedback controller and a plant. The control problem of a finite system can be solved by exact
alternating simulation relations [22]. Approximated alternating simulation relations are also introduced
as well as simulation / bisimulation relations to consider abstraction [10].
A cyber-physical system (CPS) contains communication networks, which cause disturbances and
noises such as data dropouts. A control performance is often degraded by them, so robustness of the
CPS is important. An approach to design of a symbolic controller under the existence of disturbances is
shown in [3, 4], and approximated relations are used in [17]. It is shown that the input-output dynamical
Kargahi and Trivedi: Verification and Validation of
Cyber-Physical Systems 2016 (V2CPS-16)
EPTCS 232, 2016, pp. 37–51, doi:10.4204/EPTCS.232.7

c Masashi Mizoguchi & Toshimitsu Ushio
This work is licensed under the
Creative Commons Attribution License.

38

Output Feedback Controller Design with Symbolic Observers for Cyber-physical Systems

stability (IODS) is preserved under the abstraction if there exists an approximated alternating simulation
relation [18, 19, 20, 23].
On the other hand, the design methods of the output feedback controller have been proposed. There
are a lot of approaches such as game strategies and specification-based estimators [6, 7, 9]. Especially,
finite state abstraction is used in [8, 24, 25]. But, these are not based on (alternating) simulation relations.
Relation-based approaches can be seen in [5, 26] where an observer-based control problem for discrete
event systems is considered. These approaches are based on the exact alternating simulation / bisimulation relations. The output feedback controller based on approximated relations is designed in [15] under
the assumption that the relation is based on distance between the state of the physical plant and the state
of the abstracted plant.
In this paper, we propose a symbolic output feedback controller without introducing the distance. It
is shown that there exists an approximate contractive alternating simulation relation from the proposed
symbolic controller to the physical plant. Since the approximate contractive alternating simulation relation has the contraction property, the abstraction error between the physical plant and the symbolic
controller does not diverge. Thus, the plant controlled by the proposed output feedback controller approximately exhibits the desired behavior.
The rest of this paper is organized as follows. In Section 2, we define a system as a transition
system, and introduce notions of approximated relations. Moreover, we review an approach to design of
a symbolic state feedback controller. In Section 3, we design a symbolic observer based on approximated
relations. In Section 4, we construct an output feedback controller. It is shown that the controlled plant by
the controller approximately exhibits the desired behavior. The proof is shown in Section 5. In Section
6, we consider an example to demonstrate how the proposed controller works.

2
2.1

Preliminaries
Simulation Relations

In this subsection, we review several fundamental notions for transition systems [19, 20].
Definition 1 A system S is a tuple (X, X0 ,U, r), where:
• X is a set of states;
• X0 ⊆ X is a set of initial states;
• U is a set of inputs;
• r : X ×U → 2X is a transition map.
For any x ∈ X, let U(x) = {u ∈ U | r(x, u) 6= 0}.
/
Let S1 = (X1 , X10 ,U1 , r1 ) and S2 = (X2 , X20 ,U2 , r2 ) be two systems. For a relation R ⊆ X1 × X2 ×U1 ×
U2 over the state sets X1 , X2 and the input sets U1 ,U2 , denoted by RX ⊆ X1 × X2 is a projection of R to the
state sets X1 , X2 defined as follows:
RX = {(x1 , x2 ) ∈ X1 × X2 | ∃u1 ∈ U1 , ∃u2 ∈ U2 : (x1 , x2 , u1 , u2 ) ∈ R}.
Definition 2 Let S1 = (X1 , X10 ,U1 , r1 ) and S2 = (X2 , X20 ,U2 , r2 ) be two systems, let κ, λ ∈ R≥0 , β ∈ [0, 1[
be some parameters, and consider a map d : U1 × U2 → R≥0 . We call a parameterized (by ε ∈ [κ, ∞[)

Masashi Mizoguchi & Toshimitsu Ushio

39

relation R(ε) ⊆ X1 × X2 × U1 × U2 a κ-approximate (β , λ )-contractive simulation relation ((κ, β , λ )acSR) from S1 to S2 with d if R(ε) ⊆ R(ε 0 ) holds for all ε ≤ ε 0 and the following two conditions hold for
all ε ∈ [κ, ∞[.
1. ∀x10 ∈ X10 , ∃x20 ∈ X20 : (x10 , x20 ) ∈ RX (κ);
2. ∀(x1 , x2 ) ∈ RX (ε), ∀u1 ∈ U1 (x1 ), ∃u2 ∈ U2 (x2 ):
(x1 , x2 , u1 , u2 ) ∈ R(ε) ∧ ∀x10 ∈ r1 (x1 , u1 ), ∃x20 ∈ r2 (x2 , u2 ) : (x10 , x20 ) ∈ RX (κ + β ε + λ d(u1 , u2 )).
We call R(ε) a simulation relation (SR) from S1 to S2 if R(ε) is a (0, 0, 0)-acSR from S1 to S2 .
Definition 3 Let S1 = (X1 , X10 ,U1 , r1 ) and S2 = (X2 , X20 ,U2 , r2 ) be two systems, let κ, λ ∈ R≥0 , β ∈ [0, 1[
be some parameters, and consider a map d : U1 × U2 → R≥0 . We call a parameterized (by ε ∈ [κ, ∞[)
relation R(ε) ⊆ X1 × X2 × U1 × U2 a κ-approximate (β , λ )-contractive alternating simulation relation
((κ, β , λ )-acASR) from S1 to S2 with d if R(ε) ⊆ R(ε 0 ) holds for all ε ≤ ε 0 and the following two
conditions hold for all ε ∈ [κ, ∞[.
1. ∀x10 ∈ X10 , ∃x20 ∈ X20 : (x10 , x20 ) ∈ RX (κ);
2. ∀(x1 , x2 ) ∈ RX (ε), ∀u1 ∈ U1 (x1 ), ∃u2 ∈ U2 (x2 ):
(x1 , x2 , u1 , u2 ) ∈ R(ε) ∧ ∀x20 ∈ r2 (x2 , u2 ), ∃x10 ∈ r1 (x1 , u1 ) : (x10 , x20 ) ∈ RX (κ + β ε + λ d(u1 , u2 )).
We call R(ε) an alternating simulation relation (ASR) from S1 to S2 if R(ε) is a (0, 0, 0)-acASR from S1
to S2 .
Definition 4 Let S1 = (X1 , X10 ,U1 , r1 ) and S2 = (X2 , X20 ,U2 , r2 ) be two systems, and let R ⊆ X1 × X2 ×
U1 × U2 be a relation. We define the composition of S1 and S2 with respect to R, denoted by S :=
S1 ×R S2 = (X, X0 ,U, r) where:
• X = X1 × X2 ;
• X0 = (X10 × X20 ) ∩ RX ;
• U = U1 ×U2 ;
• r : X ×U → 2X is defined as follows: (x10 , x20 ) ∈ r((x1 , x2 ), (u1 , u2 )) if and only if
x10 ∈ r1 (x1 , u1 ) ∧ x20 ∈ r2 (x2 , u2 ) ∧ (x1 , x2 , u1 , u2 ) ∈ R ∧ (x10 , x20 ) ∈ RX .
If R(ε) is a (κ, β , λ )-acSR or a (κ, β , λ )-acASR from S1 to S2 with d, we replace the above definitions
of X0 and r with the following conditions:
• X0 = (X10 × X20 ) ∩ RX (κ);
• r : X ×U → 2X is defined as follows: (x10 , x20 ) ∈ r((x1 , x2 ), (u1 , u2 )) if and only if
x10 ∈ r1 (x1 , u1 ) ∧ x20 ∈ r2 (x2 , u2 ) ∧ (x1 , x2 , u1 , u2 ) ∈ R(e(x1 , x2 ))
∧ (x10 , x20 ) ∈ RX (κ + β e(x1 , x2 ) + λ d(u1 , u2 )),
where e(x1 , x2 ) := inf{ε ∈ R≥0 | (x1 , x2 ) ∈ RX (ε)}.

40

2.2

Output Feedback Controller Design with Symbolic Observers for Cyber-physical Systems

State Feedback

In this subsection, we review the state feedback control [19, 20]. A physical plant to be controlled,
denoted by S = (X, X0 ,U, r), is a discrete time system, and its state set X is a Euclidean space. Thus, S is
an infinite transition system. In order to design a digital controller, we introduce a finite abstracted model
of the plant that is implemented in the cyber space. We consider an abstracted system Ŝ = (X̂, X̂0 , Û, r̂) of
the plant S, called a c-abstracted system, such that there exists a (κ, β , λ )-acASR R(ε) ⊆ X̂ × X × Û ×U
from Ŝ to S. A desired behavior of the plant is described by ŜC = (X̂C , X̂C0 , ÛC , r̂C ) based on Ŝ in such a
way that there exists an ASR R̂C ⊆ X̂C × X̂ × ÛC × Û from ŜC to Ŝ. Then, the following theorem shows
the existence of a symbolic state feedback controller [19, 20].
Theorem 1 Let ŜC = (X̂C , X̂C0 , ÛC , r̂C ), Ŝ = (X̂, X̂0 , Û, r̂), and S = (X, X0 ,U, r) be systems, let κ, λ ∈
R≥0 , β ∈ [0, 1[ be some parameters, and consider a map d : U × Û → R≥0 . Assume that there exist an
ASR R̂C ⊆ X̂C × X̂ × ÛC × Û from ŜC to Ŝ and a (κ, β , λ )-acASR R(ε) ⊆ X̂ × X × Û × U from Ŝ to S
with d. Then, the following relation RC (ε) ⊆ (X̂C × X̂) × X × (ÛC × Û) × U is a (κ, β , λ )-acASR from
SC := ŜC ×R̂C Ŝ to S with dC ((ûC , û), u) = d(û, u).
RC (ε) = {((x̂C , x̂), x, (ûC , û), u) | (x̂, x, û, u) ∈ R(ε) ∧ (x̂C , x̂) ∈ R̂CX }.

(1)

Theorem 1 implies that SC , which is the composition of the abstracted systems ŜC and Ŝ, is a controller of S. In the case where the state x of S is fully observed, we can determine the state x̂ of Ŝ by
the relation R(ε). Then, the state x̂C of ŜC is determined by the relation R̂C . The controller determines a
control input ûC ∈ ÛC such that r̂C (x̂C , ûC ) 6= 0.
/
However, in general, all states are not always measured. Moreover, the output value is abstracted by
the resolution of sensors. Then, in the next section, we introduce a symbolic observer based on abstracted
outputs.

3

Observer Design

Let Y be a set of outputs, and H : X → Y be an output map of the plant S = (X, X0 ,U, r). We call
(S,Y, H) = (X, X0 ,U, r,Y, H) a plant with outputs. The observer introduced in this section is based on
the concept of observers for discrete event systems [5]. In order that the observer always estimates the
current state of the plant, it must simulate any behavior of the plant. Thus, we introduce an abstracted
system Š = (X̌, X̌0 , Ǔ, ř) of the plant S, called an o-abstracted system, such that there exists an acSR Ř(ε)
from S to Š. Note that Š 6= Ŝ in general. The acSR Ř(ε) is based on measured outputs of the physical
plant and satisfies the following condition:
∀x1 ∈ X, ∀x2 ∈ X, ∀x̌ ∈ X̌ : (x1 , x̌) ∈ ŘX (ε) ∧ (x2 , x̌) ∈ ŘX (ε) ⇒ H(x1 ) = H(x2 ).

(2)

Definition 5 Let (S,Y, H) be a plant with outputs and Š be an o-abstracted system, let κ 0 , λ 0 ∈ R≥0 ,
β 0 ∈ [0, 1[ be some parameters, and consider a map ď : X × X̌ → R≥0 . There exists a (κ 0 , β 0 , λ 0 )-acSR
Ř(ε) ⊆ X × X̌ ×U × Ǔ from S to Š with ď. Then, we define a system S̃ = (X̃, X̃0 , Ũ, r̃) where:
• X̃ = 2X̌ \ {0};
/
• X̃0 = 2X̌0 \ {0}
/ ⊆ X̃;
• Ũ = Ǔ;

Masashi Mizoguchi & Toshimitsu Ushio

41

• r̃ : X̃ × Ũ → 2X̃ is defined as follows:
r̃(x̃, ǔ) = {x̃0 ∈ X̃ | ∀x̌0 ∈ x̃0 , ∃x̌ ∈ x̃, ∃x ∈ X, ∃u ∈ U, ∃x0 ∈ r(x, u), ∃ε ∈ [κ 0 , ∞[:
x̌0 ∈ ř(x̌, ǔ) ∧ (x, x̌, u, ǔ) ∈ Ř(ε) ∧ (x0 , x̌0 ) ∈ ŘX (κ 0 + β 0 ε + λ 0 ď(u, ǔ))},
where ŘX (ε) ⊆ X × X̌ is the projection of a relation induced by Ř(ε) defined as follows:
ŘX (ε) = {(x, x̌) ∈ X × X̌ | ∃u ∈ U, ∃ǔ ∈ Ǔ : (x, x̌, u, ǔ) ∈ Ř(ε)}.
We call S̃ an observer of S induced by Š.
Theorem 2 Let (S,Y, H) be a plant with outputs, Š is an o-abstracted system, and there exists a (κ 0 , β 0 , λ 0 )acSR Ř(ε) ⊆ X × X̌ × U × Ǔ from S to Š with ď for some κ 0 , λ 0 ∈ R≥0 , β 0 ∈ [0, 1[, and a map ď :
X × X̌ → R≥0 . The observer S̃ is induced by Š as in Definition 5. Then, the following relation R0 (ε) ⊆
X × X̃ ×U × Ũ is a (κ 0 , β 0 , λ 0 )-acSR from (S,Y, H) to S̃ with ď:
R0 (ε) = {(x, x̃, u, ǔ) | ∃x̌ ∈ x̃ : (x̌, x, u, ǔ) ∈ Ř(ε)}.

(3)

Proof We will show that R0 (ε) satisfies the conditions of a (κ 0 , β 0 , λ 0 )-acSR from S to S̃ with ď.
1. Consider any x0 ∈ X0 . Let H(x0 ) = y0 . We consider the following state x̃0 of S̃:
x̃0 = {x̌0 ∈ X̌0 | ∃x p0 ∈ X0 : H(x p0 ) = y0 ∧ (x p0 , x̌0 ) ∈ ŘX (κ 0 )}.
Note that by the (κ 0 , β 0 , λ 0 )-acSR Ř(ε), x̃0 is a non-empty set. Recall that X̃0 = 2X̌0 \ {0}.
/ Then,
we have x̃0 ∈ X̃0 . By the definition of R0 (ε), (x0 , x̃0 ) ∈ R0X (κ 0 ) holds.
2. First, consider any (x, x̃) ∈ R0X (ε). We have
∃x̌ ∈ x̃ : (x, x̌) ∈ ŘX (ε).
Choose any u ∈ U(x). By the (κ 0 , β 0 , λ 0 )-acSR Ř(ε), there exists ǔ ∈ Ũ(x̃) such that (x, x̌, u, ǔ) ∈
Ř(ε). Now, we have (x, x̃, u, ǔ) ∈ R0 (ε).
Next, consider any x0 ∈ r(x, u). Let H(x0 ) = y0 . We consider the following state x̃0 of S̃:
x̃0 = {x̌0 ∈ X̌ | ∃x̌ ∈ x̃, ∃x p ∈ X, ∃x0p ∈ r(x p , u) :
x̌0 ∈ ř(x̌, ǔ) ∧ H(x0p ) = y0 ∧ (x p , x̌, u, ǔ) ∈ Ř(ε) ∧ (x0p , x̌0 ) ∈ ŘX (κ 0 + β 0 ε + λ 0 ď(u, ǔ))}.
Note that by the (κ 0 , β 0 , λ 0 )-acSR Ř(ε), x̃0 is a non-empty set. Moreover, we have
∃x̌0 ∈ x̃0 : (x0 , x̌0 ) ∈ ŘX (κ 0 + β 0 ε + λ 0 ď(u, ǔ)).
By the definition of r̃, x̃0 ∈ r̃(x̃, ǔ) holds. Thus, by the definition of R0 (ε), (x0 , x̃0 ) ∈ R0X (κ 0 + β 0 ε +
λ 0 ď(u, ǔ)) holds.

Theorem 2 implies that for the current state x̃ of the observer, there always exists x̌ ∈ x̃ such that x̌ is
an o-abstracted state of the current state x of the plant. Thus, S̃ lists up all candidates of x̌.

42

4

Output Feedback Controller Design with Symbolic Observers for Cyber-physical Systems

Output Feedback Control System

In this section, we construct an output feedback system with the observer defined in the previous section.
Definition 6 We define a system Ŝ = (X̂, X̂0 , Û, r̂) induced by Ŝ = (X̂, X̂0 , Û, r̂) where:
• X̂ = 2X̂ \ {0};
/
• X̂0 = 2X̂0 \ {0}
/ ⊆ X̂;
• Û = Û;
• r̂ : X̂ × Û → 2X̂ is defined as follows:
( S
2 x̂∈x̂ r̂(x̂,û) \ {0}
/
if ∀x̂ ∈ x̂ : r̂(x̂, û) 6= 0,
/
r̂(x̂, û) =
0/
otherwise.
Intuitively, each x̂ ∈ x̂ corresponds to (at least) one candidate listed up by the observer. Recall that
S̃ is induced by Š that is different from Ŝ. Then, we consider x̂ such that each c-abstracted state x̂ ∈ x̂
corresponds to (at least) one o-abstracted state x̌ ∈ x̃. The transition map r̂ is defined only when r̂ is
defined for all x̂ ∈ x̂.
We define ŜC induced by ŜC as well as Ŝ induced by Ŝ.
Definition 7 We define a system ŜC = (X̂C , X̂C0 , ÛC , r̂C ) induced by ŜC = (X̂C , X̂C0 , ÛC , r̂C ) where:
• X̂C = 2X̂C \ {0};
/
• X̂C0 = 2X̂C0 \ {0}
/ ⊆ X̂C ;
• ÛC = ÛC ;
• r̂C : X̂C × ÛC → 2X̂C is defined as follows:
( S
2 x̂C ∈x̂C r̂C (x̂C ,ûC ) \ {0}
/
if ∀x̂C ∈ x̂C : r̂C (x̂C , ûC ) 6= 0,
/
r̂C (x̂C , ûC ) =
0/
otherwise.
Then, we have the following main theorems.
Theorem 3 Consider the same condition as Theorem 1. In addition, let Š = (X̌, X̌0 , Ǔ, ř) be an oabstracted system, and there exists a (κ 0 , β 0 , λ 0 )-acSR Ř(ε) ⊆ X × X̌ × U × Ǔ from S to Š with ď for
some κ 0 , λ 0 ∈ R≥0 , β 0 ∈ [0, 1[, and a map ď : X × X̌ → R≥0 . Let S̃ = (X̃, X̃0 , Ũ, r̃) be an observer induced
by Š as in Definition 5. Let Ŝ = (X̂, X̂0 , Û, r̂) and ŜC = (X̂C , X̂C0 , ÛC , r̂C ) be systems induced by a cabstracted system Ŝ and ŜC , respectively as in Definitions 6 and 7. Assume that R̂C satisfies (4), that there
exists a map d̄ : Û × Ǔ → R≥0 satisfying (5), and that R(ε) and Ř(ε) satisfy (6) and (7), respectively.
∀ûC ∈ ÛC , ∃û ∈ Û, ∀(x̂C , x̂) ∈ R̂CX : ûC ∈ ÛC (x̂C ) ⇒ (x̂C , x̂, ûC , û) ∈ R̂C ,

(4)

∀û ∈ Û, ∀u ∈ U, ∀ǔ ∈ Ǔ : d̄(û, ǔ) ≥ d(û, u) + ď(u, ǔ),

(5)

∀ε ∈ [κ, ∞[, ∀û ∈ Û, ∃u ∈ U, ∀(x̂, x) ∈ RX (ε) : û ∈ Û(x̂) ⇒ (x̂, x, û, u) ∈ R(ε),

(6)

∀ε ∈ [κ, ∞[, ∀u ∈ U, ∃ǔ ∈ Ǔ, ∀(x, x̌) ∈ ŘX (ε) : u ∈ U(x) ⇒ (x, x̌, u, ǔ) ∈ Ř(ε).

(7)

Masashi Mizoguchi & Toshimitsu Ushio

43

Figure 1: The proposed output feedback controller S̄C = SC ×RC (ε) S̃ consisting of SC = ŜC ×R̂C Ŝ and
the observer S̃.
Let SC := ŜC ×R̂C Ŝ. Then, the following relation RC (ε) ⊆ (X̂C × X̂) × X̃ × (ÛC × Û) × Ũ is a
(κ + κ 0 , max{β , β 0 }, max{λ , λ 0 })-acASR from SC to S̃ with dC ((ûC , û), ǔ) = d̄(û, ǔ).
RC (ε) = {((x̂C , x̂), x̃, (ûC , û), ǔ) | (x̂, x̃, û, ǔ) ∈ R(ε) ∧ (x̂C , x̂) ∈ R̂CX },

(8)

where the relations R̂C ⊆ X̂C × X̂ × ÛC × Û and R(ε) ⊆ X̂ × X̃ × Û × Ũ are defined by (9) and (10),
respectively.
R̂C = {(x̂C , x̂, ûC , û) | ∀x̂ ∈ x̂, ∃x̂C ∈ x̂C : (x̂C , x̂, ûC , û) ∈ R̂C },

(9)

0

R(ε) = {(x̂, x̃, û, ǔ) | ∃u ∈ U, ∃ε1 ≥ κ, ∃ε2 ≥ κ , ∀x̌ ∈ x̃, ∃x ∈ X, ∃x̂ ∈ x̂ :
ε1 + ε2 = ε ∧ (x̂, x, û, u) ∈ R(ε1 ) ∧ (x, x̌, u, ǔ) ∈ Ř(ε2 )}.

(10)

Theorem 4 Consider the same condition as Theorem 3. Let S̄C := SC ×RC (ε) S̃ = (X̄C , X̄C0 , ŪC , r̄C ). The
following relation R̄C (ε) ⊆ ((X̂C × X̂)× X̃)×X ×((ÛC × Û)× Ũ)×U is a (κ +κ 0 , max{β , β 0 }, max{λ , λ 0
})-acASR from S̄C to (S,Y, H) with d̄C (((ûC , û), ǔ), u) = d̄(û, ǔ):
R̄C (ε) = {(((x̂C , x̂), x̃), x, ((ûC , û), ǔ), u) | ∃ε1 ≥ κ, ∃ε2 ≥ κ 0 , ∃x̂ ∈ x̂ :
ε1 + ε2 = ε ∧ (x̂, x, û, u) ∈ R(ε1 ) ∧ (x, x̃, u, ǔ) ∈ R0 (ε2 )}, (11)
where R0 (ε) is defined by (3).
The definition of RC (ε) corresponds to that of RC (ε) given by (1). Then, Theorem 4 is an extension
of Theorem 1 to the output feedback control of the physical plant. The block diagram of the proposed
control system is shown in Fig. 1. When the observer S̃ receives the output y, it updates the estimtion x̃
of the current state of the plant. Then, SC updates the state (x̂C , x̂) by the relation RC (ε). The controller
determines a control input ûC ∈ ÛC (x̂C ) such that for any x̂C ∈ x̂C , r̂C (x̂C , ûC ) 6= 0/ holds. This is the
key idea of our approach. Then, by Theorem 4, the physical plant controlled by the output feedback
controller S̄C exhibits a desired behavior approximately in the sense of the acASR.

44

Output Feedback Controller Design with Symbolic Observers for Cyber-physical Systems

In the case where Ŝ and Š are constructed by discretization of the state set X of the plant, we can
define the parameterized relations based on the Euclidean distance on X that measures the abstraction
error as shown in the illustrative example.
In the next section, we show the proofs of these theorems.

5

Proofs of Main Theorems

First, we show two lemmas that are needed in the proofs of the main theorems.
Lemma 1 The relation R̂C ⊆ X̂C × X̂ × ÛC × Û defined by (9) is an ASR from ŜC to Ŝ.
Proof We will show that R̂C satisfies the conditions of an ASR from ŜC to Ŝ.
1. Consider any x̂C0 ∈ X̂C0 . We consider the following state x̂0 of Ŝ:
x̂0 = {x̂0 ∈ X̂0 | ∃x̂C0 ∈ x̂C0 : (x̂C0 , x̂0 ) ∈ R̂CX }.
Since R̂C is an ASR, x̂0 is a non-empty set. Recall that X̂0 = 2X̂0 \ {0},
/ and we have x̂0 ∈ X̂0 . By
the definition of R̂C , (x̂C0 , x̂0 ) ∈ R̂CX holds.
2. First, consider any (x̂C , x̂) ∈ R̂CX . Choose any ûC ∈ ÛC (x̂C ). From (4), there exists û ∈ Û(x̂) such
that (x̂C , x̂, ûC , û) ∈ R̂C . By the definition of R̂C , the following condition holds:
∀x̂ ∈ x̂, ∃x̂C ∈ x̂C : (x̂C , x̂, ûC , û) ∈ R̂C ,
which implies together with the definition of the ASR that
∀x̂0 ∈

[

r̂(x̂, û), ∃x̂C0 ∈

[

r̂C (x̂C , ûC ) : (x̂C0 , x̂0 ) ∈ R̂CX .

(12)

x̂C ∈x̂C

x̂∈x̂

Next, consider any x̂0 ∈ r̂(x̂, û). By the definition of r̂, we have
x̂0 ⊆

[

r̂(x̂, û).

x̂∈x̂

By the definition of r̂C , we have
S

r̂C (x̂C , ûC ) = 2

x̂C ∈x̂C r̂C (x̂C ,ûC )

\ {0}.
/

Thus, from (12), there always exists x̂0C ∈ r̂C (x̂C , ûC ) satisfying the following condition:
∀x̂0 ∈ x̂0 , ∃x̂C0 ∈ x̂0C : (x̂C0 , x̂0 ) ∈ R̂CX .
Therefore, by the definition of R̂C , (x̂0C , x̂0 ) ∈ R̂CX holds.



Lemma 1 shows that ŜC is a feedback controller of Ŝ.
Lemma 2 The relation R(ε) ⊆ X̂ × X̃ × Û × Ũ defined by (10) is a (κ + κ 0 , max{β , β 0 }, max{λ , λ 0 })acASR from Ŝ to S̃ with d̄.

Masashi Mizoguchi & Toshimitsu Ushio

45

Proof We will show that R(ε) satisfies the conditions of a (κ + κ 0 , max{β , β 0 }, max{λ , λ 0 })-acASR
from Ŝ to S̃ with d̄.
1. Consider any x̂0 ∈ X̂0 . We consider the following state x̃0 of S̃:
x̃0 = {x̌0 ∈ X̌0 | ∃x̂0 ∈ x̂0 , ∃x0 ∈ X0 : (x̂0 , x0 ) ∈ RX (κ) ∧ (x0 , x̌0 ) ∈ ŘX (κ 0 )}.
Since R(ε) and Ř(ε) are a (κ, β , λ )-acASR from Ŝ to S and a (κ 0 , β 0 , λ 0 )-acSR from S to Š, respec/ and we have x̃0 ∈ X̃0 . By the definition of
tively, x̃0 is a non-empty set. Recall that X̃0 = 2X̌0 \ {0},
R(ε), (x̂0 , x̃0 ) ∈ RX (κ + κ 0 ) holds.
2. First, consider any (x̂, x̃) ∈ RX (ε). Choose any û ∈ Û(x̂). From (6) and (7), there exist u ∈ U and
ǔ ∈ Ũ(x̃) such that (x̂, x̃, û, ǔ) ∈ R(ε). By the definition of R(ε), there exist ε1 ≥ κ and ε2 ≥ κ 0
such that ε1 + ε2 = ε, and the following condition holds:
∀x̌ ∈ x̃, ∃x ∈ X, ∃x̂ ∈ x̂ : (x̂, x, û, u) ∈ R(ε1 ) ∧ (x, x̌, u, ǔ) ∈ Ř(ε2 ),
which implies together with the definition of r̃ that
∀x̌0 ∈

[

ř(x̌, u), ∃x0 ∈

x̌∈x̃

r(x, u) : (x0 , x̌0 ) ∈ ŘX (κ 0 + β 0 ε2 + λ 0 ď(u, ǔ)).

[
x̌∈x̃,(x̌,x)∈ŘX (ε2 )

By the definition of (κ, β , λ )-acASR from Ŝ to S with d, we have the following condition:
∀x0 ∈

r(x, u), ∃x̂0 ∈

[

[

r̂(x̂, û) : (x̂0 , x0 ) ∈ RX (κ + β ε1 + λ d(û, u)).

x̂∈x̂

x̌∈x̃,(x̌,x)∈ŘX (ε2 )

Thus, we have the following condition:
∀x̌0 ∈

[
x̌∈x̃

ř(x̌, ǔ), ∃x0 ∈

r(x, u), ∃x̂0 ∈

[

[

r̂(x̂, û) :

x̂∈x̂

x̌∈x̃,(x̌,x)∈ŘX (ε2 )

(x̂0 , x0 ) ∈ RX (κ + β ε1 + λ d(û, u)) ∧ (x0 , x̌0 ) ∈ ŘX (κ 0 + β 0 ε2 + λ 0 ď(u, ǔ)).

(13)

Next, consider any x̃0 ∈ r̃(x̃, ǔ). By the definition of r̃, we have
x̃0 ⊆

[

ř(x̌, ǔ).

x̌∈x̃

By the definition of r̂, we have
r̂(x̂, û) = 2

S

x̂∈x̂ r̂(x̂,û)

\ {0},
/

which implies together with (13) that there always exists x̂0 ∈ r̂(x̂, û) satisfying the following condition:
∀x̌0 ∈ x̃0 , ∃x0 ∈ X, ∃x̂0 ∈ x̂0 : (x̂0 , x0 ) ∈ RX (κ + β ε1 + λ d(û, u)) ∧ (x0 , x̌0 ) ∈ ŘX (κ 0 + β 0 ε2 + λ 0 ď(u, ǔ)).
Thus, by the definition of R(ε) and (5), we have
(x̂0 , x̃0 ) ∈ R(κ + κ 0 + β ε1 + β 0 ε2 + λ d(û, u) + λ 0 ď(u, ǔ))
⊆ R(κ + κ 0 + max{β , β 0 }ε + max{λ , λ 0 }d̄(û, ǔ)).


46

Output Feedback Controller Design with Symbolic Observers for Cyber-physical Systems

By Lemmas 1 and 2, R̂C and R(ε) are an ASR from ŜC to Ŝ and a (κ + κ 0 , max{β , β 0 }, max{λ , λ 0 })acASR from Ŝ to S̃ with d̄, respectively, which implies together with Theorem 1 that Theorem 3 holds.
Next, we prove Theorem 4. We will show that R̄C (ε) satisfies the conditions of a (κ +κ 0 , max{β , β 0 },
max{λ , λ 0 })-acASR from S̄C to (S,Y, H) with d̄C .
1. Consider any ((x̂C0 , x̂0 ), x̃0 ) ∈ X̄C0 . By the definition of the composed systems, we have (x̂C0 , x̂0 ) ∈
R̂CX and (x̂0 , x̃0 ) ∈ RX (κ + κ 0 ). By the proof (1) of Lemma 2, there exists x0 ∈ X0 such that
∃x̂0 ∈ x̂0 ,∃x̌0 ∈ x̃0 : (x̂0 , x0 ) ∈ RX (κ) ∧ (x0 , x̌0 ) ∈ ŘX (κ 0 ),
which implies together with the definition of R0 (ε) that we have (((x̂C0 , x̂0 ), x̃0 ), x0 ) ∈ R̄CX (κ +
κ 0 )).
2. First, consider any (((x̂C , x̂), x̃), x) ∈ R̄CX (ε). Choose any ((ûC , û), ǔ) ∈ ŪC (((x̂C , x̂), x̃)). By the
definition of the composed systems, we have (x̂C , x̂, ûC , û) ∈ R̂C and (x̂, x̃0 , û, ǔ) ∈ R(ε). By the
definition of R(ε), there exists u ∈ U(x) such that
∃ε1 ≥ κ, ∃ε2 ≥ κ 0 , ∃x̌ ∈ x̃, ∃x̂ ∈ x̂ : ε1 + ε2 = ε ∧ (x̂, x, û, u) ∈ R(ε1 ) ∧ (x, x̌, u, ǔ) ∈ Ř(ε2 ),
which implies together with the definition of R0 (ε) that we have (((x̂C , x̂), x̃), x, ((ûC , û), ǔ), u) ∈
R̄C (ε).
Next, consider any x0 ∈ r(x, u). Since R(ε) is a (κ, β , λ )-acASR from Ŝ to S with d, there exists
x̂0 ∈ r̂(x̂, û) such that (x̂0 , x0 ) ∈ RX (κ + β ε1 + λ d(û, u)). Moreover, since R0 (ε) is a (κ 0 , β 0 , λ 0 )-acSR
from S to S̃ with ď, there exists x̃0 ∈ r̃(x̃, ǔ) such that
∃x̌0 ∈ x̃0 : (x0 , x̌0 ) ∈ ŘX (κ 0 + β 0 ε2 + λ 0 ď(u, ǔ)).

(14)

Since R(ε) is a (κ + κ 0 , max{β , β 0 }, max{λ , λ 0 })-acASR from Ŝ to S̃ with d̄, there exists x̂0 ∈
r̂(x̂, û) such that
x̂0 ∈ x̂0 ∧ (x̂0 , x̃0 ) ∈ RX (κ + κ 0 + max{β , β 0 }ε + max{λ , λ 0 }d̄(û, ǔ)).
Thus, we have
∃x̂0 ∈ x̂0 : (x̂0 , x0 ) ∈ RX (κ + β ε1 + λ d(û, u)).
By the ASR R̂C , we have
∃x̂0C ∈ r̂C (x̂C , ûC ) : (x̂0C , x̂0 ) ∈ R̂CX .
By the definition of the composed systems, we have
((x̂0C , x̂0 ), x̃0 ) ∈ r̄C (((x̂C , x̂), x̃), ((ûC , û), ǔ)).
On the other hand, by the definition of d̄C and (5), we have
d̄C (((ûC , û), ǔ), u) = d̄(û, ǔ) ≥ d(û, u) + ď(u, ǔ).
Therefore, by (14) and (15), we have
(((x̂0C , x̂0 ), x̃0 ), x0 ) ∈ R̄CX (κ + κ 0 + max{β , β 0 }ε + max{λ , λ 0 }d̄C (((ûC , û), ǔ), u)).

(15)

Masashi Mizoguchi & Toshimitsu Ushio

6

47

Illustrative Example

6.1

Physical Plant

We consider a physical plant given by
 

 

 
ξ1 [k + 1]
0.5
0
ξ1 [k]
3.6056


=
+
u[k],


0 0.25
ξ2 [k]
3.9051
 ξ2 [k + 1]


 ξ1 [k]
yc [k] = 2.7042 2.2535
,


ξ2 [k]



y[k] = rdZ (yc [k]) ,

(16)

where yc [k] is the output of the plant, and y[k] is the measured value of the sensor. rdZ (y) is a rounded
value of y to an integer. We will design a symbolic controller determining the control input u[k]. Data
transmission between the plant and the controller is done via unreliable communication channels where
data dropouts sometimes occur. If data dropouts occur, the control signal u (resp. the output signal y)
is set to be 0 at the plant (resp. at the controller). Assume that data dropouts never occur consecutively.
The dynamics of communication channels is modeled by a system shown in Fig. 2. First, we introduce
a system with outputs (S,Y, H) = (X, X0 ,U, r,Y, H) that represents the dynamics of the plant and the
dynamics of the communication channels, where X = R2 × {0, 1} × {0, 1}, X0 = {[0 0 0 0]T }, U =
{0.032, 0.064}, and Y = Z. H : X → Y is defined as follows:
(
rdZ {2.7042ξ1 [k] + 2.2535ξ2 [k]} if ξ4 [k] = 0,
H([ ξ1 [k] ξ2 [k] ξ3 [k] ξ4 [k]]T ) =
0
if ξ4 [k] = 1.
Note that ξ3 [k] (resp. ξ4 [k]) is a state of communication channels from the controller to the physical plant
(resp. vice versa), and their Boolean values correspond to the state number of Fig. 2. The transition map
r : X ×U → 2X is defined as follows:
n
T 
T 
T 
T o
r([ ξ1 ξ2 0 0]T , u) =
ξ10 ξ20 0 0 , ξ10 ξ20 0 1 , ξ100 ξ200 1 0 , ξ100 ξ200 1 1
,
n
o
T 
T
r([ ξ1 ξ2 0 1]T , u) =
ξ10 ξ20 0 0 , ξ100 ξ200 1 0
,
n
o
n
T 
T
T o
r([ ξ1 ξ2 1 0 ]T , u) =
ξ10 ξ20 0 0 , ξ10 ξ20 0 1
, r([ ξ1 ξ2 1 1]T , u) =
ξ10 ξ20 0 0
,
where


ξ10
ξ20




=

0.5
0
0 0.25



ξ1
ξ2




+

3.6056
3.9051




u,

ξ100
ξ200




=

0.5
0
0 0.25

Figure 2: The dynamics of the communication channel.



ξ1
ξ2


.

(17)

48

Output Feedback Controller Design with Symbolic Observers for Cyber-physical Systems

Second, let [A]η := {x ∈ A | ∃k ∈ Zn : x = 2kη} for a set A ⊆ Rn . Then, we introduce a c-abstracted system
Ŝ = (X̂, X̂0 , Û, r̂) where X̂ = [[0, 0.4]2 ]0.005 × {0, 1} × {0, 1}, X̂0 = {[0 0 0 0]T }, and Û = {0.032, 0.064}.
The transition map r̂ : X̂ × Û → 2X̂ is defined as follows:
h
h
iT
iT h
iT h
iT h
iT 
0 ˆ0
0 ˆ0
00 ˆ 00
00 ˆ 00
ˆ
ˆ
ˆ
ˆ
ˆ
ˆ
r̂( ξ1 ξ2 0 0 , û) =
ξ1 ξ2 0 0 , ξ1 ξ2 0 1 , ξ1 ξ2 1 0 , ξ1 ξ2 1 1
,
h
h
iT
iT h
iT 
0 ˆ0
00 ˆ 00
ˆ
ˆ
ˆ
ˆ
r̂( ξ1 ξ2 0 1 , û) =
ξ1 ξ2 0 0 , ξ1 ξ2 1 0
,

h

h
h
iT
iT h
iT
h
iT
iT 
0 ˆ0
0 ˆ0
0 ˆ0
ˆ
ˆ
ˆ
ˆ
ˆ
ˆ
ˆ
ξ1 ξ2 0 0 , ξ1 ξ2 0 1
ξ1 ξ2 0 0
r̂( ξ1 ξ2 1 0 , û) =
, r̂( ξ1 ξ2 1 1 , û) =
,
where
"
#
ξˆ10
= rd2
ξˆ20



0.5
0
0 0.25

 ! " ˆ 00 #

"
" ˆ # 
3.6056
0.5
0
ξ1
ξ1
+
û ,
= rd2
3.9051
0 0.25
ξˆ2
ξˆ200

ξˆ1
ξˆ2

#!
.
(18)

Note that rd2 (y) rounds y off to two decimal place. Then, the following relation R(ε) ⊆ X̂ × X × Û ×U
is a (0.005, 0.5, 0)-acASR from Ŝ to S:
 

 




ξˆ1
ξ


1
"
#




  ˆ  


ˆ

ξ1
ξ1
 ξ2   ξ2 

ˆ
ˆ
R(ε) =  ˆ  , 
,
û,
u
û
=
u
∧
−
≤
ε
∧
ξ
=
ξ
∧
ξ
=
ξ
. (19)

3
3
4
4
ξ3 
ξ2


 ξ3 

ξˆ2






ξ4
ξˆ4
The desired behavioris that yc [k] converges to 1. Then, we introduce ŜC = (X̂C , X̂C0 , ÛC , r̂C ) as shown
in Fig. 3 where X̂C0 = [0 0 0 0]T and ÛC = {0.032, 0.064}. The red arrows in Fig. 3 describe the
transitions when ûC = 0.064, and the black arrows describe the transitions when ûC = 0.032.
Then, the following relation R̂C ⊆ X̂C × X̂ × ÛC , Û is an ASR from ŜC to Ŝ:
R̂C = {(x̂C , x̂, ûC , û) | x̂C = x̂ ∧ ûC = û}.

(20)

Third, we introduce an o-abstracted system Š = (X̌, X̌0 , Ǔ, ř) where X̌ = [[0, 0.4]2 ]0.05 × {0, 1} × {0, 1},
X̌0 = {[0 0 0 0]T }, and Ǔ = {0.032, 0.064}. The transition map ř : X̌ × Ǔ → 2X̌ is defined as follows:
h
h
iT
iT h
iT h
iT h
iT 
0 ˇ0
0 ˇ0
00 ˇ 00
00 ˇ 00
ˇ
ˇ
ˇ
ˇ
ˇ
ˇ
ř( ξ1 ξ2 0 0 , ǔ) =
ξ1 ξ2 0 0 , ξ1 ξ2 0 1 , ξ1 ξ2 1 0 , ξ1 ξ2 1 1
,


h
iT
h
iT h
iT
ř( ξˇ1 ξˇ2 0 1 , ǔ) =
ξˇ10 ξˇ20 0 0 , ξˇ100 ξˇ200 1 0
,
h
h
h
iT
iT h
iT 
h
iT
iT 
0 ˇ0
0 ˇ0
0 ˇ0
ˇ
ˇ
ˇ
ˇ
ˇ
ˇ
ˇ
ř( ξ1 ξ2 1 0 , ǔ) =
ξ1 ξ2 0 0 , ξ1 ξ2 0 1
, ř( ξ1 ξ2 1 1 , ǔ) =
ξ1 ξ2 0 0
,
where
"
#
ξˇ10
= rd1
ξˇ20



0.5
0
0 0.25

" ˇ # 
 ! " ˇ 00 #

"
ξ1
3.6056
ξ1
0.5
0
+
ǔ ,
= rd1
0 0.25
3.9051
ξˇ2
ξˇ200

ξˇ1
ξˇ2

#!
.
(21)

Masashi Mizoguchi & Toshimitsu Ushio

Figure 3: The behavior of ŜC .

49

Figure 4: The occurrences of data dropouts.

Note that rd1 (y) rounds y off to one decimal place.
Then, the following relation Ř(ε) ⊆ X × X̌ ×U × Ǔ is a (0.05, 0.5, 0)-acSR from S to Š:
 



 

Ř(ε) = 






6.2



  ˇ 

ξ1
ξ1

"
#




 ˇ 

ˇ
ξ2 
ξ
ξ
ξ

2 
1
1
ˇ
ˇ
,
,
u,
ǔ
u
=
ǔ
∧
−
≤
ε
∧
ξ
=
ξ
∧
ξ
=
ξ



3
3
4
4 . (22)
ξ3   ξˇ3 
ξ2


ξˇ2



ˇ
ξ4
ξ4

Output Feedback Control

We construct an observer S̃ = (X̃, X̃0 , Ũ, r̃) induced by Š as shown in Definition 5. Consider the ASR
R̂C , (0.005, 0.5, 0)-acASR R(ε), and (0.05, 0.5, 0)-acSR Ř(ε) defined in the previous subsection. Then,
it is shown that R̂C satisfies (4), that R(ε) satisfies (6), and that Ř(ε) satisfies (7). Note that U = Û =
Ǔ. We introduce Ŝ = (X̂, X̂0 , Û, r̂) induced by Ŝ and ŜC = (X̂C , X̂C0 , ÛC , r̂C ) induced by ŜC defined in
Definitions 6 and 7, respectively. Now, we use Theorems 3 and 4 to design the output feedback controller
S̄C , where R̄C (ε) is a (0.055, 0.5, 0)-acASR from S̄C to S.

6.3

Simulation Result

By the computer simulation, it is shown that the observer S̃ has 10 states, and that the output feedback
controller S̄C has 27 states. The occurrences of data dropouts are shown in Fig. 4. The time response
of yc [k] is shown in Fig. 5. It is shown that yc [k] converges to 1 though sometimes deviates by the input
disturbances. The numbers of candidates of the current state are shown in Fig. 6. Since we have X̌ ⊆ X̂,
it is noticed that the number of candidates listed up by the controller is always larger than that by the
observer.

50

Output Feedback Controller Design with Symbolic Observers for Cyber-physical Systems

Figure 5: The time response of yc [k].

7

Figure 6: The numbers of candidates of the current
state.

Conclusion

We consider a symbolic design of an observer that lists up all possible candidates of the current state
of the physical plant. In order to design a symbolic output feedback controller, two abstracted systems
are introduced. One abstracted system needs an acASR to construct a feedback controller. The other
needs an acSR to estimate the state of the plant. They are given independently, which means that the
separation principle of the control and the observation holds. We proved that there exists an acASR from
the proposed output feedback controller to the physical plant without introducing the distance.
It is shown in [18, 19, 20, 23] that the input-output dynamical stability is preserved under an acASR.
Thus, it is future work to show the stability of the controlled plant.

Acknowledgment
This work was supported by JSPS KAKENHI No. 15K14007.

References
[1] R. Alur, T.A. Henzinger, O. Kupferman & M.Y. Vardi (1998): Alternating refinement relations. In: Proc.
of the 9th International Conference on Concurrency Theory, volume 1466 of LNCS, Springer, pp. 163–178,
doi:10.1007/BFb0055622.
[2] R. Alur, T.A. Henzinger, G. Lafferriere & G.J. Pappas (2000): Discrete abstractions of hybrid systems. In:
Proc. of the IEEE, 88, IEEE, pp. 971–984, doi:10.1109/5.871304.
[3] R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger & B. Jobstmann (2010): Robustness in the presence
of liveness. In: Proc. of the 22nd International Conference on Computer Aided Verification, Springer, pp.
410–424, doi:10.1007/978-3-642-14295-6 36.
[4] R. Bloem, K. Greimel, T.A. Henzinger & B. Jobstmann (2009): Synthesizing robust systems. In: Proc. of the Formal Methods in Computer-Aided Design 2009, FMCAD, pp. 85–92,
doi:10.1109/FMCAD.2009.5351139.
[5] C.G. Cassandras & S. Lafortune (2009): Introduction to Discrete Event Systems, 2nd edition. Springer.
[6] K. Chatterjee, L. Doyen, T.A. Henzinger & J.F. Raskin (2007): Algorithms for omega-regular games with imperfect information. Logical Methods in Computer Science 3(4), pp. 1–23, doi:10.2168/LMCS-3(3:4)2007.

Masashi Mizoguchi & Toshimitsu Ushio

51

[7] R. Ehlers & U. Topcu (2015): Estimator-based reactive synthesis under incomplete information. In: Proc.
of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, pp. 249–258,
doi:10.1145/2728606.2728626.
[8] D. Fan & D.C. Tarraf (2014): On finite memory observability of a class of systems over finite alphabets with
linear dynamics. In: Proc. of the IEEE 53rd Annual Conference on Decision and Control, pp. 3884–3891,
doi:10.1109/CDC.2014.7039992.
[9] R. Ghaemi & D.D. Vecchio (2014): Control for safety specifications of systems with imperfect
information on a partial order.
IEEE Transactions on Automatic Control 59(4), pp. 982–995,
doi:10.1109/TAC.2014.2301563.
[10] A. Girard & G.J. Pappas (2007): Approximation metrics for discrete and continuous systems. IEEE Transactions on Automatic Control 52(5), pp. 782–798, doi:10.1109/TAC.2007.895849.
[11] A. Girard & G.J. Pappas (2011): Approximate bisimulation: A bridge between computer science and control
theory. European Journal of Control 17(5-6), pp. 568 – 578, doi:10.3166/ejc.17.568-578.
[12] A. Girard, G. Pola & P. Tabuada (2010): Approximately bisimilar symbolic models for incrementally stable switched systems.
IEEE Transactions on Automatic Control 55(1), pp. 116–126,
doi:10.1109/TAC.2009.2034922.
[13] R. Goebel, R.G. Sanfelice & A.R. Teel (2012): Hybrid Dynamical Systems: Modeling, Stability, and Robustness. Princeton University Press.
[14] R. Milner (1989): Communication and Concurrency. Prentice-Hall.
[15] M. Mizoguchi & T. Ushio (2015): Observer-based similarity output feedback control of cyber-physical systems. IFAC-PapersOnLine 48(27), pp. 248–253, doi:10.1016/j.ifacol.2015.11.183.
[16] G. Pola, A. Girard & P. Tabuada (2008): Approximately bisimilar symbolic models for nonlinear control
systems. Automatica 44(10), pp. 2508 – 2516, doi:10.1016/j.automatica.2008.02.021.
[17] G. Pola & P. Tabuada (2009): Symbolic models for nonlinear control systems: Alternating approximate
bisimulations. SIAM Journal on Control and Optimization 48(2), pp. 719–733, doi:10.1137/070698580.
[18] M. Rungger & P. Tabuada (2013): A symbolic approach to the design of robust cyber-physical systems. In: Proc. of the IEEE 52nd Annual Conference on Decision and Control, pp. 3932–3937,
doi:10.1109/CDC.2013.6760490.
[19] M. Rungger & P. Tabuada (2014): Abstracting and refining robustness for cyber-physical systems. In: Proc.
of the 17th International Conference on Hybrid Systems: Computation and Control, ACM, pp. 223–232,
doi:10.1145/2562059.2562133.
[20] M. Rungger & P. Tabuada (2015): A Notion of robustness for cyber-physical systems. IEEE Transactions on
Automatic Control, doi:10.1109/TAC.2015.2492438. To appear.
[21] P. Tabuada (2008): An approximate simulation approach to symbolic control. IEEE Transactions on Automatic Control 53(6), pp. 1406–1418, doi:10.1109/TAC.2008.925824.
[22] P. Tabuada (2009): Verification and Control of Hybrid Systems: A Symbolic Approach.
doi:10.1007/978-1-4419-0224-5.

Springer,

[23] P. Tabuada, S.Y. Caliskan, M. Rungger & R. Majumdar (2014): Towards robustness for cyber-physical systems. IEEE Transactions on Automatic Control 59(12), pp. 3151–3163, doi:10.1109/TAC.2014.2351632.
[24] D.C. Tarraf (2012): A control-oriented notion of finite state approximation. IEEE Transactions on Automatic
Control 57(12), pp. 3197–3202, doi:10.1109/TAC.2012.2199180.
[25] D.C. Tarraf (2014): An input-output construction of finite state ρ/µ approximations for control design. IEEE
Transactions on Automatic Control 59(12), pp. 3164–3177, doi:10.1109/TAC.2014.2351631.
[26] N. Tung Vu & S. Takai (2016): Synthesis of output feedback controllers for bisimilarity control of transition
systems. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences E99A(2), pp. 483–490, doi:10.1587/transfun.E99.A.483.

