# Approximate Equivalence of the Hybrid Automata with Taylor Theory

Authors: Anping He; Jinzhao Wu; Shihan Yang; Hongyan Tan
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

Hybrid automaton is a formal model for precisely describing a hybrid
system in which the computational processes interact with the physical
ones. The reachability analysis of the polynomial hybrid automaton is
decidable, which makes theTaylor approximation of a hybrid automaton
applicable and valuable. In this paper, we studied the simulation relation
among the hybrid automaton and its Taylor approximation, as well as
the approximate equivalence relation. We also proved that the Taylor approximation simulates its original hybrid automaton, and similar hybrid
automata could be compared quantitatively, for example, the approximate equivalence we proposed in the paper.


---

## Body

## 1. Introduction

Hybrid automaton is a formal model of a hybrid system in which computational processes interact with the physical ones. Similar to other automata, the hybrid one also contains states and transitions, but it labels and groups all closely related states as an activity to express continuous behaviour by astate function; moreover, it also employs functions to update variable values while transiting from an activity to another. In short, a hybrid automaton shows the hybrid behaviour composed of the discrete state transitions and continuous state evolution.Most hybrid systems are safety critical applications, which require guarantees of safe operations; the unwarrantable configurations must be unreached. Formally, we can validate these safety properties byreachability analysis, for example, the forward or backward iteration with initial conditions, activities, and so on. However, for most types of hybrid automata, the computation of the iteration may not halt and then leads to an undecidable reachability analysis. Luckily, there exists one type of hybrid automaton called the polynomial hybrid automaton; its reachability analysis is proved decidable. Then it is very valuable to construct an approximate polynomial hybrid automaton of a common one. In [1], the authors build the polynomial one in terms of Taylor theory.In this paper, we study the relation of the hybrid automaton and its Taylor approximation in terms of the semantic models, for example, how different similar automata behave, and then the quantitative comparison of the automata. We find that the automaton and its approximation show a simulation relation; furthermore, fortunately, we propose a quantitative equivalence of similar hybrid automata in terms of simulation. To our knowledge, there seems no work done for this.


### 1.1. Related Works

The hybrid automaton was introduced in [2, 3] with analysis for the linear and nonlinear one and some simple examples, and, in [4], the authors focus on its verification aspect. There are many works on verification and analysis of hybrid automata; [2, 4–6] studied the model checking of hybrid automata; [2, 3, 7] performed reachability analysis; [8, 9] showed some achievements of probabilistic hybrid automata; [10] studied the hybrid automata by a domain-theoretic semantics.The behavior of hybrid system is so complex that the approximation of the system is necessary in most of applications. In [2], authors found the reachability of the multirated simple hybrid automata is decidable. Several papers (see, e.g., [1, 2, 7, 11, 12]) tried to classify hybrid automata, for example, a specific type of automaton satisfies the properties if its approximation holds the same ones. Other papers (see, e.g., [13–15]) were concerned with the way of analyzing classes of hybrid systems for which the strategy previously described does not work.In [1], the authors approximated syntactically an automaton H with Approx
(
H
,
k
) in terms of Taylor theory and then studied also how close the behaviors of H and Approx
(
H
,
k
) are. However, they missed the relation between H and Approx
(
H
,
k
) in a behaviour view, nevertheless, the quantitative equivalence based on the relation was not considered either.


### 1.2. Organization of the Paper

The paper is organized as follows: in Section2 we recall the definition of hybrid automata and their Taylor approximations; in Section 3 we study the simulation and approximation and then prove a hybrid automaton being simulated by its Taylor approximation; in Section 4 we propose a Taylor k-relation and then prove this relation is an equivalence; we concluded in Section 5.


## 1.1. Related Works

