# A Case Study on Formal Analysis of an Automated Guided Vehicle System

Authors: Jie Zhang; Yuntao Peng; William N. N. Hung; Xiaojuan Li; Jindong Tan; Zhiping Shi
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

This paper considers a hybrid I/O automata model for an automated guided vehicle (AGV) system. A set of key properties of an AGV system are characterized for the correctness of the system. An abstract model is constructed from the hybrid automata model to simplify the proof of the constraints. The two models are equivalent in terms of bisimulation relation. We derive the constraints to ensure
the correctness of the properties. We validate the system by analyzing the parameters of the constraints of the AGV system.


---

## Body

## 1. Introduction

Complex systems cannot be described by a pure discrete model or a continuous model [1–3]. Hybrid models have become increasingly popular in the last few decades as systems become increasingly complex. A hybrid system is a dynamic system with interacting continuous time triggered and discrete event triggered dynamics [1, 2, 4–6]. Many applications involve hybrid systems, such as embedded controllers [7], robotics [8, 9], mobile computing [10], and process control [11], in which high reliability is a requirement [4]. To model such a system, we need to describe and analyze it with the rigorous use of mathematics. An I/O automaton is used to model concurrent and distributed discrete event systems [12]. A hybrid input/output automaton (HIOA) [4] is a framework, which is developed by Lynch et al. and extended from hybrid automata for modeling complex hybrid systems. This is done by dividing the state variables of a HIOA into two sets, classified as internal variables and external variables, where the external variables include input variables and output variables. Discrete transitions and continuous trajectories can change the states of a system. An extremely important feature of the hybrid I/O automaton framework is that the hybrid system is divided into multiple modules. These modules are described so that the hybrid system can be modeled easily. The hybrid I/O automaton uses the external variables, input variables, and output variables to communicate among the automatons.Automated guided vehicles (AGVs) are robots that move on the floor of a facility directed by a combination of software and sensor-based guidance systems. Earlier inventions on AGVs can be dated back to Barrett Electronics in 1953. One of the oldest publications on AGV can be found in [13]. In the past, AGVs were typically deployed to manufacturing facilities due to their efficiency, accuracy, and flexibility. Nowadays, AGVs are also used in warehouses, distribution centers and transshipment terminals, and so forth for repeated transportation tasks [14, 15]. The tracking path for the AGV can be designed as a circle, ellipse, sine wave, or other shapes such as arbitrary curves [16, 17]. The tracking trajectory is very important as many papers develop effective approaches to solve it, but our AGV is an example of applying HIOA modeling. Our modeling is inspired by [2]. But unlike [2] which uses a straight line orbit that can be approximated to one-dimension, we investigate a two-dimensional problem where an automated guided vehicle moves along a circular painted orbit.The first contribution of this paper is the formal modeling of an automated guided vehicle system using hybrid I/O automata. The second contribution of this paper is a set of important constraints which are characterized to ensure the correctness of the properties of the vehicle system. In order to simplify the model, we abstract a model from the hybrid automata of the AGV and establish a bisimulation relation between the two automata.This paper is organized as follows. In Section2, an automated guided vehicle system is introduced. In Section 3, the HIOA framework is introduced. In Section 4, we present a HIOA model of the AGV system and abstract a model from HIOA model. We prove that the two models have a bisimulation relation. In Section 5, we extract the key properties and deduce the corresponding constraints to ensure the correctness of the properties. We analyze the parameters of the AGV system at the end of Section 6. Finally, we point out some directions for future work.


## 2. An Automated Guided Vehicle System

We introduce the structure and behavior of a vehicle. The vehicle consists of five components: the left wheels, the right wheels, chassis, sensor, and controller. Figure1 shows a circular orbit tracking of our vehicle which is the focus of the remainder of this paper. The vehicle has two degrees of freedom. One is the velocity such that, at any time t, it can move forward with a speed of v
(
t
), with the restriction that 0
≤
v
(
t
)
≤
10 mph (miles per hour). The other degree of freedom is the circular movement of the vehicle such that at any time t the vehicle can rotate its body via the wheels with an angular speed of -
π
≤
ω
(
t
)
≤
π rad/s (radians per second). Ignoring the inertia of the vehicle, we assume that we can instantaneously change the velocity or angular speed. The sensor measures the displacement e
(
t
) between the center of the vehicle and the center of the track using an array of photodiodes. As the AGV passes over the track, the diode directly above the track generates more current than the other diodes. If the vehicle is close enough to the track, it will move forward. When the vehicle strays too far to the left, it will steer to the right; and when the vehicle strays too far to the right, it will steer to the left. The vehicle can be stopped at any time as long as it receives the control signal. If the vehicle is too far away from the track that it is difficult to follow the track, then it moves backward.Figure 1
AGV tracking circular painted orbit.


## 3. Hybrid I/O Automata Framework

In this section, we first introduce some basic notions about the model we use and then consider the definitions and theories of hybrid automata, hybrid I/O automata, and their operations [4]. More detailed discussion of the hybrid I/O automata can be found in [4].


### 3.1. Basic Notions

Hybrid behaviors, including discrete behavior, continuous behavior, and information flows into the system, are often described using static and dynamic variables, trajectories, and hybrid sequences. First, we introduce several basic notions involved in hybrid behavior. A location of the internal state of a system or a location of a connection between a component of a system and a component of another system can be represented as a variable, which may be static in type and denote a set of values of the variable, or dynamic in type and indicate a set of trajectories of the variable. A set of variables can be changed by discrete transitions, which are taken via discrete actions when they are enabled or by trajectories over a time interval. A hybrid sequence represents a series of changes that occur instantaneously along with the evolution of time and may be finite or infinite.


### 3.2. Hybrid Automata

As hybrid I/O automata are an extension of hybrid automata, we define the structure of hybrid automata first in order to describe the hybrid I/O automata. The definition of hybrid automata is given below, where≜ denotes mathematical definition. For a more detailed description, see [4].Definition 1.
A hybrid automaton (HA) is an eight-tupleH
M
=
(
E
V
,
I
V
,
S
,
s
0
,
E
A
,
I
A
,
D
T
,
T
), where (i)
E
V is a set of external variables,
(ii)
I
V is a set of internal variables, and V
≜
E
V
∪
I
V is the disjunction that represent all variables,
(iii)
S
⊆
val
(
I
V
) is a set of states,
(iv)
s
0
⊆
S is a nonempty set of initial states,
(v)
E
A is a set of external actions,
(vi)
I
A is a set of internal actions, and A
≜
E
A
∪
I
A is the union of E
A and I
A,
(vii)
D
T
⊆
S
×
A
×
S is a set of discrete transitions,
(viii)
T is a set of trajectories for V. For every τ
∈
T and t
∈
dom
⁡
(
τ
) (domain of τ), we have τ
(
t
)
⌈
I
V
∈
S, where τ
(
t
)
⌈
I
v is the restriction of τ
(
t
) to I
V; that is, the function g with dom
⁡
(
g
)
=
dom
⁡
(
τ
)
∩
I
v such that g
(
t
)
=
τ
(
t
). We require the following axioms:
(A1)
for allτ
∈
T  for all τ
′
≤
τ
τ
′
∈
T;
(A2)
for allτ
∈
T  for all t
∈
dom
⁡
(
τ
)
τ
⊳
t
∈
T where τ
⊳
t denotes (
(
τ
⌈
[
t
,
+
∞
)
)
-
t
);
(A3)
supposeτ
0
,
τ
1
,
τ
2
,
…
,
τ
i
,
… is a sequence of trajectories in T; if τ
i is closed and τ
i
·
l
state
=
τ
i
+
1
·
f
state, where i
∈
ℕ, τ
i is not the last trajectory of the hybrid sequence, then τ
0
⌢
τ
1
⌢
τ
2
⋯
∈
T, where τ
⌢
τ
′
≜
τ
∪
(
τ
′
⌈
(
0
,
∞
)
+
τ
·
l
time
).The execution fragment of a hybrid automaton is a hybrid sequenceα
=
τ
0
a
1
τ
1
a
2
,
…
,
τ
i
a
i
+
1
,
…, where τ
i
∈
T, where i is a nonnegative integer and T is defined in Definition 1; and if τ
i is not the last trajectory, then τ
i
·
l
state
→
a
i
+
1
τ
i
+
1
·
f
state, where l
state represents the last state and f
state denotes the first state. Any input trajectory of the composition can be accepted by the composition, and we say that the components of the composition are strongly compatible HIOAs. Trace is the external behavior of a hybrid I/O automaton. Concatenation represents two hybrid sequences linked together. Let and be hybrid sequences and closed, with the concatenation being denoted by α
⌢
α
′
≜
init
(
α
)
(
last
(
α
)
⌢
head
(
α
′
)
)
tail
(
α
′
).


### 3.3. Hybrid I/O Automata

