# A case study on formal analysis of an automated guided vehicle system.

1. IntroductionComplex 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 Section 2, 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. Figure 1 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 [less than or equal to] v(t) [less than or equal to] 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 -[pi] [less than or equal to] [omega](t) [less than or equal to] [pi] 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.

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 maybe 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-tuple [H.sub.M] = ([E.sub.V], [I.sub.V], S, [S.sub.0], [E.sub.A], [I.sub.A], [D.sub.T], T), where

(i) [E.sub.V] is a set of external variables,

(ii) [I.sub.V] is a set of internal variables, and V [??] [E.sub.V] [union] [I.sub.V] is the disjunction that represent all variables,

(iii) S [subset or equal to] val([I.sub.V]) is a set of states,

(iv) [S.sub.0] [subset or equal to] S is a nonempty set of initial states,

(v) [E.sub.A] is a set of external actions,

(vi) [I.sub.A] is a set of internal actions, and A [??] [E.sub.A] [union] [I.sub.A] is the union of [E.sub.A] and [I.sub.A],

(vii) [D.sub.T] [subset or equal to] S x A x S is a set of discrete transitions,

(viii) T is a set of trajectories for V. For every [tau] [member of] T and t [member of] dom([tau]) (domain of [tau]), we have [tau](t)[[I.sub.V] [member of] S, where [tau](t)[[I.sub.v] is the restriction of [tau](t) to [I.sub.v]; that is, the function g with dom(g) = dom([tau]) n IV such that g(t) = [tau](t). We require the following axioms:

(A1) for all [tau] [member of] T ref for all [tau]' [less than or equal to] [tau][tau]' [member of] T;

(A2) for all [tau] [member of] T for all t [member of] dom([tau]) [tau] [??] t [member of] T where [tau] [??] t denotes (([tau][[t, +[infinity])) - t);

(A3) suppose [[tau].sub.0], [[tau].sub.1], [[tau].sub.2], ..., [[tau].sub.i], ... is a sequence of trajectories in T; if [[tau].sub.i] is closed and [[tau].sub.i] x l state = [[tau].sub.i+1] x f state, where i [member of] N, [[tau].sub.i] is not the last trajectory of the hybrid sequence, then [[tau].sub.0] [??] [[tau].sub.1] [??] [[tau].sub.2] ... [member of] T, where [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

The execution fragment of a hybrid automaton is a hybrid sequence [alpha] = [[tau].sub.0][a.sub.1] [[tau].sub.1][a.sub.2], ..., [[tau].sub.i][a.sub.i+1], ..., where [[tau].sub.i] [member of] T, where i is a nonnegative integer and T is defined in Definition 1; and if [[tau].sub.i] is not the last trajectory, then [[tau].sub.i] x l state [??] [[tau].sub.i+1] x f state, where l state represents the last state and /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 [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

3.3. Hybrid I/O Automata. We described thehybridautomata 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-tuple [A.sub.M] = ([H.sub.M], U, Y, I, O), where

(i) [H.sub.M] = (-[E.sub.V], [I.sub.V], S, [s.sub.0], [E.sub.A], [I.sub.A], [D.sub.T], T) is a hybrid automaton,

(ii) U [subset or equal to] [E.sub.V] is a set of input variables,

(iii) Y [??] [E.sub.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 all x [member of] S for all [alpha] [member of] I [there exist]x' [member of] S such that x [??] x',

(A2) let trajs(U) denote the set of all trajectories for U, for all x [member of] S for all [upsilon] [member of] trajs(U) [there exist][tau] [member of] T such that [tau] x f state = x, [tau] [down arrow] U [less than or equal to] v, and either

(a) [tau] [down arrow] U = [upsilon], or

(b) [tau] is closed and some l [member of] L is enabled in [tau] x l state,

where g = [tau] [down arrow] U represents dom(g) = dom([tau]) such that, for all c [member of] dom(g) has g(c) = [tau](c)[U.

We further define

(i) Z [??] [I.sub.V] [union] Y is a set of variables that are locally controlled, and

(ii) L [??] [I.sub.A] [union] 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 [parallel]. For the proof of Theorem 3 and Lemma 4, see [!].

Theorem 3. [A.sub.M1] [parallel] [A.sub.M2] is a hybrid I/O automaton when [A.sub.M1] and [A.sub.M2] are strongly compatible hybrid I/O automata and [U.sub.1] [intersection] [Y.sub.2] = 0.

Another important operation is hiding external variables in HIOA. Suppose [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Lemma 4. If [A.sub.M] is a HIOA and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], then VarHide ([E.sub.V], [A.sub.M]) is a HIOA.

Definition 5 (simulation relations). For all states [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] of [A.sub.M] and [B.sub.M], given two comparable HIOAs, from [A.sub.M] to [B.sub.M] there exists a simulation relation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (denoted as [A.sub.M][R.sub.S][B.sub.M]) when the following three conditions are met:

(i) knowing that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and suppose there exists a state [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the set of initial states of [A.sub.M] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the set of initial states of [B.sub.M];

(ii) suppose [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and an execution fragment of [A.sub.M]; execution fragment [alpha] = [[tau].sub.0][a.sub.1][[tau].sub.1][a.sub.2], ..., [[tau].sub.i][a.sub.i+1], ..., meets [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]; there exists a closed execution fragment [beta] in [B.sub.M] that meets [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and [alpha] x l state R[beta] x l state;

(iii) suppose [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and an execution fragment of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]; there exists a closed execution fragment [beta] in [B.sub.M] that meets [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and [alpha] x l state R[beta] x l state.

Corollary 6. Given two comparable HAs [A.sub.M] and [B.sub.M], and a simulation from [A.sub.M] to [B.sub.M] denoted as [A.sub.M][R.sub.s][B.sub.M], then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

The proof refers to [4]. According to [18,19], we define a bisimulation as follows.

Definition 7 (bisimulation). Given two comparable HIOAs [A.sub.M] and [B.sub.M], for all pairs (p, q) among all reachable states of [A.sub.M] and [B.sub.M], p in [A.sub.M], and q in [B.sub.M]. If all reachable states [p.sup.*] in [A.sub.M] have p [??] [p.sup.*], this implies the existence of a state [q.sup.*] in [B.sub.M] such that p [??] [p.sup.*]. At the same time, all reachable states [q.sup.*] in [B.sub.M] have p [??] [p.sup.*], implying that there exists a state [q.sup.*] in [A.sub.M] such that p [??] [p.sup.*]. Under these circumstances, we say that [A.sub.M] and [B.sub.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 [[theta].sub.1] and [[theta].sub.2] are the angles of the left and right wheels relative to the v-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.

XOY is the global coordinate frame. v is the forward velocity of the car. [t.sub.sample] is the sampling time. [omega] is the angular speed of the vehicle. e(t) is the displacement of the center of the vehicle from the track at time t. [[epsilon].sub.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. [[epsilon].sub.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. [[epsilon].sub.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. [alpha] is the maximum angle of vehicle velocity direction to the tangential direction of the center point on the track, where 0 [less than or equal to] [alpha] [less than or equal to] [pi]/2. [theta] is the angle of the vehicle velocity direction to the x-axis positive direction. [eta] is the angle of the vehicle velocity direction to the tangential direction of the center point on the track, where -[alpha] [less than or equal to] [eta] [less than or equal to] [alpha]. 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, [theta]) where x is the v-coordinate of the center of the vehicle; y is the y-coordinate of the center of the vehicle; and [theta] 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

[eta] [member of] [-[alpha], [alpha]] [conjunction] [absolute value of e (t)] [less than or equal to] [[epsilon].sub.1]. (1)

From Figure 2, the chassis secures the wheels. Hence the left wheels, right wheels, and the chassis have the same angles. We obtain the following algebraic equation:

[[theta].sub.1] = [[theta].sub.2] = [theta]. (2)

4.2. Component LWheel. We model the behavior of left wheels as the hybrid automaton LWheel. The left wheel has external variables: [x.sub.1], which gives the x-coordinate of the left wheel; [y.sub.1], which gives the y-coordinate of the right wheel; and [[theta].sub.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:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (3)

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 the sensor 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:

sensor = e(t) = f (x (t), y (t)). (4)

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 automaton controller, 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:

c = k x t, (5)

where k is the rate of the clock, t is the variable of time, and k = d[c(t)]/dt. In our model, the value of k can be a constant 1.

The controller has a variable e, 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:

c = 0 [conjunction] sample [member of] [-[[epsilon].sub.1], [[epsilon].sub.1]]. (6)

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 signals is_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:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], (7)

where [??] denotes the event trigger.

For trajectories we require that

sample ([t.sub.1]) = sample ([t.sub.2]), (8)

for all time [t.sub.1], [t.sub.2] between clock transitions; that is, [t.sub.1], [t.sub.2] [member of] [m x [t.sub.sample], (m + 1) x [t.sub.sample]) for all m [member of] N.

The new_sample will record the new value from the sensor:

new_sample = e(t). (9)

For every state, the following equations must hold:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (10)

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 displacement e(t) is the function of x and y and that the control logic guards the transitions whether enabled or not. They are as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (11)

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 [[theta].sub.1] and [[theta].sub.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:

Plant = VarHide ({[[theta].sub.1], [[theta].sub.2]}, (Chassis [parallel] LWheel [parallel] RWheel)). (12)

Likewise, the sensor can be regarded as a hybrid I/O automaton, for which the inputs are x 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:

[H.sub.M] = VarHide ({x, y, e, is_stop, l_control, r_control}, (Plant [parallel] Sensor [parallel] Controller)). (13)

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.sub.M]:

[absolute value of sample] [less than or equal to] [[epsilon].sub.3]. (14)

In addition, we hope that the forward mode occurs infinitely often:

GF (c = 0 [conjunction] [absolute value of sample] [less than or equal to] [[epsilon].sub.3]). (15)

In order to simplify the model, we abstract a model [A.sub.M] from the previous model [H.sub.M]. Then, we use model [A.sub.M] instead of [H.sub.M]. We find the constraints we need from model [A.sub.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:

c = 0 [??] [absolute value of e (t)] [less than or equal to] [[epsilon].sub.3]. (16)

We find that the variables new_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 [[phi].sub.forward], [[phi].sub.right], [[phi].sub.left], [[phi].sub.back], and [[phi].sub.stop], respectively; [[phi].sub.step] is the disjunction of the five:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (17)

Now we get the abstract model of the AGV system. Since the abstract model A 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 model [H.sub.M] and the abstract model [A.sub.M] have a bisimulation equivalence relationship.

Lemma 8. Let [S.sub.K] be a set of all reachable states of [H.sub.M], for all s [member of] [S.sub.R]; one has

c = 0 [??] [[absolute value of sample] [less than or equal to] [[epsilon].sub.2] [??] [absolute value of e(t)] [less than or equal to] [[epsilon].sub.2]] (18)

Proof. Use (14) and 15) to prove Lemma 8.

Theorem 9. The two comparable HIOAs [H.sub.M] and [A.sub.M] have a bisimulation relation.

Proof. Owing to the limitation of space, we do not provide a detailed proof of Theorem 9, but the key step will be given. [H.sub.M] and [A.sub.M] satisfy the following condition:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (19)

For all state pairs (p, q) among all reachable states of [H.sub.M] and [A.sub.M], p [member of] [H.sub.M] and q [member of] [A.sub.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.sub.M] bisimulates an initial state of [A.sub.M], and there exists an execution fragment from p to [p.sup.*], where [p.sup.*] in [H.sub.M] has p [right arrow] [p.sup.*], implying the existence of a transition according to the transition predicate [[phi].sub.step] of [A.sub.M] from q to [q.sup.*] in [A.sub.M], such that q [??] [q.sup.*]. At the same time, there exists a transition according to the transition predicate [[phi].sub.step] of [A.sub.M] from q to [q.sup.*], where [q.sup.*] in [A.sub.M] has q [??] [q.sup.*], implying the existence of an execution fragment from p to [p.sup.*], where [p.sup.*] in [H.sub.M], such that p [right arrow] [p.sup.*]. We can then use Definition 5, Corollary 6, and Definition 7 to prove Theorem 9.

5. Correctness

5.1. The Desired Properties of [A.sub.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 [[epsilon].sub.3], and never be less than the threshold -[[epsilon].sub.3]. At the same time, we ensure that [eta] lies in the interval [-[alpha], [alpha]].

Property 1. The vehicle always moves forward and never moves backward. It can be described as

[[phi].sub.safety] [??] [eta] [member of] [-[alpha], [alpha]] [conjunction] [absolute value of e(t)] [less than or equal to] [[epsilon].sub.3]. (20)

Property 2. The vehicle moves forward infinitely often. It can be described using the temporal logic formula

[[phi].sub.fairness] [??] GF [absolute value of e(t)] [less than or equal to] [[epsilon].sub.1]. (21)

Lemma 10. If [[phi].sub.safety] is an invariant of [A.sub.M] and formula [[phi].sub.fairness] holds for [A.sub.M], then (14) is an invariant of [H.sub.M] and (15) holds for [H.sub.M].

Proof. Use Lemma 8, 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

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (22)

Theorem 11. If [[phi].sub.1], [[phi].sub.2], and [[phi].sub.3] are met, then the [[phi].sub.safety] property is an invariant of [A.sub.M]; that is,

[[phi].sub.safety] [conjunction] [[phi].sub.1] [conjunction] [[phi].sub.2] [conjunction] [[phi].sub.3] [??] [[phi].sup.*.sub.safety]. (23)

Proof. In the first step, we prove that [[phi].sub.safety] [conjunction] [[phi].sub.1] [??] 0 [less than or equal to] [e.sup.*](t) [less than or equal to] [[epsilon].sub.3] holds. Since the circle is symmetrical, we only need to consider the situation of the first quadrant. In order to guarantee that [absolute value of e(t)] [less than or equal to] [[epsilon].sub.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) [less than or equal to] [[epsilon].sub.2]. The vehicle then moves forward to B with [eta] = [alpha] at the next sampling; the e(t) reaches the largest displacement. We use [[phi].sub.1] to illustrate that 0 < e(t) [less than or equal to] [[epsilon].sub.3] holds for [A.sub.M]. The derivations in (24) show that [e.sup.*] (t) [less than or equal to] [[epsilon].sub.3].

Deriving from [[phi].sub.1]. Consider the following:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (24)

Since the vehicle moves on the outside of the circle, e[(t).sup.*] > 0. Therefore, [[phi].sub.safety] [conjunction] [[phi].sub.1] [??] 0 < [e.sup.*](t) [less than or equal to] [[epsilon].sup.3].

In the second step, we prove that [[phi].sub.safety] [conjunction] [[phi].sub.2] [??] -[[epsilon].sub.3] [less than or equal to] [e.sup.*](t) [less than or equal to] 0 holds. In order to guarantee that [absolute value of e(t)] [less than or equal to] [[epsilon].sub.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) > -[[epsilon].sub.2], and then moves forward to B with [eta] = -[alpha] at the next sampling, where the vehicle reaches the farthest to the track. We use [[phi].sub.2] to illustrate that -[[phi].sub.3] [less than or equal to] e(t) < 0 holds for [A.sub.M]. The derivations in (25) show that [e.sup.*](t) [greater than or equal to] -[[epsilon].sub.3].

Deriving from [[phi].sub.2]. Consider the following:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (25)

Since the vehicle moves on the inside of the circle, [e.sup.*](t) < 0. Therefore, [[phi].sub.safety] [conjunction] [[phi].sub.2] [??] -[[epsilon].sub.3] [less than or equal to] [e.sup.*](t) [less than or equal to] 0.

In the third step, we prove that [[phi].sub.safety] [conjunction] [[phi].sub.3] [??] [[eta].sup.*] [member of] [- [alpha], [alpha]] holds. Constraint [omega][t.sub.sample] [less than or equal to] [alpha] is required to guarantee that [eta] is always in the interval [-[alpha], [alpha]]. 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 [eta] < 0 (the angle between [??] and [??]), relative to the coordinate frame X'O'Y', is [[eta].sup.*] = [eta] + [omega][t.sub.sample] < [omega][t.sub.sample] at the next sampling. If [omega][t.sub.sample] [less than or equal to] [alpha], then [[eta].sup.*] = [eta] + [omega][t.sub.sample] < [alpha]. If the vehicle reaches point C in the current sampling, the vehicle will steer to the left. The angle [eta] > 0 (the angle between [??] and [??]), relative to the coordinate frame X'O'Y', is [[eta].sup.*] = [eta] - [omega][t.sub.sample] > -[omega][t.sub.sample] at the next sampling. If [omega][t.sub.sample] [less than or equal to] [alpha], then -[omega][t.sub.sample] [greater than or equal to] -[alpha], and we will get [[eta].sup.*] = [eta] - [omega]t[s.sub.ample] > -[alpha]. We have proved that [[eta].sup.*] [member of] [-[alpha], [alpha]].

Therefore, [[phi].sub.safety] [conjunction] [[phi].sub.1] [conjunction] [[phi].sub.2] [conjunction] [[phi].sub.3] [??] [[phi].sup.*.sub.safety] is proved.

Theorem 12. If [[phi].sub.4] holds for [A.sub.M], then the property of [[phi].sub.fairness] is an invariance of [A.sub.M]; that: is [[phi].sub.fairness] [conjunction] [[phi].sub.4] [??] [[phi].sup.*.sub.fairness]

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 Figure 6. The center of the vehicle is very close to point A in the current sampling, and e(t) < [[epsilon].sub.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 [??], and we look at [??] as a straight line AB. Suppose that [eta] = [alpha], e(t) < [[epsilon].sub.1] at the next sampling and that the vehicle switches to the forward mode. From [[phi].sub.4], we can derive the following:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (26)

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:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (27)

We assume that the value range of v is from [v.sub.min] to [v.sub.max], [t.sub.sample] is from [t.sub.min] to [t.sub.max], [alpha] is from "min to [[alpha].sub.max], [[epsilon].sub.1] is from [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to is from [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] 2 to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is from [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], R is from [R.sub.min] to [R.sub.max], and w is from [[omega].sub.min] to [[omega].sub.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:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (28)

It is obvious that the parameters [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and [[omega].sub.min] do not appear in the constraint inequalities. Therefore, we increase [[epsilon].sub.1] and [[epsilon].sub.3] from the minimum and decrease [omega] from the maximum. We do not know the exact values of such parameters as v, [t.sub.sample], [omega], 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 [[phi].sub.safety] as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (29)

Parameters v and [omega] 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.

http://dx.doi.org/10.1155/2014/327465

Conflict of Interests

The authors declare that there is no conflict of interests regarding the publication of this paper.

Acknowledgments

The research for this study was supported by the NSFC (61373034,61170304) and the International S&T Cooperation Program of China (2011DFG13000) (KZ201210028036).

References

[1] M. S. Branicky, "Introduction to hybrid systems," in Handbook of Networked and Embedded Control Systems, D. Hristu-Varsakelis and W. S. Levine, Eds., Control Engineering, pp. 91-116, Birkhauser Boston, Boston, Mass, USA, 2005.

[2] A. Fehnker, F. Vaandrager, and M. Zhang, "Modeling and verifying a Lego car using hybrid I/O automata," in Proceedings of the 3rd International Conference on Quality Software (QSIC '03), pp. 280-289, IEEE Computer Society, 2003.

[3] L. Balbis, A. W. Ordys, M. J. Grimble, and Y. Pang, "Tutorial introduction to the modelling and control of hybrid systems," International Journal of Modelling, Identification and Control, vol. 2, no. 4, pp. 259-272, 2007

[4] N. Lynch, R. Segala, and F. Vaandrager, "Hybrid I/O automata," Information and Computation, vol. 185, no. 1, pp. 105-157, 2003.

[5] T. A. Henzinger, "Theory of hybrid automata," in Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS '96), pp. 278-292, IEEE Computer Society, July 1996.

[6] J. Lygeros, G. Pappas, and S. Sastry, "An introduction to hybrid systems modeling, analysis and control," in Proceedings of the 1st Nonlinear Control Network Pedagogical School, pp. 307-329, Athens, Greece, 1999.

[7] A. Balluchi, L. Benvenuti, M. D. D. I. Benedetto, S. Member, C. Pinello, and A. Luigi, "Automotive engine control and hybrid systems: challenges and opportunities," Proceedings of the IEEE, vol. 88, no. 7, pp. 888-912, 2000.

[8] R. Alur, R. Grosu, Y. Hur, V. Kumar, and I. Lee, "Modular specification of hybrid systems in charon," in Hybrid Systems: Computation and Control, N. Lynch and B. Krogh, Eds., vol. 1790 of Lecture Notes in Computer Science, pp. 6-19, Springer, Berlin, Germany, 2000.

[9] M. Song, T. Tarn, and N. Xi, "Integration of task scheduling, action planning, and control in robotic manufacturing systems," Proceedings of the IEEE, vol. 88, no. 7, pp. 1097-1107, 2000.

[10] M. Katara, "Hybrid models for mobile computing," in Coordination Languages and Models, A. Porto and G. C. Roman, Eds., vol. 1906 of Lecture Notes in Computer Science, pp. 216-231, Springer, Berlin, Germany, 2000.

[11] B. Lennartson, M. Tittus, B. Egardt, and S. Pettersson, "Hybrid systems in process control," IEEE Control Systems Magazine, vol. 16, no. 5, pp. 45-56, 1996.

[12] N. A. Lynch and M. R. Tuttle, "An introduction to input/output automata," CWI Quarterly, vol. 2, no. 3, pp. 219-246, 1989.

[13] T. Muller, Automated Guided Vehicles, IFS, Kempston, UK, 1983.

[14] T. Le-Anh and M. B. M. de Koster, "A review of design and control of automated guided vehicle systems," European Journal of Operational Research, vol. 171, no. 1, pp. 1-23, 2006.

[15] I. F. A. Vis, "Survey of research in the design and control of automated guided vehicle systems," European Journal of Operational Research, vol. 170, no. 3, pp. 677-709, 2006.

[16] W. Kang, N. Xi, and J. Tan, "Analysis and design of non-time based motion controller for mobile robots," in Proceedings of the IEEE International Conference on Robotics and Automation (ICRA '99), pp. 2964-2969, May 1999.

[17] J. Tan, N. Xi, and W. Kang, "Non-time based tracking controller for mobile robots," in Proceedings of the 1999 IEEE Canadian Conference on Electrical and Computer Engineering, pp. 919-924, May 1999.

[18] R. Milner, Communication and Concurrency, Prentice-Hall, 1989.

[19] D. Park, "Concurrency and automata on infinite sequences," in Theoretical Computer Science, P. Deussen, Ed., vol. 104 of Lecture Notes in Computer Science, pp. 167-183, Springer, Berlin, Germany, 1981.

Jie Zhang, (1,2) Yuntao Peng, (1) William N. N. Hung, (3) Xiaojuan Li, (4) Jindong Tan, (2) and Zhiping Shi (4)

(1) College of Information Science and Technology, Beijing University of Chemical Technology, Beijing, China

(2) University of Tennessee, Knoxville, TN, USA

(3) Synopsys Inc., Mountain View, CA, USA

(4) Beijing Engineering Research Center of High Reliable Embedded System, College of Information Engineering,

Capital Normal University, Beijing, China

Correspondence should be addressed to Jie Zhang; jzhang@mail.buct.edu.cn

Received 6 March 2014; Accepted 30 March 2014; Published 4 May 2014

Academic Editor: Xiaoyu Song

Printer friendly Cite/link Email Feedback | |

Title Annotation: | Research Article |
---|---|

Author: | Zhang, Jie; Peng, Yuntao; Hung, William N.N.; Li, Xiaojuan; Tan, Jindong; Shi, Zhiping |

Publication: | Journal of Applied Mathematics |

Article Type: | Report |

Date: | Jan 1, 2014 |

Words: | 7225 |

Previous Article: | Model and topological characteristics of power distribution system security region. |

Next Article: | Generalized fuzzy Shapley function for fuzzy games. |

Topics: |