The hybrid automaton was introduced in [2, 3] with analysis for the linear and nonlinear one and some simple examples, and, in [4], the authors focus on its verification aspect. There are many works on verification and analysis of hybrid automata; [2, 4–6] studied the model checking of hybrid automata; [2, 3, 7] performed reachability analysis; [8, 9] showed some achievements of probabilistic hybrid automata; [10] studied the hybrid automata by a domain-theoretic semantics.The behavior of hybrid system is so complex that the approximation of the system is necessary in most of applications. In [2], authors found the reachability of the multirated simple hybrid automata is decidable. Several papers (see, e.g., [1, 2, 7, 11, 12]) tried to classify hybrid automata, for example, a specific type of automaton satisfies the properties if its approximation holds the same ones. Other papers (see, e.g., [13–15]) were concerned with the way of analyzing classes of hybrid systems for which the strategy previously described does not work.In [1], the authors approximated syntactically an automaton H with Approx
(
H
,
k
) in terms of Taylor theory and then studied also how close the behaviors of H and Approx
(
H
,
k
) are. However, they missed the relation between H and Approx
(
H
,
k
) in a behaviour view, nevertheless, the quantitative equivalence based on the relation was not considered either.


## 1.2. Organization of the Paper

The paper is organized as follows: in Section2 we recall the definition of hybrid automata and their Taylor approximations; in Section 3 we study the simulation and approximation and then prove a hybrid automaton being simulated by its Taylor approximation; in Section 4 we propose a Taylor k-relation and then prove this relation is an equivalence; we concluded in Section 5.


## 2. Taylor Approximation of Hybrid System

Let us show the formal definition of a hybrid automaton.Definition 1.
A hybrid automatonH is a tuple (
x
→
,
ϕ
init
,
Q
,
q
0
,
Σ
,
T
,
Act
,
Event
). (i)
x
→
=
(
x
1
,
…
,
x
n
) is vector of real variables.
(ii)
ϕ
init
∈
Φ
(
(
x
1
,
…
,
x
n
)
) is initial condition.
(iii)
Q is finite set of states.
(iv)
q
0
∈
Q is the initial state.
(v)
Σ is a set of events symbol.
(vi)
ActQ
→
Φ
(
(
x
1
,
…
,
t
,
x
1
′
,
…
,
x
n
′
)
) is the activity function assigning to each state q a formula Act
(
q
). The variable t represents time elapsing.
(vii)
T
⊂
Q
×
Φ
(
(
x
1
,
…
,
x
n
,
t
,
x
1
′
,
…
,
x
n
′
)
)
×
Q is a set of transitions. Variables x
1
′
,
…
,
x
n
′ represent the new values taken by the variables x
1
,
…
,
x
n after the transition: T
=
T
f
∪
T
j:
(a)
T
f
⊂
q
×
Act
(
q
)
×
q, that q
∈
Q,
(b)
T
j
⊂
Q
×
Φ
(
(
x
1
,
…
,
x
n
,
0
,
x
1
′
,
…
,
x
n
′
)
)
×
Q.
(viii)
EventT
→
Σ is event mapping function attaching each transition an event name.There are many similar definitions of hybrid automata, such as ones in [2, 3]. Generally, the hybrid automata behave in two ways, namely, an internalflow and statejump transition. The flow is a stutter at states which shows the continuous behavior of a hybrid automaton, for example, a variation that does not involve states switching but updates value of variables only. In contrast, jump transition always switches states. Let q
,
q
′
∈
Q, α
∈
Σ, and t
∈
R be time elapsing. We denote the flow as below:
(1)
q
⟶
t
q
and jump
(2)
q
⟶
α
q
′
.The basic way of analyzing a hybrid automaton isreachability analysis, which involves computing the forward or backward reachable regions of a hybrid automaton from initial conditions recursively [1, 2]. However, in most cases, the computing failed because of the nondecidability of the reachabilty analysis.There are many aspects that can be adopted to classify the hybrid automata; one of them concerns the mathematical expressions; for example, a hybrid automaton is apolynomial hybrid automaton if and only if ϕ
init is a polynomial formula; for each state q, Act
(
q
) is a polynomial formula, and for each transition (
q
,
ϕ
,
q
′
), ϕ is a polynomial formula. Researchers and engineers try their best to find the polynomial hybrid automaton, or even an approximated one, of a real system, because the problem of reachability in n steps for polynomial hybrid automata is decidable [16, 17].It is clear that the most types of hybrid automata do not belong to the polynomial ones; then it is valuable to study a polynomial approximation of a hybrid automaton. Ruggero Lanotte and Simone Tini proposed polynomial approximation of a generic hybrid automaton in [1] in terms of Taylor approximation theory. The following is the definition of Taylor approximation of a hybrid automaton H.Definition 2.
LetH be a hybrid automaton; all functions appearing in its formulae Φ are derivable k
+
1 times. The approximation of rank k for H
=
(
x
→
,
ϕ
init
,
Q
,
q
0
,
Σ
,
T
,
Act
,
Event
) is the polynomial hybrid automaton Approx
(
H
,
k
)
=
(
x
→
,
ϕ
init
k
,
Q
′
,
q
0
′
,
Σ
,
T
k
,
Act
k
,
Event
′
). (i)
Each formula inϕ
init
k, T
k, and Act
k is derived from ϕ by replacing each nonpolynomial subformula f
(
y
→
)
~
c in ϕ with
(3)
p
k
(
f
,
y
→
)
-
R
k
(
f
,
y
→
,
ϕ
)
~
c
,
if
R
k
(
f
,
y
→
,
ϕ
)
≠
∞
;
true
,
if
R
k
(
f
,
y
→
,
ϕ
)
=
∞
,
where y
→ stays for either x
→, if ϕ is ϕ
init, or (
x
→
,
x
→
′
), if ϕ is a transition label, or (
x
→
,
t
,
x
→
′
), if ϕ is an activity function.
(ii)
Q
′ is constructed by one-to-one mapping M, which maps Q to Q
′, q
0
′
=
M
(
q
0
).
(iii)
T
k
=
{
(
q
1
k
,
ϕ
k
,
q
2
k
)
∣
q
1
k
=
M
(
q
1
)
∧
q
2
k
=
M
(
q
2
)
∧
(
q
1
,
ϕ
,
q
2
)
∈
T
}.
(iv)
Act
k
=
{
(
q
k
,
ϕ
k
)
∣
q
k
=
M
(
q
)
∧
(
q
,
ϕ
)
∈
Act
}.
(v)
Event
′
=
{
(
t
k
,
α
)
} that (
t
,
α
)
∈
Event with t
∈
T
∧
t
k
∈
T
k
∧
α
∈
Σ and t corresponds to t
k.In [1], the authors also proved that given any hybrid automaton H and k
∈
ℕ, the polynomial hybrid automaton Approx
(
H
,
k
) is an approximation of H.We study the relations between generic hybrid automata and their Taylor approximations.