We described the hybrid automata above. Here, we present the behavior and structure of a HIOA. A HIOA is used to model a complex hybrid system. The discrete state of the controller can be modeled by control modes, represented as internal variables. Each mode observes an invariant condition. The internal variables can be changed in two ways: in a discrete transition or in a continuous trajectory. External variables, including input variables and output variables, are used to exchange information between two automatons. Here is the definition of a hybrid input/output automaton. For a more detailed description, see [4].Definition 2.
A hybrid I/O automaton (HIOA) is a five-tupleA
M
=
(
H
M
,
U
,
Y
,
I
,
O
), where (i)
H
M
=
(
E
V
,
I
V
,
S
,
s
0
,
E
A
,
I
A
,
D
T
,
T
) is a hybrid automaton,
(ii)
U
⊆
E
V is a set of input variables,
(iii)
Y
≜
E
V
∖
U is a set of output variables,
(iv)
I is a set of input actions,
(v)
O is a set of output actions,
(vi)
the following axioms are satisfied:
(A1)
for allx
∈
S  for all α
∈
I
∃
x
′
∈
S such that x
→
a
x
′,
(A2)
lettrajs
(
U
) denote the set of all trajectories for U, for all x
∈
S  for all υ
∈
trajs
(
U
)
∃
τ
∈
T such that τ
·
f
state
=
x
,
τ
↓
U
≤
υ, and either
(a)
τ
↓
U
=
υ, or
(b)
τ is closed and some l
∈
L is enabled in τ
·
l
state,
whereg
=
τ
↓
U represents dom
⁡
(
g
)
=
dom
⁡
(
τ
) such that, for
all
c
∈
dom
⁡
(
g
) has g
(
c
)
=
τ
(
c
)
⌈
U.
We further define(i)
Z
≜
I
V
∪
Y is a set of variables that are locally controlled, and
(ii)
L
≜
I
A
∪
O is a set of actions that are locally controlled.Typically, it is difficult to model a complex system in one shot. HIOA can decompose a hybrid system into multiple components, model the modules as HIOAs, respectively, and then compose them in the end. We introduce a very important operation to compose two HIOAs, denoted as symbol∥. For the proof of Theorem 3 and Lemma 4, see [4].Theorem 3.
A
M
1
∥
A
M
2 is a hybrid I/O automaton when A
M
1 and A
M
2 are strongly compatible hybrid I/O automata and U
1
∩
Y
2
=
∅.Another important operation is hiding external variables in HIOA. SupposeE
V
⊆
E
V
A, B
M
=
VarHide
(
E
V
,
A
M
), E
V
B
=
E
V
A
-
E
V, and T
B
M
=
T
A
M
↓
(
V
A
M
-
E
V
).Lemma 4.
IfA
M is a HIOA and E
V
⊆
E
V
A
M, then VarHide
(
E
V
,
A
M
) is a HIOA.Definition 5 (simulation relations).
For all statesx
A
M and x
B
M of A
M and B
M, given two comparable HIOAs, from A
M to B
M there exists a simulation relation R
S
⊆
S
A
M
×
S
B
M (denoted as A
M
R
S
B
M) when the following three conditions are met: (i)
knowing thatx
A
M
∈
s
0
A
M and suppose there exists a state x
B
M
∈
s
0
B
M such that x
A
M
R
S
x
B
M, where s
0
A
M is the set of initial states of A
M and s
0
B
M is the set of initial states of B
M;
(ii)
supposex
A
M
R
S
x
B
M and an execution fragment of A
M; execution fragment α
=
τ
0
a
1
τ
1
a
2
,
…
,
τ
i
a
i
+
1
,
…, meets α
·
f
state
=
x
A
M; there exists a closed execution fragment β in B
M that meets β
·
f
state
=
x
B
M, trace
(
β
)
=
trace
(
α
), and α
·
f
state
R
β
·
f
state;
(iii)
supposex
A
M
R
S
x
B
M and an execution fragment of A
M
α
=
τ
0 has α
·
f
state
=
x
B
M; there exists a closed execution fragment β in B
M that meets β
·
f
state
=
x
B
M, trace
(
β
)
=
trace
(
α
), and α
·
l
state
R
β
·
l
state.Corollary 6.
Given two comparable HAsA
M and B
M, and a simulation from A
M to B
M denoted as A
M
R
s
B
M, then t
r
a
c
e
s
A
M
⊆
t
r
a
c
e
s
B
M.The proof refers to [4]. According to [18, 19], we define a bisimulation as follows.Definition 7 (bisimulation).
Given two comparable HIOAsA
M and B
M, for all pairs (
p
,
q
) among all reachable states of A
M and B
M, p in A
M, and q in B
M. If all reachable states p
* in A
M have p
→
a
p
*, this implies the existence of a state q
* in B
M such that p
→
a
p
*. At the same time, all reachable states q
* in B
M have p
→
a
p
*, implying that there exists a state q
* in A
M such that p
→
a
p
*. Under these circumstances, we say that A
M and B
M have a bisimulation relation.


## 3.1. Basic Notions

Hybrid behaviors, including discrete behavior, continuous behavior, and information flows into the system, are often described using static and dynamic variables, trajectories, and hybrid sequences. First, we introduce several basic notions involved in hybrid behavior. A location of the internal state of a system or a location of a connection between a component of a system and a component of another system can be represented as a variable, which may be static in type and denote a set of values of the variable, or dynamic in type and indicate a set of trajectories of the variable. A set of variables can be changed by discrete transitions, which are taken via discrete actions when they are enabled or by trajectories over a time interval. A hybrid sequence represents a series of changes that occur instantaneously along with the evolution of time and may be finite or infinite.


## 3.2. Hybrid Automata

As hybrid I/O automata are an extension of hybrid automata, we define the structure of hybrid automata first in order to describe the hybrid I/O automata. The definition of hybrid automata is given below, where≜ denotes mathematical definition. For a more detailed description, see [4].Definition 1.
A hybrid automaton (HA) is an eight-tupleH
M
=
(
E
V
,
I
V
,
S
,
s
0
,
E
A
,
I
A
,
D
T
,
T
), where (i)
E
V is a set of external variables,
(ii)
I
V is a set of internal variables, and V
≜
E
V
∪
I
V is the disjunction that represent all variables,
(iii)
S
⊆
val
(
I
V
) is a set of states,
(iv)
s
0
⊆
S is a nonempty set of initial states,
(v)
E
A is a set of external actions,
(vi)
I
A is a set of internal actions, and A
≜
E
A
∪
I
A is the union of E
A and I
A,
(vii)
D
T
⊆
S
×
A
×
S is a set of discrete transitions,
(viii)
T is a set of trajectories for V. For every τ
∈
T and t
∈
dom
⁡
(
τ
) (domain of τ), we have τ
(
t
)
⌈
I
V
∈
S, where τ
(
t
)
⌈
I
v is the restriction of τ
(
t
) to I
V; that is, the function g with dom
⁡
(
g
)
=
dom
⁡
(
τ
)
∩
I
v such that g
(
t
)
=
τ
(
t
). We require the following axioms:
(A1)
for allτ
∈
T  for all τ
′
≤
τ
τ
′
∈
T;
(A2)
for allτ
∈
T  for all t
∈
dom
⁡
(
τ
)
τ
⊳
t
∈
T where τ
⊳
t denotes (
(
τ
⌈
[
t
,
+
∞
)
)
-
t
);
(A3)
supposeτ
0
,
τ
1
,
τ
2
,
…
,
τ
i
,
… is a sequence of trajectories in T; if τ
i is closed and τ
i
·
l
state
=
τ
i
+
1
·
f
state, where i
∈
ℕ, τ
i is not the last trajectory of the hybrid sequence, then τ
0
⌢
τ
1
⌢
τ
2
⋯
∈
T, where τ
⌢
τ
′
≜
τ
∪
(
τ
′
⌈
(
0
,
∞
)
+
τ
·
l
time
).The execution fragment of a hybrid automaton is a hybrid sequenceα
=
τ
0
a
1
τ
1
a
2
,
…
,
τ
i
a
i
+
1
,
…, where τ
i
∈
T, where i is a nonnegative integer and T is defined in Definition 1; and if τ
i is not the last trajectory, then τ
i
·
l
state
→
a
i
+
1
τ
i
+
1
·
f
state, where l
state represents the last state and f
state denotes the first state. Any input trajectory of the composition can be accepted by the composition, and we say that the components of the composition are strongly compatible HIOAs. Trace is the external behavior of a hybrid I/O automaton. Concatenation represents two hybrid sequences linked together. Let and be hybrid sequences and closed, with the concatenation being denoted by α
⌢
α
′
≜
init
(
α
)
(
last
(
α
)
⌢
head
(
α
′
)
)
tail
(
α
′
).


## 3.3. Hybrid I/O Automata