## 3. The Simulation of a Hybrid Automaton and Its Approximation

Thebehavior is one of the most important concepts in formal methods, which shows a way of analyzing a formal system dynamically. The behavior analysis is also seen as the base of comparing formal systems. Formally, the behavior is composed of traces of sequences of states, which exhibits the system run. We study the relation between hybrid automata by their behaviors.There are two kinds of hybrid system run, namely, flow and jump, which interleave and interact. Starting from initial condition, the hybrid automaton shows state sequence, which we calledtrace. Similar to the discrete systems, the simplest comparison of hybrid automata is a trace equivalent, for example, whether hybrid automata own the same trace set. However, the trace equivalence is not an accurate way of comparison; it cannot distinguish different behaviors under the branching semantics. The hybrid system is composed of computational processes interacting with physical processes; it rejects the simple comparison which may hide the key information. In contrast, simulation relation checks each state in each trace starting from the initial; it is considered that simulation is more accurate for the complex branching semantics.Definition 3.
LetH
1
=
(
x
→
,
ϕ
init
1
,
Q
1
,
q
0
1
,
Σ
,
T
1
,
Act
1
,
Event
1
) and H
2
=
(
x
→
,
ϕ
init
2
,
Q
2
,
q
0
2
,
Σ
,
T
2
,
Act
2
,
Event
2
) be hybrid automata with the same event symbols. The binary relation ≻
⊆
Q
1
×
Q
2 is a simulation of H
2 by H
1 if the following two conditions hold.(i)
For each stateq
1
∈
Q
1, q
2
∈
Q
2, and t
∈
R being time elapsing, if q
1
⪯
q
2 and q
1
→
t
1
q
1, then there exists a state q
2
′ such that q
2
→
t
2
q
2
′ and q
1
′
⪯
q
2
′.
(ii)
For each stateq
1
∈
Q
1, q
2
∈
Q
2, and α
∈
Σ, if q
1
⪯
q
2 and q
1
→
α
1
q
1, then there exists a state q
2
′ such that q
2
→
α
2
q
2
′ and q
1
′
⪯
q
2
′.
(iii)
For initial stateq
0
2 and for state q
1
∈
Q
1, if q
1
⪯
q
0
2, then s
1
=
q
0
1. We denote H
1 is simulated by H
2 as H
1
⪯
H
2 for short.Definition3 shows a qualitative relation that the hybrid automaton H
2 simulates H
1. Because the hybrid systems are so complex that it is not easy to be analyzed directly, it is a common way of computing the reachability of the approximation. Let us define the approximation of a hybrid automaton formally; the following definition is from [1].Definition 4.
A hybrid automatonH
′ is an approximation of a hybrid automaton H if H
′ is obtained from H by replacing each formula ϕ with a formula ϕ
′ such that ⟦
ϕ
⟧
⊆
⟦
ϕ
′
⟧.The operator⟦
⟧ maps a formula to its satisfied value set, and it is proved in [1] that the Approx
(
H
,
k
) is the approximation of a hybrid automaton H.The Taylor approximation is one of the most useful and applicable approximation of a hybrid automaton. Although the Taylor approximation has been proposed for several years, the relation between the approximation and hybrid automaton is not well studied. It is interesting to check the simulation relation between an automaton and its Taylor approximation. We show this as a theorem.Theorem 5.
A hybrid automaton is simulated by its Taylor approximation, for example, for a hybrid automatonH, H
⪯
A
p
p
r
o
x
(
H
,
k
).Proof.
SupposeH
=
(
x
→
,
ϕ
init
,
Q
,
q
0
,
Σ
,
T
,
Act
,
Event
) is a hybrid automaton and Approx
(
H
,
k
)
=
(
x
→
,
ϕ
init
k
,
Q
′
,
q
0
′
,
Σ
,
T
k
,
Act
k
,
Event
′
) its Taylor approximation. Let q
∈
Q and q
′
∈
Q
′; q and q
′ have relation R, for example, q
R
q
′; we prove R is a simulation relation.
Case  1 (q
→
α
q
1 that α
∈
Σ be an event). According to Definition 2, Q
′ is constructed by a one-to-one mapping from Q; for example, ∃
q
k, q
1
k
∈
Q
′ that q
k
=
M
(
q
), q
1
k
=
M
(
q
1
), and q
k
→
α
q
1
k.
Case  2 (q
→
t
q that t
∈
R be time elapsing). According to Definition 2, ∃
q
k
∈
Q
′ that q
k
=
M
(
q
), Act
k
(
q
k
)
=
ϕ
k, and Act
(
q
)
=
ϕ. Then according to Definition 4, we have ⟦
ϕ
⟧
⊆
⟦
ϕ
k
⟧. Let u
→
=
(
u
1
,
…
,
t
0
,
u
1
′
,
…
,
u
n
′
) and u
→
=
(
u
1
,
…
,
t
0
+
t
,
u
1
′
,
…
,
u
n
′
) be two values that satisfy Act
(
q
) at moments t
0 and t
0
+
t separately; then t is a time duration; for example, we formally express this as u
→
=
(
u
1
,
…
,
t
0
,
u
1
′
,
…
,
u
n
′
), u
→
=
(
u
1
,
…
,
t
0
+
t
,
u
1
′
,
…
,
u
n
′
)
∈
⟦
ϕ
⟧. Because we have known that ⟦
ϕ
⟧
⊆
⟦
ϕ
k
⟧, then u
→
=
(
u
1
,
…
,
t
0
,
u
1
′
,
…
,
u
n
′
), u
→
=
(
u
1
,
…
,
t
0
+
t
,
u
1
′
,
…
,
u
n
′
)
∈
⟦
ϕ
k
⟧; for example, we get q
k
→
t
q
k.
Case  3 (q
0
k
=
M
(
q
0
) in terms of Definition 2). Then Theorem 5 is proved.From now on, we know that the Taylor approximation simulates its original hybrid automaton; for example, the behavior of the hybrid automaton is preserved by its Taylor approximation totally. Although there might be “granularity” problems while checking the safety related properties, the approximation provides a very applicable way. Moreover, Theorem5 could be extended to all types of approximations.