We described the hybrid automata above. Here, we present the behavior and structure of a HIOA. A HIOA is used to model a complex hybrid system. The discrete state of the controller can be modeled by control modes, represented as internal variables. Each mode observes an invariant condition. The internal variables can be changed in two ways: in a discrete transition or in a continuous trajectory. External variables, including input variables and output variables, are used to exchange information between two automatons. Here is the definition of a hybrid input/output automaton. For a more detailed description, see [4].Definition 2.
A hybrid I/O automaton (HIOA) is a five-tupleA
M
=
(
H
M
,
U
,
Y
,
I
,
O
), where (i)
H
M
=
(
E
V
,
I
V
,
S
,
s
0
,
E
A
,
I
A
,
D
T
,
T
) is a hybrid automaton,
(ii)
U
⊆
E
V is a set of input variables,
(iii)
Y
≜
E
V
∖
U is a set of output variables,
(iv)
I is a set of input actions,
(v)
O is a set of output actions,
(vi)
the following axioms are satisfied:
(A1)
for allx
∈
S  for all α
∈
I
∃
x
′
∈
S such that x
→
a
x
′,
(A2)
lettrajs
(
U
) denote the set of all trajectories for U, for all x
∈
S  for all υ
∈
trajs
(
U
)
∃
τ
∈
T such that τ
·
f
state
=
x
,
τ
↓
U
≤
υ, and either
(a)
τ
↓
U
=
υ, or
(b)
τ is closed and some l
∈
L is enabled in τ
·
l
state,
whereg
=
τ
↓
U represents dom
⁡
(
g
)
=
dom
⁡
(
τ
) such that, for
all
c
∈
dom
⁡
(
g
) has g
(
c
)
=
τ
(
c
)
⌈
U.
We further define(i)
Z
≜
I
V
∪
Y is a set of variables that are locally controlled, and
(ii)
L
≜
I
A
∪
O is a set of actions that are locally controlled.Typically, it is difficult to model a complex system in one shot. HIOA can decompose a hybrid system into multiple components, model the modules as HIOAs, respectively, and then compose them in the end. We introduce a very important operation to compose two HIOAs, denoted as symbol∥. For the proof of Theorem 3 and Lemma 4, see [4].Theorem 3.
A
M
1
∥
A
M
2 is a hybrid I/O automaton when A
M
1 and A
M
2 are strongly compatible hybrid I/O automata and U
1
∩
Y
2
=
∅.Another important operation is hiding external variables in HIOA. SupposeE
V
⊆
E
V
A, B
M
=
VarHide
(
E
V
,
A
M
), E
V
B
=
E
V
A
-
E
V, and T
B
M
=
T
A
M
↓
(
V
A
M
-
E
V
).Lemma 4.
IfA
M is a HIOA and E
V
⊆
E
V
A
M, then VarHide
(
E
V
,
A
M
) is a HIOA.Definition 5 (simulation relations).
For all statesx
A
M and x
B
M of A
M and B
M, given two comparable HIOAs, from A
M to B
M there exists a simulation relation R
S
⊆
S
A
M
×
S
B
M (denoted as A
M
R
S
B
M) when the following three conditions are met: (i)
knowing thatx
A
M
∈
s
0
A
M and suppose there exists a state x
B
M
∈
s
0
B
M such that x
A
M
R
S
x
B
M, where s
0
A
M is the set of initial states of A
M and s
0
B
M is the set of initial states of B
M;
(ii)
supposex
A
M
R
S
x
B
M and an execution fragment of A
M; execution fragment α
=
τ
0
a
1
τ
1
a
2
,
…
,
τ
i
a
i
+
1
,
…, meets α
·
f
state
=
x
A
M; there exists a closed execution fragment β in B
M that meets β
·
f
state
=
x
B
M, trace
(
β
)
=
trace
(
α
), and α
·
f
state
R
β
·
f
state;
(iii)
supposex
A
M
R
S
x
B
M and an execution fragment of A
M
α
=
τ
0 has α
·
f
state
=
x
B
M; there exists a closed execution fragment β in B
M that meets β
·
f
state
=
x
B
M, trace
(
β
)
=
trace
(
α
), and α
·
l
state
R
β
·
l
state.Corollary 6.
Given two comparable HAsA
M and B
M, and a simulation from A
M to B
M denoted as A
M
R
s
B
M, then t
r
a
c
e
s
A
M
⊆
t
r
a
c
e
s
B
M.The proof refers to [4]. According to [18, 19], we define a bisimulation as follows.Definition 7 (bisimulation).
Given two comparable HIOAsA
M and B
M, for all pairs (
p
,
q
) among all reachable states of A
M and B
M, p in A
M, and q in B
M. If all reachable states p
* in A
M have p
→
a
p
*, this implies the existence of a state q
* in B
M such that p
→
a
p
*. At the same time, all reachable states q
* in B
M have p
→
a
p
*, implying that there exists a state q
* in A
M such that p
→
a
p
*. Under these circumstances, we say that A
M and B
M have a bisimulation relation.


## 4. Modeling the AGV System

We model the AGV system using HIOA. Inspired by [2], the AGV system is modeled as a network of hybrid automata as shown in Figure 2. The model consists of five parts: chassis, left wheels, right wheels, sensor, and controller, respectively. The five components communicate via shared variables. In Figure 2, variables θ
1 and θ
2 are the angles of the left and right wheels relative to the x-axis positive direction of globe coordinate, respectively. Variables x and y represent the chassis coordinates with respect to the global coordinate frame. Variable e is the distance e
(
t
) from which the center of the AGV deviates from the center of the track at time t. The variable is used to communicate between the sensor and the controller. The controller receives the variable e, sends control signals to the left wheel and the right wheel, and then changes the mode of the AGV.Figure 2
Network of hybrid automata for an AGV.XOY is the global coordinate frame.v is the forward velocity of the car. t
sample is the sampling time. ω is the angular speed of the vehicle. e
(
t
) is the displacement of the center of the vehicle from the track at time t. ɛ
1 is the threshold indicating that the AGV is close enough to the center of the track that the AGV can move straight ahead in a forward mode. ɛ
2 is the threshold indicating that there is too great a distance between the center of the AGV and the center of track, and that the vehicle must therefore be steered to the other side. ɛ
3 is the threshold denoting that the vehicle has strayed so far from the center of track that the vehicle is in an unsafe condition and must be moved back via switching to the back mode. α is the maximum angle of vehicle velocity direction to the tangential direction of the center point on the track, where 0
≤
α
≤
π
/
2. θ is the angle of the vehicle velocity direction to the x-axis positive direction. η is the angle of the vehicle velocity direction to the tangential direction of the center point on the track, where -
α
≤
η
≤
α. R is the radius of the track.The AGV system is decomposed into five components and modeled as hybrid automata: chassis, LWheel, RWheel, sensor, and controller, respectively.


### 4.1. Component Chassis

The chassis secures the position of each component. The state is composed of three state variables:〈
x
,
y
,
θ
〉 where x is the x-coordinate of the center of the vehicle; y is the y-coordinate of the center of the vehicle; and θ is the angle of the vehicle velocity direction to the x-axis positive direction. We use differential algebraic equations (DAEs) to describe the dynamic of the chassis. Initially, we ensure that the vehicle moves forward, and the initial condition is
(1)
η
∈
[
-
α
,
α
]
∧
|
e
(
t
)
|
≤
ɛ
1
.From Figure2, the chassis secures the wheels. Hence the left wheels, right wheels, and the chassis have the same angles. We obtain the following algebraic equation:
(2)
θ
1
=
θ
2
=
θ
.


### 4.2. Component LWheel

We model the behavior of left wheels as the hybrid automaton LWheel. The left wheel has external variables:x
1, which gives the x-coordinate of the left wheel; y
1, which gives the y-coordinate of the right wheel; and θ
1, which is the angle of the moving direction of the left wheel to the x-axis positive direction. The types of these variables are real. This hybrid automaton model has no actions or discrete transitions, just satisfied trajectories. It communicates with the controller via the Boolean variable l
_
control and is
_
stop. We obtain differential equations for the left wheel as follows:
(3)
d
x
1
d
t
=
i
f
stop
t
h
e
n
0
e
l
s
e
i
f
l
_
control
t
h
e
n
v
cos
⁡
⁡
θ
1
e
l
s
e
-
v
cos
⁡
⁡
θ
1
d
y
1
d
t
=
i
f
stop
t
h
e
n
0
e
l
s
e
i
f
l
_
control
t
h
e
n
v
sin
⁡
θ
1
e
l
s
e
-
v
sin
⁡
θ
1
.


### 4.3. Component RWheel

Since the left wheels and right wheels are symmetrical, we omit the description of the right wheels.


### 4.4. Component Sensor

We model the behavior of thesensor as the hybrid automaton sensor, whose output at time t, for all t
e
(
t
)
=
f
(
x
(
t
)
,
y
(
t
)
), gives the center position of the AGV relative to the center of the track, shown in Figure 1. The sensor communicates with the controller through the variable e, which equals e
(
t
). Since the hybrid automaton sensor has no internal variables, and there are neither actions nor discrete transitions, only the following algebraic equation is met for the trajectories of the sensor:
(4)
sensor
=
e
(
t
)
=
f
(
x
(
t
)
,
y
(
t
)
)
.


### 4.5. Component Controller

The controller can be divided into two levels. The supervisory controller determines the structure of the mode transition and guards the enabled transitions. The low-level controller determines the time-based inputs to the system. We are modeling the behavior of the controller as a hybrid automatoncontroller, whose input is the sensor value and the output the control signals to the left and right wheels that determine the operation of the wheels. There is a clock built into the controller for measuring the time interval since the last sampling. We use the variable c to represent this clock. A clock can be modeled as a first-order differential equation, and the clock variable c is defined as follows:
(5)
c
=
k
·
t
,
where k is the rate of the clock, t is the variable of time, and k
=
d
[
c
(
t
)
]
/
d
t. In our model, the value of k can be a constant 1.The controller has a variablee, which gets its value from the sensor. There are two variables recording the value of the sensor: variable new
_
sample, used to record the latest sample value, and variable sample, used to record the last sample value. In order to ensure that the vehicle moves forward, the initial states should satisfy:
(6)
c
=
0
∧
sample
∈
[
-
ϵ
1
,
ϵ
1
]
.We define a transition as occurring when a guard in an outgoing transition from the current state becomes enabled. This control logic is captured in the mode transitions. The outputs are the pure signalsis
_
stop, forward, and backward. There are three Boolean variables recording the outputs, is
_
stop, l
_
control, and r
_
control, respectively. We use an asterisk * to represent the next sample value. When the internal action clock transitions is taken, each state transition that is enabled will be taken:
(7)
c
=
t
sample
⇝
{
c
*
=
0
sampl
e
*
=
new
_
sample
,
where ⇝ denotes the event trigger.For trajectories we require that(8)
sample
(
t
1
)
=
sample
(
t
2
)
,
for all time t
1
,
t
2 between clock transitions; that is, t
1
,
t
2
∈
[
m
·
t
sample
,
(
m
+
1
)
·
t
sample
) for all m
∈
ℕ.Thenew
_
sample will record the new value from the sensor:
(9)
new
_
sample
=
e
(
t
)
.For every state, the following equations must hold:(10)
a
a
a
a
i
d
c
d
t
=
1
l
_
control
=
i
f
sample
∈
[
-
ϵ
3
,
ϵ
3
]
t
h
e
n
true
aaaaaaaaaa
e
l
s
e
false
r
_
control
=
i
f
sample
∈
[
-
ϵ
3
,
ϵ
3
]
t
h
e
n
true
aaaaaaaaaa
e
l
s
e
false
aa
is
_
stop
=
i
f
stop
t
h
e
n
true
aaaaaaaaaa
e
l
s
e
false
.The control logic determines the change in the state of the controller. Our AGV is running on the circular track. Since the circle is symmetrical, it suffices for us to just consider the situation of the first quadrant. The refinement of the mode gives the dynamic behavior of the output as a function of the input. We know that the displacemente
(
t
) is the function of x and y and that the control logic guards the transitions whether enabled or not. They are as follows:
(11)
forward
⟹
¬
stop
∧
-
ϵ
1
≤
e
(
t
)
≤
ϵ
1
⟹
{
x
′
=
v
cos
⁡
θ
,
y
′
=
v
sin
θ
,
θ
′
=
0
right
⟹
¬
stop
∧
ϵ
3
≥
e
(
t
)
>
ϵ
2
⟹
{
x
′
=
v
cos
⁡
θ
,
y
′
=
v
sin
θ
,
θ
′
=
-
ω
left
⟹
¬
stop
∧
-
ϵ
3
≤
e
(
t
)
<
-
ϵ
2
⟹
{
x
′
=
v
cos
⁡
θ
,
y
′
=
v
sin
θ
,
θ
′
=
ω
back
⟹
¬
stop
∧
e
(
t
)
<
-
ϵ
3
∨
e
(
t
)
>
ϵ
3
⟹
{
x
′
=
-
v
cos
⁡
θ
,
y
′
=
-
v
sin
θ
,
θ
′
=
0
stop
⟹
{
x
′
=
0
,
y
′
=
0
,
θ
′
=
0
maintain
⟹
{
-
ϵ
2
≤
e
(
t
)
<
-
ϵ
1
,
or
ϵ
1
<
e
(
t
)
≤
ϵ
2
.


### 4.6. Composition

Since the left wheels, the right wheels, and the chassis have no output, they cannot be regarded as hybrid I/O automata. Sinceθ
1 and θ
2 are the internal variables of wheels, we are modeling the three components as the hybrid I/O automaton Plant by hiding these variables. In our model, Plant, is
_
stop, l
_
control, and r
_
control are inputs, and x and y are outputs:
(12)
Plant
=
VarHide
(
{
θ
1
,
θ
2
}
,
(
Chassis
∥
LWheel
∥
RWheel
)
)
.Likewise, the sensor can be regarded as a hybrid I/O automaton, for which the inputs arex and y, and the output is e. The controller can also be viewed as a hybrid I/O automaton for which the input is e, and the outputs are is
_
stop, l
_
control, and r
_
control. According to Theorem 3 and Lemma 4, all of the components of the system are HIOAs and the composition also an HIOA. We have obtained a complete hybrid I/O automaton of the AGV system by hiding the external variables:
(13)
H
M
=
VarHide
(
{
x
,
y
,
e
,
is
_
stop
,
l
_
control
,
r
_
control
}
,
(
Plant
∥
Sensor
∥
Controller
)
{
}
)
.


### 4.7. Abstraction

We expect that the AGV is always moving forward and never moves backward and use (14) to describe this situation. We select the appropriate threshold and ensure that the vehicle moves in the way we expect by specifying parameter constraints for all reachable states of the hybrid I/O automata H
M:
(14)
|
sample
|
≤
ϵ
3
.In addition, we hope that the forward mode occurs infinitely often:(15)
GF
(
c
=
0
∧
|
sample
|
≤
ϵ
1
)
.In order to simplify the model, we abstract a modelA
M from the previous model H
M. Then, we use model A
M instead of H
M. We find the constraints we need from model A
M to guarantee the correctness of the properties that we expect. Here, we simplify the model in several ways, as follows.Based on (8), we know that the value of the variable sample remains unchanged during the interval after the current sampling and before the next sampling. Therefore we can easily prove that (14) is satisfied. We cannot consider the influence of the clock variable c. Furthermore, we assume that the vehicle is at the initial state at the time 0:
(16)
c
=
0
⟹
|
e
(
t
)
|
≤
ϵ
3
.We find that the variablesnew
_
sample and sample are ruled out in our abstract model. Now, we use the refinements of the five modes of AGV to describe the dynamic behavior of an AGV. The formulas of the five modes are given as φ
forward
,
φ
right
,
φ
left
,
φ
back
,
and
φ
stop, respectively; φ
step is the disjunction of the five:
(17)
φ
step
≜
φ
right
∨
φ
left
∨
φ
forward
∨
φ
back
∨
φ
stop
φ
forward
≜
{
¬
stop
,
|
e
(
t
)
|
≤
ϵ
1
,
x
*
=
x
+
v
cos
⁡
θ
t
sample
,
y
*
=
y
+
v
sin
θ
t
sample
,
θ
*
=
θ
φ
right
≜
{
¬
stop
,
e
(
t
)
>
ϵ
2
,
x
*
=
x
+
v
cos
⁡
θ
t
sample
,
y
*
=
y
+
v
sin
θ
t
sample
,
θ
*
=
θ
-
ω
t
sample
φ
left
≜
{
¬
stop
,
e
(
t
)
<
-
ϵ
2
,
x
*
=
x
+
v
cos
⁡
θ
t
sample
,
y
*
=
y
+
v
sin
θ
t
sample
,
θ
*
=
θ
+
ω
t
sample
φ
back
≜
{
¬
stop
,
|
e
(
t
)
|
>
ϵ
3
,
x
*
=
x
-
v
cos
⁡
θ
t
sample
,
y
*
=
y
-
v
sin
θ
t
sample
,
θ
*
=
θ
φ
stop
≜
{
stop
,
x
*
=
x
,
y
*
=
y
,
θ
*
=
θ
.Now we get the abstract model of the AGV system. Since the abstract modelA omits the time variable, it is simpler than the original model. We will derive and verify the properties using the abstract model. There are two kinds of typical errors in formal verification, one is true error, where errors exist in the physical system, but the result of formal verification is correct. The reason of first kind of error is because we abstract a model from our original model, and the details we omitted may lead to the errors of original model being omitted, so we get a passing proof. The other is false error which do not exist in the physical system but the result of formal verification is incorrect. The reason is that abstract model omitted the details of original model. The abstract model cannot express the original system due to lack of information from the original system, and then the result of formal verification is incorrect.In order to ensure the two kinds of errors never occur, we prove the original modelH
M and the abstract model A
M have a bisimulation equivalence relationship.Lemma 8.
LetS
K be a set of all reachable states of H
M, for all s
∈
S
R; one has
(18)
c
=
0
⟹
[
|
s
a
m
p
l
e
|
≤
ϵ
2
⟺
|
e
(
t
)
|
≤
ϵ
2
]Proof.
Use (14) and (15) to prove Lemma 8.Theorem 9.
The two comparable HIOAsH
M and A
M have a bisimulation relation.Proof.
Owing to the limitation of space, we do not provide a detailed proof of Theorem9, but the key step will be given. H
M and A
M satisfy the following condition:
(19)
c
H
M
=
0
∧
θ
H
M
=
θ
A
M
∧
x
H
M
=
x
A
M
∧
y
H
M
=
y
A
M
.
For all state pairs(
p
,
q
) among all reachable states of H
M and A
M, p
∈
H
M and q
∈
A
M, if states of state pair (
p
,
q
) hold the weakest condition of labeled transition system respectively, we say the pair (
p
,
q
) is bisimulation equivalent. If each initial state of H
M bisimulates an initial state of A
M, and there exists an execution fragment from p to p
*, where p
* in H
M has p
→
p
*, implying the existence of a transition according to the transition predicate φ
step of A
M from q to q
* in A
M, such that q
⇒
q
*. At the same time, there exists a transition according to the transition predicate φ
step of A
M from q to q
*, where q
* in A
M has q
⇒
q
*, implying the existence of an execution fragment from p to p
*, where p
* in H
M, such that p
→
p
*. We can then use Definition 5, Corollary 6, and Definition 7 to prove Theorem 9.


## 4.1. Component Chassis

The chassis secures the position of each component. The state is composed of three state variables:〈
x
,
y
,
θ
〉 where x is the x-coordinate of the center of the vehicle; y is the y-coordinate of the center of the vehicle; and θ is the angle of the vehicle velocity direction to the x-axis positive direction. We use differential algebraic equations (DAEs) to describe the dynamic of the chassis. Initially, we ensure that the vehicle moves forward, and the initial condition is
(1)
η
∈
[
-
α
,
α
]
∧
|
e
(
t
)
|
≤
ɛ
1
.From Figure2, the chassis secures the wheels. Hence the left wheels, right wheels, and the chassis have the same angles. We obtain the following algebraic equation:
(2)
θ
1
=
θ
2
=
θ
.


## 4.2. Component LWheel

We model the behavior of left wheels as the hybrid automaton LWheel. The left wheel has external variables:x
1, which gives the x-coordinate of the left wheel; y
1, which gives the y-coordinate of the right wheel; and θ
1, which is the angle of the moving direction of the left wheel to the x-axis positive direction. The types of these variables are real. This hybrid automaton model has no actions or discrete transitions, just satisfied trajectories. It communicates with the controller via the Boolean variable l
_
control and is
_
stop. We obtain differential equations for the left wheel as follows:
(3)
d
x
1
d
t
=
i
f
stop
t
h
e
n
0
e
l
s
e
i
f
l
_
control
t
h
e
n
v
cos
⁡
⁡
θ
1
e
l
s
e
-
v
cos
⁡
⁡
θ
1
d
y
1
d
t
=
i
f
stop
t
h
e
n
0
e
l
s
e
i
f
l
_
control
t
h
e
n
v
sin
⁡
θ
1
e
l
s
e
-
v
sin
⁡
θ
1
.


## 4.3. Component RWheel

Since the left wheels and right wheels are symmetrical, we omit the description of the right wheels.


## 4.4. Component Sensor

We model the behavior of thesensor as the hybrid automaton sensor, whose output at time t, for all t
e
(
t
)
=
f
(
x
(
t
)
,
y
(
t
)
), gives the center position of the AGV relative to the center of the track, shown in Figure 1. The sensor communicates with the controller through the variable e, which equals e
(
t
). Since the hybrid automaton sensor has no internal variables, and there are neither actions nor discrete transitions, only the following algebraic equation is met for the trajectories of the sensor:
(4)
sensor
=
e
(
t
)
=
f
(
x
(
t
)
,
y
(
t
)
)
.


## 4.5. Component Controller

The controller can be divided into two levels. The supervisory controller determines the structure of the mode transition and guards the enabled transitions. The low-level controller determines the time-based inputs to the system. We are modeling the behavior of the controller as a hybrid automatoncontroller, whose input is the sensor value and the output the control signals to the left and right wheels that determine the operation of the wheels. There is a clock built into the controller for measuring the time interval since the last sampling. We use the variable c to represent this clock. A clock can be modeled as a first-order differential equation, and the clock variable c is defined as follows:
(5)
c
=
k
·
t
,
where k is the rate of the clock, t is the variable of time, and k
=
d
[
c
(
t
)
]
/
d
t. In our model, the value of k can be a constant 1.The controller has a variablee, which gets its value from the sensor. There are two variables recording the value of the sensor: variable new
_
sample, used to record the latest sample value, and variable sample, used to record the last sample value. In order to ensure that the vehicle moves forward, the initial states should satisfy:
(6)
c
=
0
∧
sample
∈
[
-
ϵ
1
,
ϵ
1
]
.We define a transition as occurring when a guard in an outgoing transition from the current state becomes enabled. This control logic is captured in the mode transitions. The outputs are the pure signalsis
_
stop, forward, and backward. There are three Boolean variables recording the outputs, is
_
stop, l
_
control, and r
_
control, respectively. We use an asterisk * to represent the next sample value. When the internal action clock transitions is taken, each state transition that is enabled will be taken:
(7)
c
=
t
sample
⇝
{
c
*
=
0
sampl
e
*
=
new
_
sample
,
where ⇝ denotes the event trigger.For trajectories we require that(8)
sample
(
t
1
)
=
sample
(
t
2
)
,
for all time t
1
,
t
2 between clock transitions; that is, t
1
,
t
2
∈
[
m
·
t
sample
,
(
m
+
1
)
·
t
sample
) for all m
∈
ℕ.Thenew
_
sample will record the new value from the sensor:
(9)
new
_
sample
=
e
(
t
)
.For every state, the following equations must hold:(10)
a
a
a
a
i
d
c
d
t
=
1
l
_
control
=
i
f
sample
∈
[
-
ϵ
3
,
ϵ
3
]
t
h
e
n
true
aaaaaaaaaa
e
l
s
e
false
r
_
control
=
i
f
sample
∈
[
-
ϵ
3
,
ϵ
3
]
t
h
e
n
true
aaaaaaaaaa
e
l
s
e
false
aa
is
_
stop
=
i
f
stop
t
h
e
n
true
aaaaaaaaaa
e
l
s
e
false
.The control logic determines the change in the state of the controller. Our AGV is running on the circular track. Since the circle is symmetrical, it suffices for us to just consider the situation of the first quadrant. The refinement of the mode gives the dynamic behavior of the output as a function of the input. We know that the displacemente
(
t
) is the function of x and y and that the control logic guards the transitions whether enabled or not. They are as follows:
(11)
forward
⟹
¬
stop
∧
-
ϵ
1
≤
e
(
t
)
≤
ϵ
1
⟹
{
x
′
=
v
cos
⁡
θ
,
y
′
=
v
sin
θ
,
θ
′
=
0
right
⟹
¬
stop
∧
ϵ
3
≥
e
(
t
)
>
ϵ
2
⟹
{
x
′
=
v
cos
⁡
θ
,
y
′
=
v
sin
θ
,
θ
′
=
-
ω
left
⟹
¬
stop
∧
-
ϵ
3
≤
e
(
t
)
<
-
ϵ
2
⟹
{
x
′
=
v
cos
⁡
θ
,
y
′
=
v
sin
θ
,
θ
′
=
ω
back
⟹
¬
stop
∧
e
(
t
)
<
-
ϵ
3
∨
e
(
t
)
>
ϵ
3
⟹
{
x
′
=
-
v
cos
⁡
θ
,
y
′
=
-
v
sin
θ
,
θ
′
=
0
stop
⟹
{
x
′
=
0
,
y
′
=
0
,
θ
′
=
0
maintain
⟹
{
-
ϵ
2
≤
e
(
t
)
<
-
ϵ
1
,
or
ϵ
1
<
e
(
t
)
≤
ϵ
2
.


## 4.6. Composition

Since the left wheels, the right wheels, and the chassis have no output, they cannot be regarded as hybrid I/O automata. Sinceθ
1 and θ
2 are the internal variables of wheels, we are modeling the three components as the hybrid I/O automaton Plant by hiding these variables. In our model, Plant, is
_
stop, l
_
control, and r
_
control are inputs, and x and y are outputs:
(12)
Plant
=
VarHide
(
{
θ
1
,
θ
2
}
,
(
Chassis
∥
LWheel
∥
RWheel
)
)
.Likewise, the sensor can be regarded as a hybrid I/O automaton, for which the inputs arex and y, and the output is e. The controller can also be viewed as a hybrid I/O automaton for which the input is e, and the outputs are is
_
stop, l
_
control, and r
_
control. According to Theorem 3 and Lemma 4, all of the components of the system are HIOAs and the composition also an HIOA. We have obtained a complete hybrid I/O automaton of the AGV system by hiding the external variables:
(13)
H
M
=
VarHide
(
{
x
,
y
,
e
,
is
_
stop
,
l
_
control
,
r
_
control
}
,
(
Plant
∥
Sensor
∥
Controller
)
{
}
)
.


## 4.7. Abstraction

We expect that the AGV is always moving forward and never moves backward and use (14) to describe this situation. We select the appropriate threshold and ensure that the vehicle moves in the way we expect by specifying parameter constraints for all reachable states of the hybrid I/O automata H
M:
(14)
|
sample
|
≤
ϵ
3
.In addition, we hope that the forward mode occurs infinitely often:(15)
GF
(
c
=
0
∧
|
sample
|
≤
ϵ
1
)
.In order to simplify the model, we abstract a modelA
M from the previous model H
M. Then, we use model A
M instead of H
M. We find the constraints we need from model A
M to guarantee the correctness of the properties that we expect. Here, we simplify the model in several ways, as follows.Based on (8), we know that the value of the variable sample remains unchanged during the interval after the current sampling and before the next sampling. Therefore we can easily prove that (14) is satisfied. We cannot consider the influence of the clock variable c. Furthermore, we assume that the vehicle is at the initial state at the time 0:
(16)
c
=
0
⟹
|
e
(
t
)
|
≤
ϵ
3
.We find that the variablesnew
_
sample and sample are ruled out in our abstract model. Now, we use the refinements of the five modes of AGV to describe the dynamic behavior of an AGV. The formulas of the five modes are given as φ
forward
,
φ
right
,
φ
left
,
φ
back
,
and
φ
stop, respectively; φ
step is the disjunction of the five:
(17)
φ
step
≜
φ
right
∨
φ
left
∨
φ
forward
∨
φ
back
∨
φ
stop
φ
forward
≜
{
¬
stop
,
|
e
(
t
)
|
≤
ϵ
1
,
x
*
=
x
+
v
cos
⁡
θ
t
sample
,
y
*
=
y
+
v
sin
θ
t
sample
,
θ
*
=
θ
φ
right
≜
{
¬
stop
,
e
(
t
)
>
ϵ
2
,
x
*
=
x
+
v
cos
⁡
θ
t
sample
,
y
*
=
y
+
v
sin
θ
t
sample
,
θ
*
=
θ
-
ω
t
sample
φ
left
≜
{
¬
stop
,
e
(
t
)
<
-
ϵ
2
,
x
*
=
x
+
v
cos
⁡
θ
t
sample
,
y
*
=
y
+
v
sin
θ
t
sample
,
θ
*
=
θ
+
ω
t
sample
φ
back
≜
{
¬
stop
,
|
e
(
t
)
|
>
ϵ
3
,
x
*
=
x
-
v
cos
⁡
θ
t
sample
,
y
*
=
y
-
v
sin
θ
t
sample
,
θ
*
=
θ
φ
stop
≜
{
stop
,
x
*
=
x
,
y
*
=
y
,
θ
*
=
θ
.Now we get the abstract model of the AGV system. Since the abstract modelA omits the time variable, it is simpler than the original model. We will derive and verify the properties using the abstract model. There are two kinds of typical errors in formal verification, one is true error, where errors exist in the physical system, but the result of formal verification is correct. The reason of first kind of error is because we abstract a model from our original model, and the details we omitted may lead to the errors of original model being omitted, so we get a passing proof. The other is false error which do not exist in the physical system but the result of formal verification is incorrect. The reason is that abstract model omitted the details of original model. The abstract model cannot express the original system due to lack of information from the original system, and then the result of formal verification is incorrect.In order to ensure the two kinds of errors never occur, we prove the original modelH
M and the abstract model A
M have a bisimulation equivalence relationship.Lemma 8.
LetS
K be a set of all reachable states of H
M, for all s
∈
S
R; one has
(18)
c
=
0
⟹
[
|
s
a
m
p
l
e
|
≤
ϵ
2
⟺
|
e
(
t
)
|
≤
ϵ
2
]Proof.
Use (14) and (15) to prove Lemma 8.Theorem 9.
The two comparable HIOAsH
M and A
M have a bisimulation relation.Proof.
Owing to the limitation of space, we do not provide a detailed proof of Theorem9, but the key step will be given. H
M and A
M satisfy the following condition:
(19)
c
H
M
=
0
∧
θ
H
M
=
θ
A
M
∧
x
H
M
=
x
A
M
∧
y
H
M
=
y
A
M
.
For all state pairs(
p
,
q
) among all reachable states of H
M and A
M, p
∈
H
M and q
∈
A
M, if states of state pair (
p
,
q
) hold the weakest condition of labeled transition system respectively, we say the pair (
p
,
q
) is bisimulation equivalent. If each initial state of H
M bisimulates an initial state of A
M, and there exists an execution fragment from p to p
*, where p
* in H
M has p
→
p
*, implying the existence of a transition according to the transition predicate φ
step of A
M from q to q
* in A
M, such that q
⇒
q
*. At the same time, there exists a transition according to the transition predicate φ
step of A
M from q to q
*, where q
* in A
M has q
⇒
q
*, implying the existence of an execution fragment from p to p
*, where p
* in H
M, such that p
→
p
*. We can then use Definition 5, Corollary 6, and Definition 7 to prove Theorem 9.


## 5. Correctness

### 5.1. The Desired Properties ofA
M

For a system, we often hope that bad things will never happen, a situation called safety, that good things will eventually happen, and that they will happen infinitely often, a situation called fairness. We express the properties via invariants. For our system, we expect the displacement from the center of the AGV to the center of the track to never be larger than the thresholdɛ
3, and never be less than the threshold -
ɛ
3. At the same time, we ensure that η lies in the interval [
-
α
,
α
].Property 1.
The vehicle always moves forward and never moves backward. It can be described as(20)
φ
safety
≜
η
∈
[
-
α
,
α
]
∧
|
e
(
t
)
|
≤
ɛ
3
.Property 2.
The vehicle moves forward infinitely often. It can be described using the temporal logic formula(21)
φ
fairness
≜
GF
|
e
(
t
)
|
≤
ɛ
1
.Lemma 10.
Ifφ
s
a
f
e
t
y is an invariant of A
M and formula φ
f
a
i
r
n
e
s
s holds for A
M, then (14) is an invariant of H
M and (15) holds for H
M.Proof.
Use Lemma8, Theorem 9, and (8) to prove Lemma 10.


### 5.2. Parameter Constraints of the AGV System

In this section, we will give several parameter constraints for our AGV system. They are indispensable to guaranteeing the correctness of the properties of safety (20) and fairness (21). We define them in (22).Parameter Constraints. Consider the following
(22)
φ
1
≜
(
v
cos
⁡
α
t
sample
)
2
+
(
R
+
ɛ
2
+
v
sin
α
t
sample
)
2
aai
≤
(
ɛ
3
+
R
)
φ
2
≜
(
R
-
ɛ
2
)
2
+
v
2
t
sample
2
-
2
(
R
-
ɛ
2
)
v
t
sample
sin
α
aai
≥
(
R
-
ɛ
3
)
2
φ
3
≜
ω
t
sample
≤
α
φ
4
≜
(
R
-
ɛ
3
)
2
aai
≤
(
v
cos
⁡
α
t
sample
)
2
+
(
R
-
ɛ
2
+
v
sin
α
t
sample
)
2
aai
≤
(
R
+
ɛ
1
)
2
.Theorem 11.
Ifφ
1, φ
2, and φ
3 are met, then the φ
s
a
f
e
t
y property is an invariant of A
M; that is,
(23)
φ
s
a
f
e
t
y
∧
φ
1
∧
φ
2
∧
φ
3
⟹
φ
s
a
f
e
t
y
*
.Proof.
In the first step, we prove thatφ
safety
∧
φ
1
⇒
0
≤
e
*
(
t
)
≤
ɛ
3 holds. Since the circle is symmetrical, we only need to consider the situation of the first quadrant. In order to guarantee that |
e
(
t
)
|
≤
ɛ
3 is met in all cases of outside the circle track, we consider the most extreme case of the outside of the circle. First of all, suppose that the vehicle moves on the outside of the circle shown in Figure 3. The vehicle is very close to point A at the time of the current sampling, and e
(
t
)
≤
ɛ
2. The vehicle then moves forward to B with η
=
α at the next sampling; the e
(
t
) reaches the largest displacement. We use φ
1 to illustrate that 0
<
e
(
t
)
≤
ɛ
3 holds for A
M. The derivations in (24) show that e
*
(
t
)
≤
ɛ
3.
Deriving from
φ
1. Consider the following:
(24)
(
v
cos
⁡
α
t
sample
)
2
+
(
R
+
ɛ
2
+
v
sin
α
t
sample
)
2
≤
(
ɛ
3
+
R
)
2
(
v
cos
⁡
α
t
sample
)
2
+
(
R
+
ɛ
2
+
v
sin
α
t
sample
)
2
≤
(
ɛ
3
+
R
)
(
v
cos
⁡
α
t
sample
)
2
+
(
R
+
ɛ
2
+
v
sin
α
t
sample
)
2
-
R
≤
ɛ
3
|
B
D
|
2
+
|
O
D
|
2
-
R
≤
ɛ
3
(
use
the
Pythagorean
theorem
)
|
B
D
|
2
-
R
≤
ɛ
3
|
O
B
|
-
R
≤
ɛ
3
e
*
(
t
)
≤
ɛ
3
.
Since the vehicle moves on the outside of the circle,e
(
t
)
*
>
0. Therefore, φ
safety
∧
φ
1
⇒
0
<
e
*
(
t
)
≤
ɛ
3.
In the second step, we prove thatφ
safety
∧
φ
2
⇒
-
ɛ
3
≤
e
*
(
t
)
≤
0 holds. In order to guarantee that |
e
(
t
)
|
≤
ɛ
3 in all cases inside the track of the circle, we consider the most extreme case inside. First of all, suppose that the vehicle moves on the inside of the circle shown in Figure 4. The vehicle is very close to point A at the time of the current sampling, with e
(
t
)
>
-
ɛ
2, and then moves forward to B with η
=
-
α at the next sampling, where the vehicle reaches the farthest to the track. We use φ
2 to illustrate that -
φ
3
≤
e
(
t
)
<
0 holds for A
M. The derivations in (25) show that e
*
(
t
)
≥
-
ɛ
3.
Deriving from
φ
2
. Consider the following:
(25)
(
R
-
ɛ
2
)
2
+
v
2
t
sample
2
-
2
(
R
-
ɛ
2
)
v
t
sample
sin
α
≥
(
R
-
ɛ
3
)
2
(
R
-
ɛ
2
)
2
+
v
2
t
sample
2
-
2
(
R
-
ɛ
2
)
v
|
sin
(
-
α
)
|
t
sample
≥
R
-
ɛ
3
|
O
A
|
2
+
|
A
B
|
2
-
2
|
O
A
∥
A
B
∥
sin
(
-
α
)
|
≥
R
-
ɛ
3
|
O
A
|
2
+
|
A
B
|
2
-
2
|
O
A
|
|
A
B
|
cos
⁡
(
π
2
-
α
)
≥
R
-
ɛ
3
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
i
(
use
the
Law
of
cosines
)
|
O
B
|
≥
R
-
ɛ
3
O
B
-
R
≥
-
ɛ
3
e
*
(
t
)
≥
-
ɛ
3
.
Since the vehicle moves on the inside of the circle,e
*
(
t
)
<
0. Therefore, φ
safety
∧
φ
2
⇒
-
ɛ
3
≤
e
*
(
t
)
≤
0.
In the third step, we prove thatφ
safety
∧
φ
3
⇒
η
*
∈
[
-
α
,
α
] holds. Constraint ω
t
sample
≤
α is required to guarantee that η is always in the interval [
-
α
,
α
]. First of all, we consider the scenario shown in Figure 5. We build a coordinate frame X
′
O
′
Y
′ shown in Figure 5. If the vehicle reaches point A in the current sampling, the vehicle will steer to the left. The angle η
<
0 (the angle between A
B
⟶ and O
′
X
′
⟶), relative to the coordinate frame X
′
O
′
Y
′, is η
*
=
η
+
ω
t
sample
<
ω
t
sample at the next sampling. If ω
t
sample
≤
α, then η
*
=
η
+
ω
t
sample
<
α. If the vehicle reaches point C in the current sampling, the vehicle will steer to the left. The angle η
>
0 (the angle between C
D
⟶ and O
′
X
′
⟶), relative to the coordinate frame X
′
O
′
Y
′, is η
*
=
η
-
ω
t
sample
>
-
ω
t
sample at the next sampling. If ω
t
sample
≤
α, then -
ω
t
sample
≥
-
α, and we will get η
*
=
η
-
ω
t
sample
>
-
α. We have proved that η
*
∈
[
-
α
,
α
].
Therefore,φ
safety
∧
φ
1
∧
φ
2
∧
φ
3
⇒
φ
safety
* is proved.Figure 3
Illustration of the need forφ
1.Figure 4
Illustration of the need forφ
2.Figure 5
Illustration of the need forφ
3.Theorem 12.
Ifφ
4 holds for A
M, then the property of φ
f
a
i
r
n
e
s
s is an invariance of A
M; that is, φ
f
a
i
r
n
e
s
s
∧
φ
4
⇒
φ
f
a
i
r
n
e
s
s
*.Proof.
In order to ensure that the vehicle moves forward infinitely often, we avoid the situation of always steering to left after steering to right, and steering to right after steering to left. We consider the scenario shown in Figure6. The center of the vehicle is very close to pointA in the current sampling, and e
(
t
)
<
ɛ
2, with the velocity direction approximate parallel to the direction of the tangent of point A, shown as a dashed line. The vehicle steers to the left, moves along the arc A
B
⌢, and we look at A
B
⌢ as a straight line A
B. Suppose that η
=
α, e
(
t
)
<
ɛ
1 at the next sampling and that the vehicle switches to the forward mode. From φ
4, we can derive the following:
(26)
R
-
ɛ
1
≤
|
O
B
|
≤
R
+
ɛ
1
(
R
>
ɛ
3
>
ɛ
2
>
ɛ
1
)
-
ɛ
1
≤
|
O
B
|
-
R
≤
-
ɛ
1
-
ɛ
1
≤
e
*
(
t
)
≤
-
ɛ
1
|
e
*
(
t
)
|
≤
-
ɛ
1
.Figure 6
Illustration of the need forφ
4.


## 5.1. The Desired Properties ofA
M

For a system, we often hope that bad things will never happen, a situation called safety, that good things will eventually happen, and that they will happen infinitely often, a situation called fairness. We express the properties via invariants. For our system, we expect the displacement from the center of the AGV to the center of the track to never be larger than the thresholdɛ
3, and never be less than the threshold -
ɛ
3. At the same time, we ensure that η lies in the interval [
-
α
,
α
].Property 1.
The vehicle always moves forward and never moves backward. It can be described as(20)
φ
safety
≜
η
∈
[
-
α
,
α
]
∧
|
e
(
t
)
|
≤
ɛ
3
.Property 2.
The vehicle moves forward infinitely often. It can be described using the temporal logic formula(21)
φ
fairness
≜
GF
|
e
(
t
)
|
≤
ɛ
1
.Lemma 10.
Ifφ
s
a
f
e
t
y is an invariant of A
M and formula φ
f
a
i
r
n
e
s
s holds for A
M, then (14) is an invariant of H
M and (15) holds for H
M.Proof.
Use Lemma8, Theorem 9, and (8) to prove Lemma 10.


## 5.2. Parameter Constraints of the AGV System

In this section, we will give several parameter constraints for our AGV system. They are indispensable to guaranteeing the correctness of the properties of safety (20) and fairness (21). We define them in (22).Parameter Constraints. Consider the following
(22)
φ
1
≜
(
v
cos
⁡
α
t
sample
)
2
+
(
R
+
ɛ
2
+
v
sin
α
t
sample
)
2
aai
≤
(
ɛ
3
+
R
)
φ
2
≜
(
R
-
ɛ
2
)
2
+
v
2
t
sample
2
-
2
(
R
-
ɛ
2
)
v
t
sample
sin
α
aai
≥
(
R
-
ɛ
3
)
2
φ
3
≜
ω
t
sample
≤
α
φ
4
≜
(
R
-
ɛ
3
)
2
aai
≤
(
v
cos
⁡
α
t
sample
)
2
+
(
R
-
ɛ
2
+
v
sin
α
t
sample
)
2
aai
≤
(
R
+
ɛ
1
)
2
.Theorem 11.
Ifφ
1, φ
2, and φ
3 are met, then the φ
s
a
f
e
t
y property is an invariant of A
M; that is,
(23)
φ
s
a
f
e
t
y
∧
φ
1
∧
φ
2
∧
φ
3
⟹
φ
s
a
f
e
t
y
*
.Proof.
In the first step, we prove thatφ
safety
∧
φ
1
⇒
0
≤
e
*
(
t
)
≤
ɛ
3 holds. Since the circle is symmetrical, we only need to consider the situation of the first quadrant. In order to guarantee that |
e
(
t
)
|
≤
ɛ
3 is met in all cases of outside the circle track, we consider the most extreme case of the outside of the circle. First of all, suppose that the vehicle moves on the outside of the circle shown in Figure 3. The vehicle is very close to point A at the time of the current sampling, and e
(
t
)
≤
ɛ
2. The vehicle then moves forward to B with η
=
α at the next sampling; the e
(
t
) reaches the largest displacement. We use φ
1 to illustrate that 0
<
e
(
t
)
≤
ɛ
3 holds for A
M. The derivations in (24) show that e
*
(
t
)
≤
ɛ
3.
Deriving from
φ
1. Consider the following:
(24)
(
v
cos
⁡
α
t
sample
)
2
+
(
R
+
ɛ
2
+
v
sin
α
t
sample
)
2
≤
(
ɛ
3
+
R
)
2
(
v
cos
⁡
α
t
sample
)
2
+
(
R
+
ɛ
2
+
v
sin
α
t
sample
)
2
≤
(
ɛ
3
+
R
)
(
v
cos
⁡
α
t
sample
)
2
+
(
R
+
ɛ
2
+
v
sin
α
t
sample
)
2
-
R
≤
ɛ
3
|
B
D
|
2
+
|
O
D
|
2
-
R
≤
ɛ
3
(
use
the
Pythagorean
theorem
)
|
B
D
|
2
-
R
≤
ɛ
3
|
O
B
|
-
R
≤
ɛ
3
e
*
(
t
)
≤
ɛ
3
.
Since the vehicle moves on the outside of the circle,e
(
t
)
*
>
0. Therefore, φ
safety
∧
φ
1
⇒
0
<
e
*
(
t
)
≤
ɛ
3.
In the second step, we prove thatφ
safety
∧
φ
2
⇒
-
ɛ
3
≤
e
*
(
t
)
≤
0 holds. In order to guarantee that |
e
(
t
)
|
≤
ɛ
3 in all cases inside the track of the circle, we consider the most extreme case inside. First of all, suppose that the vehicle moves on the inside of the circle shown in Figure 4. The vehicle is very close to point A at the time of the current sampling, with e
(
t
)
>
-
ɛ
2, and then moves forward to B with η
=
-
α at the next sampling, where the vehicle reaches the farthest to the track. We use φ
2 to illustrate that -
φ
3
≤
e
(
t
)
<
0 holds for A
M. The derivations in (25) show that e
*
(
t
)
≥
-
ɛ
3.
Deriving from
φ
2
. Consider the following:
(25)
(
R
-
ɛ
2
)
2
+
v
2
t
sample
2
-
2
(
R
-
ɛ
2
)
v
t
sample
sin
α
≥
(
R
-
ɛ
3
)
2
(
R
-
ɛ
2
)
2
+
v
2
t
sample
2
-
2
(
R
-
ɛ
2
)
v
|
sin
(
-
α
)
|
t
sample
≥
R
-
ɛ
3
|
O
A
|
2
+
|
A
B
|
2
-
2
|
O
A
∥
A
B
∥
sin
(
-
α
)
|
≥
R
-
ɛ
3
|
O
A
|
2
+
|
A
B
|
2
-
2
|
O
A
|
|
A
B
|
cos
⁡
(
π
2
-
α
)
≥
R
-
ɛ
3
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
a
i
(
use
the
Law
of
cosines
)
|
O
B
|
≥
R
-
ɛ
3
O
B
-
R
≥
-
ɛ
3
e
*
(
t
)
≥
-
ɛ
3
.
Since the vehicle moves on the inside of the circle,e
*
(
t
)
<
0. Therefore, φ
safety
∧
φ
2
⇒
-
ɛ
3
≤
e
*
(
t
)
≤
0.
In the third step, we prove thatφ
safety
∧
φ
3
⇒
η
*
∈
[
-
α
,
α
] holds. Constraint ω
t
sample
≤
α is required to guarantee that η is always in the interval [
-
α
,
α
]. First of all, we consider the scenario shown in Figure 5. We build a coordinate frame X
′
O
′
Y
′ shown in Figure 5. If the vehicle reaches point A in the current sampling, the vehicle will steer to the left. The angle η
<
0 (the angle between A
B
⟶ and O
′
X
′
⟶), relative to the coordinate frame X
′
O
′
Y
′, is η
*
=
η
+
ω
t
sample
<
ω
t
sample at the next sampling. If ω
t
sample
≤
α, then η
*
=
η
+
ω
t
sample
<
α. If the vehicle reaches point C in the current sampling, the vehicle will steer to the left. The angle η
>
0 (the angle between C
D
⟶ and O
′
X
′
⟶), relative to the coordinate frame X
′
O
′
Y
′, is η
*
=
η
-
ω
t
sample
>
-
ω
t
sample at the next sampling. If ω
t
sample
≤
α, then -
ω
t
sample
≥
-
α, and we will get η
*
=
η
-
ω
t
sample
>
-
α. We have proved that η
*
∈
[
-
α
,
α
].
Therefore,φ
safety
∧
φ
1
∧
φ
2
∧
φ
3
⇒
φ
safety
* is proved.Figure 3
Illustration of the need forφ
1.Figure 4
Illustration of the need forφ
2.Figure 5
Illustration of the need forφ
3.Theorem 12.
Ifφ
4 holds for A
M, then the property of φ
f
a
i
r
n
e
s
s is an invariance of A
M; that is, φ
f
a
i
r
n
e
s
s
∧
φ
4
⇒
φ
f
a
i
r
n
e
s
s
*.Proof.
In order to ensure that the vehicle moves forward infinitely often, we avoid the situation of always steering to left after steering to right, and steering to right after steering to left. We consider the scenario shown in Figure6. The center of the vehicle is very close to pointA in the current sampling, and e
(
t
)
<
ɛ
2, with the velocity direction approximate parallel to the direction of the tangent of point A, shown as a dashed line. The vehicle steers to the left, moves along the arc A
B
⌢, and we look at A
B
⌢ as a straight line A
B. Suppose that η
=
α, e
(
t
)
<
ɛ
1 at the next sampling and that the vehicle switches to the forward mode. From φ
4, we can derive the following:
(26)
R
-
ɛ
1
≤
|
O
B
|
≤
R
+
ɛ
1
(
R
>
ɛ
3
>
ɛ
2
>
ɛ
1
)
-
ɛ
1
≤
|
O
B
|
-
R
≤
-
ɛ
1
-
ɛ
1
≤
e
*
(
t
)
≤
-
ɛ
1
|
e
*
(
t
)
|
≤
-
ɛ
1
.Figure 6
Illustration of the need forφ
4.


## 6. Analysis of Constraints

In this section, we analyze the parameters of our AGV system. We rewrite the constraints as shown in (27).Rewrite Constraints. Consider the following:
(27)
φ
1
≜
v
2
t
sample
2
+
ɛ
2
2
+
2
ɛ
2
v
sin
α
t
sample
aai
≤
ɛ
3
2
+
2
R
(
ɛ
3
-
ɛ
2
-
v
sin
α
t
sample
)
φ
2
≜
(
R
-
ɛ
2
-
v
t
sample
)
2
+
2
(
R
-
ɛ
2
)
v
t
sample
(
1
-
sin
α
)
aai
≥
(
R
-
ɛ
3
)
2
φ
3
≜
ω
t
sample
≤
α
.We assume that the value range ofv is from v
min
⁡ to v
max
⁡, t
sample is from t
min
⁡ to t
max
⁡, α is from α
min
⁡ to α
max
⁡, ɛ
1 is from ɛ
1
min
⁡ to ɛ
1
max
⁡, ɛ
2 is from ɛ
2
min
⁡ to ɛ
2
max
⁡, ɛ
3 is from ɛ
3
min
⁡ to ɛ
3
max
⁡, R is from R
min
⁡ to R
max
⁡, and ω is from ω
min
⁡ to ω
max
⁡. The inequalities shown in (28) need to be met to ensure that the parameter constraints hold.Inequalities Needed for the Parameter Constraints. Consider the following:
(28)
v
max
⁡
2
t
max
⁡
2
+
ɛ
2
max
⁡
2
+
2
ɛ
2
max
⁡
v
max
⁡
sin
α
max
⁡
t
max
⁡
≤
ɛ
3
min
⁡
2
+
2
R
min
⁡
(
ɛ
3
min
⁡
-
ɛ
2
max
⁡
-
v
max
⁡
sin
α
max
⁡
t
max
⁡
)
(
R
max
⁡
-
ɛ
3
min
⁡
)
2
≤
(
R
min
⁡
-
ɛ
2
max
⁡
-
v
max
⁡
t
max
⁡
)
2
+
2
(
R
min
⁡
-
ɛ
2
max
⁡
)
v
min
⁡
t
min
⁡
(
1
-
sin
α
max
⁡
)
ω
max
⁡
t
max
⁡
≤
α
min
⁡
(
R
max
⁡
-
ɛ
1
min
⁡
)
2
≤
v
min
⁡
2
t
sample
2
+
(
R
min
⁡
-
ɛ
2
max
⁡
)
2
+
2
(
R
min
⁡
-
ɛ
2
max
⁡
)
v
min
⁡
sin
α
min
⁡
t
min
⁡
(
R
min
⁡
+
ɛ
1
min
⁡
)
2
≥
v
max
⁡
2
t
max
⁡
2
+
(
R
max
⁡
-
ɛ
2
min
⁡
)
2
+
2
(
R
max
⁡
-
ɛ
2
min
⁡
)
v
max
⁡
sin
α
max
⁡
t
max
⁡
.It is obvious that the parametersɛ
1
max
⁡
,
ɛ
3
max
⁡
,
and
ω
min
⁡ do not appear in the constraint inequalities. Therefore, we increase ɛ
1 and ɛ
3 from the minimum and decrease ω from the maximum. We do not know the exact values of such parameters as v
,
t
sample
,
ω, and can measure their values only by operating the vehicle. Errors cannot be avoided when we obtain these parameters. We can write the predicate logic formula asserting safety φ
safety as follows:
(29)
∀
α
∈
[
α
min
⁡
,
α
max
⁡
]
,
∀
ɛ
1
≥
ɛ
1
min
⁡
,
∀
ɛ
2
∈
[
ɛ
2
min
⁡
,
ɛ
2
max
⁡
]
,
∀
ɛ
3
≥
ɛ
3
min
⁡
∀
R
∈
[
R
min
⁡
,
R
max
⁡
]
:
φ
safety
∧
φ
1
∧
φ
2
∧
φ
3
⟹
φ
safety
*
.Parametersv and ω can be viewed as the internal variables of the vehicle.


## 7. Conclusion

In this paper, we have modeled an AGV system using a hybrid I/O system and investigated a two-dimensional problem where the vehicle moves in a circular orbit. We derived and proved the constraints of the parameters of the AGV system so that the vehicle always move forward closely following the circular track and never moves backward. We have also analyzed the constraints of the parameters and the range of the parameters. Future research can extend this formulation from circular track to arbitrary complex curves, consider slopes or hilly terrains, and reason about multiple vehicle systems.



---

*Source: 327465-2014-05-04.xml*