## 4. Approximate Equivalence Relation

Theorem5 shows a relation between simulation and approximation. Since approximation of a hybrid automaton is always quantifiable, we can study a quantified simulation relation indirectly.Two hybrid automata could be almost the same although their formulae may be different; for example, events are same; formula owns the same Taylor expansion regardless of their remainder. We call this relationTaylor
k
-related; k is the rank of this relevancy that shows that all formulae are derivable k
+
1 times. We can construct an upper bound in terms of upper bounds of remainders of two Taylor related hybrid automata and then construct a hybrid automaton that simulates both two systems.Theorem 6.
The Taylork-related hybrid automata are simulated by the same hybrid automaton.Proof.
SupposeH
i
=
(
x
→
,
ϕ
init
i
,
Q
i
,
q
0
i
,
Σ
,
T
i
,
Act
i
,
Event
i
) with i
=
{
1,2
}; H
1 and H
2 are Taylor k-related.
We can construct the Taylor approximation of each hybrid automaton,Approx
(
H
i
,
k
). According to Theorem 5, H
i
⪯
Approx
(
H
i
,
k
). Let Φ
i be the formulae set of H
i and Φ
i
k the set of Approx
(
H
i
,
k
); then according to Definition 2, for each ϕ
i
∈
Φ
i and ϕ
i
k
∈
Φ
i
k, we have
(4)
ϕ
i
k
=
{
P
i
k
(
f
i
,
y
i
)
-
R
i
k
(
f
i
,
y
i
,
ϕ
i
)
~
c
,
if
R
i
k
(
f
i
,
y
i
,
ϕ
i
)
≠
∞
;
true
,
if
R
i
k
(
f
i
,
y
i
,
ϕ
i
)
=
∞
.
Because H
1 and H
2 are Taylor k-related, then P
=
P
1
k
(
f
1
,
y
1
)
=
P
2
k
(
f
2
,
y
2
) and Event
1
(
(
q
1
,
ϕ
1
,
q
1
′
)
)
=
Event
2
(
(
q
2
,
ϕ
2
,
q
2
′
)
) with ϕ
i
∈
Φ
i.
Now we construct the hybrid automatonH
=
(
x
→
,
ϕ
init
,
Q
,
q
0
,
Σ
,
T
,
Act
,
Event
) with
(5)
ϕ
i
=
{
P
k
(
f
,
y
)
-
R
~
c
,
if
R
i
k
(
f
i
,
y
i
,
ϕ
i
)
≠
∞
;
true
,
if
R
i
k
(
f
i
,
y
i
,
ϕ
i
)
=
∞
.
R is an upper bound of R
1
k
(
f
1
,
y
1
,
ϕ
1
) and R
2
k
(
f
2
,
y
2
,
ϕ
2
) that ∀
u
→
∈
⟦
R
1
k
(
f
1
,
y
1
,
ϕ
1
)
⟧
∪
⟦
R
2
k
(
f
2
,
y
2
,
ϕ
2
)
⟧ and u
→
∈
⟦
R
⟧, and Event
(
(
q
,
ϕ
,
q
′
)
)
=
Event
(
(
q
1
,
ϕ
1
,
q
1
′
)
).
We proveH is an approximation of H
i; for example, prove that ⟦
ϕ
i
⟧
⊆
⟦
ϕ
⟧ for any formula ϕ. We have assumed that ~ is in {
<
,
≤
}. Let us begin with the base case where ϕ
i
=
P
i
k
(
f
i
,
y
i
→
)
-
R
i
k
(
f
i
,
y
i
→
,
ϕ
i
)
~
c and ϕ
=
P
-
R
~
c.
Letu
→ be a vector such that u
→
∈
⟦
ϕ
i
⟧; that is, f
i
(
u
→
)
~
c. Let r
i
k
(
f
,
u
→
,
0
→
) be Lagrange remainder of ϕ
i; for example,
(6)
r
i
k
(
f
i
,
u
→
,
0
→
)
=
∑
j
1
+
⋯
+
j
n
=
k
+
1
‍
(
(
D
1
j
1
⋯
D
n
j
n
f
)
(
0
→
)
)
·
u
1
j
1
⋯
u
n
j
n
j
1
!
⋯
j
n
!
.
According to Definition 2, r
i
k
(
f
i
,
u
→
,
0
→
)
∈
[
-
R
i
k
(
f
i
,
u
→
,
ϕ
i
)
,
R
i
k
(
f
i
,
u
→
,
ϕ
i
)
]. By previous analysis, there exists some remainder r
k
(
f
,
u
→
,
0
→
)
∈
[
-
R
,
R
]. Therefore,
(7)
(
u
→
,
r
i
k
(
f
i
,
u
→
,
0
→
)
)
∈
⟦
P
+
e
~
c
∧
e
∈
[
-
R
,
R
]
⟧
which is equivalent to
(8)
(
u
→
,
r
i
k
(
f
i
,
u
→
,
0
→
)
)
∈
⟦
e
~
c
-
P
∧
e
∈
[
-
R
,
R
]
⟧
.
Since e
≥
-
R and ~
∈
{
≤
,
<
}, the last equation above implies
(9)
(
u
→
,
r
i
k
(
f
i
,
u
→
,
0
→
)
)
∈
⟦
-
R
~
c
-
P
∧
e
∈
[
-
R
,
R
]
⟧
which is equivalent to
(10)
(
u
→
,
r
i
k
(
f
i
,
u
→
,
0
→
)
)
∈
⟦
P
-
R
~
c
∧
e
∈
[
-
R
,
R
]
⟧
,
which implies that u
→
∈
⟦
ϕ
⟧.
Then let us consider the cases of formulae composition, for example, formulae connected with∧ or/and ∨. Let us consider the inductive step ϕ
i
≡
ϕ
i
1
∨
ϕ
i
2. It holds that ϕ
≡
ϕ
1
∨
ϕ
2. By the inductive hypothesis, ⟦
ϕ
i
1
⟧
⊆
⟦
ϕ
1
⟧ and ⟦
ϕ
i
2
⟧
⊆
⟦
ϕ
2
⟧. Hence, ⟦
ϕ
i
⟧
=
⟦
ϕ
i
1
⟧
∪
⟦
ϕ
i
2
⟧
⊆
⟦
ϕ
1
⟧
∪
⟦
ϕ
2
⟧
=
⟦
ϕ
⟧. The case of ∧ is similar and not shown here.
Then we proved that⟦
ϕ
i
⟧
⊆
⟦
ϕ
⟧; for example, H is an approximation of H
i. According to Theorem 5, H simulate H
i. Then Theorem 6 is proved.We call the Taylor approximation of Taylork-related hybrid automataTaylor related approximation. It is easy to see that the Taylor related relation is an equivalence, for example, a relation satisfying reflexive, transitive and symmetry.Theorem 7.
The Taylor related approximation is an approximate equivalence, which is denoted as≍
k with k being the rank of relevancy.Then finally we propose a quantified approximate equivalence.We can compare two similar hybrid systems by their Taylor approximation, for example, a quantitative comparison thatk shows the degree of the similarity. Let us study a thermostat that is described in [2]; the temperature of a room is controlled by a thermostat which continuously senses the temperature and turns a heater on and off. When the heater is off, the temperature describes in terms of the function x
(
t
)
=
θ
e
-
K
t; when the heater is on, the temperature follows x
(
t
)
=
θ
e
-
K
t
+
h
(
1
-
e
-
K
t
), where h and K are constants. We can express the thermostat formally in Figure 1.Figure 1
Hybrid automaton for a thermostat.According to Theorem5, we can construct its approximation (see Figure 3 in [1]); the thermostat is simulated by its approximation; for example, let the hybrid automaton of thermostat be denoted as H and let its approximate beApprox
(
H
,
3
); then H
⪯
Approx
(
H
,
3
). Furthermore, in terms of Theorem 7, it is easy to know thatH
≍
3
Approx
(
H
,
3
).


## 5. Conclusion

In this paper, we studied the simulation relation among the hybrid automata and their Taylor approximations and then proposed an approximate equivalence relation. The simulation relation discovers how a Taylor approximation confirms to its original hybrid automaton; meanwhile, the equivalence explores the degree of similarity of similar automata quantitatively. In future, we plan studying the bisimulation of the automata and approximations in two ways, a more accurate approximation theory and metric semantics of hybrid automata.



---

*Source: 850789-2014-05-11.xml*