# Modeling and Analysis of the Obstacle-Avoidance Strategies for a Mobile Robot in a Dynamic Environment

Authors: Rui Wang; Ming Wang; Yong Guan; Xiaojuan Li
Journal: Mathematical Problems in Engineering
 (2015)

---

## Abstract

Obstacle avoidance is a key performance of mobile robots. However, its experimental verification is rather difficult, due to the probabilistic behaviors of both the robots and the obstacles. This paper presents the Markov Decision Process based probabilistic formal models for three obstacle-avoidance strategies of a mobile robot in an uncertain dynamic environment. The models are employed to make analyses in PRISM, and the correctness of the analysis results is verified by MATLAB simulations. Finally, the minimum time and the energy consumption are determined by further analyses in PRISM, which prove to be useful in finding the optimal strategy. The present work provides a foundation for the probabilistic formal verification of more complicated obstacle-avoidance strategies.


---

## Body

## 1. Introduction

Obstacle avoidance is a key technique for the design and applications of mobile robots, because static barriers and even dynamic obstacles frequently exist in their paths. When several robots move in the same region, they act in fact as obstacles to one another themselves [1, 2]. Therefore, studies on obstacle avoidance have become an active topic in the field of mobile robots, and a series of strategies have been proposed to realize the avoidance of static and/or dynamic obstacles [2–5]. In the above references, the dynamic environments of the mobile robots are known in advance, because the obstacles are assumed to have predefined moving behaviors. However, mobile robots occasionally have to work in uncertain circumstances, where the movements of the obstacles cannot be predicted accurately [6, 7]. Besides, the sensor and actuator noises, the time delay of network, and other factors may still lead to inaccurate operations of the robots themselves [8]. Due to these reasons, probability-based obstacle-avoidance algorithms have been put forward in recent years [9–11], which models both the movements of the obstacles and the operations of the robots as probabilistic events.The correctness of obstacle-avoidance algorithm is very important. Testing has been the most frequently used method in the performance validation of robots, but it is by no means the best way [12]. Its deficiencies mainly lie in two aspects: (1) the testing results are incomplete, because only a subset of all the possible cases can be examined by physical experiments or software simulations; (2) the testing results are generally small-sample data that are unsuitable for probabilistic analysis.Formal verification [13] is a useful alternative method to physical experiments and software simulations, because it is not only complete in logic but also adaptable for the description and analysis of probabilistic events [14–16]. For example, probabilistic model checking (PMC) is a probability-based formal verification method widely used in the performance validation of software and hardware [17, 18]. There are three main steps involved in PMC. First, a mathematical model is built to incorporate all the possible probabilistic behaviors; second, Probabilistic Computation Tree Logic (PCTL) formulae [19] are derived to describe the key logical requirements; third, a software tool such as PRISM [20] is employed to check whether the mathematical model satisfies the logical requirements or not. If all the requirements are fully satisfied, the probabilistic behaviors are validated. Otherwise, it implies that some errors may exist in the original model. In recent years, formal verification has been widely used to verify the path planning of mobile robots. However, PMC has been scarcely applied in validating the obstacle-avoidance strategies.The purpose of the present paper is to verify three avoidance algorithms that involve a mobile robot and a single dynamic obstacle [9]. The paths of the robot and obstacle cross each other, and their movements have the properties of Markov Decision Processes (MDPs) [21, 22]. The probabilistic models and the PCTL formulae are first built, and then the PRISM software is employed to make analyses on the three avoidance strategies. Both the time and the energy requirements for the robot to reach the destination have been obtained, and the time or energy based optimal condition is thereby applied to help find the optimal obstacle-avoidance strategy under diverse circumstances. In addition, simulations are also made in MATLAB to verify the correctness of the results obtained by PRISM. To this end, the time of obstacle-avoidance output by PRISM is taken as the input of MATLAB.The rest of the paper is organized as follows. Section2 introduces the necessary preliminaries. In Section 3, we formulate the obstacle-avoidance algorithms. Then, the MDPs are constructed in Section 4, and the verification on the algorithm is made in Section 5. Finally, conclusions are presented in Section 6.


## 2. Preliminaries

### 2.1. Markov Decision Process

A Markov Decision Process (MDP) is generally defined as a multituple [18]. In the present work, a five-tuple, (S,S0,Acts,Steps,Cost), is adopted to describe the probabilistic model, where(1)
S represents a group of states,(2)
S0 is the initial state and it belongs to S,(3)
Acts stand for a set of actions, each of which has its own probability,(4)
Steps are the state transition functions,(5)
Cost is a reward function that describes quantitative information of the model.Figure1 shows the schematic diagram of a simple MDP, where p1, p2, p3, p4, and p5 are the probabilities of the corresponding actions, S={S0,S1,S2,S3}, S0=S0, Acts(S0)={A}, Acts(S1)={B,C}, Acts(S2)={D}, Acts(S3)={E}, and the four state transition functions are (1)StepsS0=A,S1⟶p1,StepsS1=B,S0⟶p2,S1⟶1-p2,C,S2⟶p3,S3⟶1-p3,StepsS2=D,S2⟶p4,StepsS3=E,S0⟶p5,S3⟶1-p5.Figure 1
Schematic diagram of a simple MDP.In addition, the reward function “Cost” only describes quantitative information that can be calculated somehow but is generally difficult to be shown in the schematic diagram.


### 2.2. Probabilistic Computation Tree Logic

Probabilistic Computation Tree Logic (PCTL) is an extension of the nonprobabilistic Computation Tree Logic (CTL), which expresses the qualitative properties of the probabilistic models [19]. Generally, a PCTL is expressed as a formula that connects the properties of the MDP using the Boolean operators (such as ¬ (negation) and ∧ (conjunction)), the temporal operators (such as X (next), U (until), F (future), and G (globally)), the probabilistic operator P, and a reward (or cost) operator R.A PCTL formula can be used to calculate a certain quantity of the MDP such as the maximum probability and the minimum time (or energy) consumption. For example, using the following formula(2)Pmax⁡=?Fspec1∧spec2,one can compute the maximum probability of a state that satisfies both the two specifications spec1 and spec2.Again, the following formula can be used to find the minimum cost of energy when the specification spec3 is satisfied:(3)R“energy”min⁡=?Fspec3.Finally, consider another PCTL formula(4)Pmax⁡=?spec4∧¬spec5Uspec6.Obviously, it can be used to calculate the maximum probability of a state, which meets the two requirements spec4 and spec6 but does not satisfy spec5.


## 2.1. Markov Decision Process

A Markov Decision Process (MDP) is generally defined as a multituple [18]. In the present work, a five-tuple, (S,S0,Acts,Steps,Cost), is adopted to describe the probabilistic model, where(1)
S represents a group of states,(2)
S0 is the initial state and it belongs to S,(3)
Acts stand for a set of actions, each of which has its own probability,(4)
Steps are the state transition functions,(5)
Cost is a reward function that describes quantitative information of the model.Figure1 shows the schematic diagram of a simple MDP, where p1, p2, p3, p4, and p5 are the probabilities of the corresponding actions, S={S0,S1,S2,S3}, S0=S0, Acts(S0)={A}, Acts(S1)={B,C}, Acts(S2)={D}, Acts(S3)={E}, and the four state transition functions are (1)StepsS0=A,S1⟶p1,StepsS1=B,S0⟶p2,S1⟶1-p2,C,S2⟶p3,S3⟶1-p3,StepsS2=D,S2⟶p4,StepsS3=E,S0⟶p5,S3⟶1-p5.Figure 1
Schematic diagram of a simple MDP.In addition, the reward function “Cost” only describes quantitative information that can be calculated somehow but is generally difficult to be shown in the schematic diagram.


## 2.2. Probabilistic Computation Tree Logic

Probabilistic Computation Tree Logic (PCTL) is an extension of the nonprobabilistic Computation Tree Logic (CTL), which expresses the qualitative properties of the probabilistic models [19]. Generally, a PCTL is expressed as a formula that connects the properties of the MDP using the Boolean operators (such as ¬ (negation) and ∧ (conjunction)), the temporal operators (such as X (next), U (until), F (future), and G (globally)), the probabilistic operator P, and a reward (or cost) operator R.A PCTL formula can be used to calculate a certain quantity of the MDP such as the maximum probability and the minimum time (or energy) consumption. For example, using the following formula(2)Pmax⁡=?Fspec1∧spec2,one can compute the maximum probability of a state that satisfies both the two specifications spec1 and spec2.Again, the following formula can be used to find the minimum cost of energy when the specification spec3 is satisfied:(3)R“energy”min⁡=?Fspec3.Finally, consider another PCTL formula(4)Pmax⁡=?spec4∧¬spec5Uspec6.Obviously, it can be used to calculate the maximum probability of a state, which meets the two requirements spec4 and spec6 but does not satisfy spec5.


## 3. Obstacle-Avoidance Algorithms

### 3.1. Probabilistic Model of a Dynamic Obstacle

Divide the whole moving process of the dynamic obstacle inton steps, each of which has the same time interval ΔT. Assume that the dynamic obstacle has a stepwise uniform motion; that is, it has different velocity at different time step. In the whole process of movement, its minimum and maximum velocities are denoted by Vmin⁡ and Vmax⁡. Then, the probability density function p(x;k) for the obstacle to reach the position x after k steps can be expressed as [9] (5)px;k=12πσ2exp⁡-x-μ22σ2,where(6)σ2=σ02+kσstep2;μ=x0+kV-ΔT;σstep2=Vmax⁡-Vmin⁡212.Here,x0, σ02, and V- are the initial position, variance, and average velocity, respectively. Integrating p(x;k) along the practical path of the obstacle, one can obtain the probability of reaching the position x.


### 3.2. Obstacle-Avoidance Strategies of a Mobile Robot

Here, three obstacle-avoidance strategies are given for a mobile robot with only a single dynamic obstacle. As shown in Figure2, the former and the latter are represented by a circle and a square, respectively.Figure 2
The paths of a mobile robot and a dynamic obstacle.Assume that the paths of the robot and the obstacle intersect at regionC with angle θ(0°<θ<180°) (see Figure 2). O1 and R1 represent their locations when they begin to enter region C, while O2 and R2 stand for those when they just leave such a region completely. R0 is a reference position of the robot, which can be specified at an arbitrary point not over R1. O0 and O3 are two reference positions of the obstacle to be determined in subsequent derivation. R3 is an undetermined position of the robot.Under this condition, we mainly consider three avoidance strategies: Acceleration, Deceleration, and Detour. In the Acceleration mode, the robot goes across regionC earlier than the obstacle does by enhancing its velocity; in the Deceleration one, it passes region C later than the obstacle does by decreasing its velocity; in the Detour one, it realizes obstacle avoidance by changing its moving direction as shown in Figure 3, where α is the rotation angle and γ is the rotation radius. When α and γ are given, the robot may go along either R0_R4 or R0_R5, due to its probabilistic behavior. Here, R0_R4 represents the expected Detour path, while R0_R5 denotes the unexpected one. In Figure 3, O4 represents the position where the obstacle begins to enter the path intersection region in the expected Detour mode.Figure 3
The detour strategy.However, how to choose one of these three strategies under a specific circumstance is still a problem that needs to be solved. Here, the concept of Dangerous Region is introduced to help explain the decision-making process of the robot. If the obstacle stays in such a region at the initial time, the robot has to choose a certain strategy to avoid collision.To describe such a concept, one needs to make the following three parameters clear at first.(a)
Reference positionO0: when the two paths are given, the position of O1 is fixed (see Figure 2). Therefore, the point O0 can be determined by the distance Din, which is defined as [9](7)Din=DrVr2+Vmax⁡2-VrVmax⁡cos⁡θVr2+Vmax⁡Vr,whereVr is the initial velocity of the robot and Dr is the distance between R1 and R2.(b)
Timetr: tr=Dr/Vr.(c)
Reference positionO3: it is defined in such a way that the obstacle can take less time than tr to go from it to O2 with the velocity Vmin⁡.Then, we name the region betweenO0 and O3 as the Dangerous Region. Note: the distance between O0 and O3 is less than that between O0 and O2.


## 3.1. Probabilistic Model of a Dynamic Obstacle

Divide the whole moving process of the dynamic obstacle inton steps, each of which has the same time interval ΔT. Assume that the dynamic obstacle has a stepwise uniform motion; that is, it has different velocity at different time step. In the whole process of movement, its minimum and maximum velocities are denoted by Vmin⁡ and Vmax⁡. Then, the probability density function p(x;k) for the obstacle to reach the position x after k steps can be expressed as [9] (5)px;k=12πσ2exp⁡-x-μ22σ2,where(6)σ2=σ02+kσstep2;μ=x0+kV-ΔT;σstep2=Vmax⁡-Vmin⁡212.Here,x0, σ02, and V- are the initial position, variance, and average velocity, respectively. Integrating p(x;k) along the practical path of the obstacle, one can obtain the probability of reaching the position x.


## 3.2. Obstacle-Avoidance Strategies of a Mobile Robot

Here, three obstacle-avoidance strategies are given for a mobile robot with only a single dynamic obstacle. As shown in Figure2, the former and the latter are represented by a circle and a square, respectively.Figure 2
The paths of a mobile robot and a dynamic obstacle.Assume that the paths of the robot and the obstacle intersect at regionC with angle θ(0°<θ<180°) (see Figure 2). O1 and R1 represent their locations when they begin to enter region C, while O2 and R2 stand for those when they just leave such a region completely. R0 is a reference position of the robot, which can be specified at an arbitrary point not over R1. O0 and O3 are two reference positions of the obstacle to be determined in subsequent derivation. R3 is an undetermined position of the robot.Under this condition, we mainly consider three avoidance strategies: Acceleration, Deceleration, and Detour. In the Acceleration mode, the robot goes across regionC earlier than the obstacle does by enhancing its velocity; in the Deceleration one, it passes region C later than the obstacle does by decreasing its velocity; in the Detour one, it realizes obstacle avoidance by changing its moving direction as shown in Figure 3, where α is the rotation angle and γ is the rotation radius. When α and γ are given, the robot may go along either R0_R4 or R0_R5, due to its probabilistic behavior. Here, R0_R4 represents the expected Detour path, while R0_R5 denotes the unexpected one. In Figure 3, O4 represents the position where the obstacle begins to enter the path intersection region in the expected Detour mode.Figure 3
The detour strategy.However, how to choose one of these three strategies under a specific circumstance is still a problem that needs to be solved. Here, the concept of Dangerous Region is introduced to help explain the decision-making process of the robot. If the obstacle stays in such a region at the initial time, the robot has to choose a certain strategy to avoid collision.To describe such a concept, one needs to make the following three parameters clear at first.(a)
Reference positionO0: when the two paths are given, the position of O1 is fixed (see Figure 2). Therefore, the point O0 can be determined by the distance Din, which is defined as [9](7)Din=DrVr2+Vmax⁡2-VrVmax⁡cos⁡θVr2+Vmax⁡Vr,whereVr is the initial velocity of the robot and Dr is the distance between R1 and R2.(b)
Timetr: tr=Dr/Vr.(c)
Reference positionO3: it is defined in such a way that the obstacle can take less time than tr to go from it to O2 with the velocity Vmin⁡.Then, we name the region betweenO0 and O3 as the Dangerous Region. Note: the distance between O0 and O3 is less than that between O0 and O2.


## 4. Construction of MDPs

This section gives the MDP models for both the obstacle and the robot. The model symbols are shown in Symbol Description.


### 4.1. Formal Model of the Dynamic Obstacle

Assume that the dynamic obstacle moves along its path from the initial positionOS to the terminal one OE. In this process, it passes the locations O0, O1, O3, O2, and O4 in turn. Under this condition, its movement is divided into seven states, and then its formal model is constructed as shown in Figure 4. According to the obstacle-avoidance strategies, O0_O3 is the Dangerous Region. Therefore, if the obstacle is in the state SO0_O1 or SO1_O3, the robot should choose a strategy to avoid collision.Figure 4
Formal model of the dynamic obstacle.To help understand the model, three typical state transitions are explained as follows:(1)
SOS_O0→To<TOS_O0SOS_O0.When the timerTo is less than TOS_O0, the obstacle is in the state SOS_O0; that is, the obstacle is moving in the region OS_O0.(2)
SOS_O0→To=TOS_O0;To≔0SO0_O1.WhenTo becomes equal to TOS_O0, the obstacle switches to the state SO0_O1 from the state SOS_O0; that is, the obstacle moves into the region O0_O1 from the region OS_O0, and then the timer To is reset to 0.(3)
SOE_OE→SOE_OE.The obstacle stays in the stateSOE_OE and will not switch to other states; that is, the obstacle reaches its terminal position.Dividing each region in Figure4 into some equal steps in time, one can compute the probability for the obstacle to reach the position x by integrating the probability density function px;k in (5).


### 4.2. Formal Model of the Mobile Robot

This section provides the formal representation for the state transitions of the robot (see Figures5–7). In the description, we assume that each avoidance strategy can be executed by the robot with a certain probability. Specifically, when the robot takes the “Detour” operation, it can rotate to the expected angle with probabilityp1, as a result of the wheel slippage and other factors; if the robot selects the action “Acceleration” or “Deceleration,” the probability of changing its velocity to the expected value is p2 or p3, because of the actuator error and other uncertainties.Figure 5
Formal model of the Detour strategy.Figure 6
Formal model of the Acceleration strategy.Figure 7
Formal model of the Deceleration strategy.


#### 4.2.1. Detour Strategy

The mobile robot moves from its initial positionRS to the reference one R0 and then takes the detour strategy to avoid the obstacle. If the robot rotates to the expected angle, it can move into the desired region R0_R4 successfully (see Figure 3). Otherwise, it may go into another arbitrary region such as R0_R5 (see Figure 3). As stated above, it rotates to the expected angle with probability p1. Therefore, the robot can go into R0_R4 with probability p1, while it will deviate into R0_R5 with probability 1-p1. In the former case, the collision will be effectively avoided and the robot can go to its terminal RE safely, because the detour operation is successful. However, in the latter case, whether the robot will collide with the obstacle or not is still uncertain. If the collision is avoided, the robot will also go to RE successfully. Otherwise, the collision will make the detour operation fail.To help understand the model, four typical state transitions are explained as follows:(1)
SRS_R0→p1,Tr=TRS_R0&Safe=0SR0_R4.When the mobile robot is in the stateSRS_R0 and the value of Safe is equal to 0 (i.e., the obstacle is in the Dangerous Region), the robot will take the detour strategy to switch to the state SR0_R4. The detour operation can be successfully made with probability p1.(2)
SRS_R0→1-p1,Tr=TRS_R0&Safe=0SR0_R5.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot will switch to the state SE0_R5 with probability (1-p1).(3)
SR0_R5→Conflict=1;Tr≔0Collision.When the robot is in the stateSR0_R5 and the value of Conflict is equal to 1 (i.e., the robot collides with the obstacle), the robot will switch to the Collision state.(4)
Collision→Collision.The robot will stay in the Collision state and stop moving.


#### 4.2.2. Acceleration Strategy

If the robot locating atR0 takes the Acceleration strategy to avoid collision, it will move to R2 by enhancing its velocity. As stated above, the probability of increasing its velocity to the expected value is p2. Therefore, it can reach R2 with probability p2 and then go to the terminal RE safely. In this strategy, it is easy to infer that the change of velocity will fail with probability 1-p2. When the desired velocity is not obtained, whether the robot will collide with the obstacle or not is uncertain. If the collision is avoided, the robot will also go to RE successfully.Two typical state transitions are explained as follows:(1)
SRS_R0→p2,Tr=TRS_R0&Safe=0SR0_R2.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Acceleration action. Its state switches from SRS_R0 to SR0_R2 with probability p2.(2)
SRS_R0→1-p2,Tr=TRS_R0&Safe=0SER0_R2.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Acceleration action. Its state will change from SRS_R0 to SER0_R2 with probability (1-p2), because the Acceleration action will fail with probability (1-p2).


#### 4.2.3. Deceleration Strategy

If the robot locating atR0 takes the Deceleration strategy to avoid collision, it will move to a certain position R5 between R0 and R1 by reducing its velocity. As stated above, the probability of decreasing its velocity to the expected value is p3. Therefore, it can reach R5 with probability p3 and then go to the terminal RE safely. Obviously, the change of velocity will fail with probability 1-p3. When the desired velocity is not obtained, whether the robot will collide with the obstacle or not is uncertain. If the collision is avoided, the robot will also go to RE successfully.Two typical state transitions are as follows:(1)
SRS_R0→p3,Tr=TSRS_R0&Safe=0SR0_R3.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Deceleration action. Its state switches from SRS_R0 to SR0_R3 with probability p3.(2)
SRS_R0→1-p3,Tr=SRS_R0&Safe=0SER0_R3.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Deceleration action. Its state will change from SRS_R0 to SER0_R3 with probability (1-p3), because the Deceleration action will fail with probability (1-p3).


## 4.1. Formal Model of the Dynamic Obstacle

Assume that the dynamic obstacle moves along its path from the initial positionOS to the terminal one OE. In this process, it passes the locations O0, O1, O3, O2, and O4 in turn. Under this condition, its movement is divided into seven states, and then its formal model is constructed as shown in Figure 4. According to the obstacle-avoidance strategies, O0_O3 is the Dangerous Region. Therefore, if the obstacle is in the state SO0_O1 or SO1_O3, the robot should choose a strategy to avoid collision.Figure 4
Formal model of the dynamic obstacle.To help understand the model, three typical state transitions are explained as follows:(1)
SOS_O0→To<TOS_O0SOS_O0.When the timerTo is less than TOS_O0, the obstacle is in the state SOS_O0; that is, the obstacle is moving in the region OS_O0.(2)
SOS_O0→To=TOS_O0;To≔0SO0_O1.WhenTo becomes equal to TOS_O0, the obstacle switches to the state SO0_O1 from the state SOS_O0; that is, the obstacle moves into the region O0_O1 from the region OS_O0, and then the timer To is reset to 0.(3)
SOE_OE→SOE_OE.The obstacle stays in the stateSOE_OE and will not switch to other states; that is, the obstacle reaches its terminal position.Dividing each region in Figure4 into some equal steps in time, one can compute the probability for the obstacle to reach the position x by integrating the probability density function px;k in (5).


## 4.2. Formal Model of the Mobile Robot

This section provides the formal representation for the state transitions of the robot (see Figures5–7). In the description, we assume that each avoidance strategy can be executed by the robot with a certain probability. Specifically, when the robot takes the “Detour” operation, it can rotate to the expected angle with probabilityp1, as a result of the wheel slippage and other factors; if the robot selects the action “Acceleration” or “Deceleration,” the probability of changing its velocity to the expected value is p2 or p3, because of the actuator error and other uncertainties.Figure 5
Formal model of the Detour strategy.Figure 6
Formal model of the Acceleration strategy.Figure 7
Formal model of the Deceleration strategy.


### 4.2.1. Detour Strategy

The mobile robot moves from its initial positionRS to the reference one R0 and then takes the detour strategy to avoid the obstacle. If the robot rotates to the expected angle, it can move into the desired region R0_R4 successfully (see Figure 3). Otherwise, it may go into another arbitrary region such as R0_R5 (see Figure 3). As stated above, it rotates to the expected angle with probability p1. Therefore, the robot can go into R0_R4 with probability p1, while it will deviate into R0_R5 with probability 1-p1. In the former case, the collision will be effectively avoided and the robot can go to its terminal RE safely, because the detour operation is successful. However, in the latter case, whether the robot will collide with the obstacle or not is still uncertain. If the collision is avoided, the robot will also go to RE successfully. Otherwise, the collision will make the detour operation fail.To help understand the model, four typical state transitions are explained as follows:(1)
SRS_R0→p1,Tr=TRS_R0&Safe=0SR0_R4.When the mobile robot is in the stateSRS_R0 and the value of Safe is equal to 0 (i.e., the obstacle is in the Dangerous Region), the robot will take the detour strategy to switch to the state SR0_R4. The detour operation can be successfully made with probability p1.(2)
SRS_R0→1-p1,Tr=TRS_R0&Safe=0SR0_R5.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot will switch to the state SE0_R5 with probability (1-p1).(3)
SR0_R5→Conflict=1;Tr≔0Collision.When the robot is in the stateSR0_R5 and the value of Conflict is equal to 1 (i.e., the robot collides with the obstacle), the robot will switch to the Collision state.(4)
Collision→Collision.The robot will stay in the Collision state and stop moving.


### 4.2.2. Acceleration Strategy

If the robot locating atR0 takes the Acceleration strategy to avoid collision, it will move to R2 by enhancing its velocity. As stated above, the probability of increasing its velocity to the expected value is p2. Therefore, it can reach R2 with probability p2 and then go to the terminal RE safely. In this strategy, it is easy to infer that the change of velocity will fail with probability 1-p2. When the desired velocity is not obtained, whether the robot will collide with the obstacle or not is uncertain. If the collision is avoided, the robot will also go to RE successfully.Two typical state transitions are explained as follows:(1)
SRS_R0→p2,Tr=TRS_R0&Safe=0SR0_R2.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Acceleration action. Its state switches from SRS_R0 to SR0_R2 with probability p2.(2)
SRS_R0→1-p2,Tr=TRS_R0&Safe=0SER0_R2.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Acceleration action. Its state will change from SRS_R0 to SER0_R2 with probability (1-p2), because the Acceleration action will fail with probability (1-p2).


### 4.2.3. Deceleration Strategy

If the robot locating atR0 takes the Deceleration strategy to avoid collision, it will move to a certain position R5 between R0 and R1 by reducing its velocity. As stated above, the probability of decreasing its velocity to the expected value is p3. Therefore, it can reach R5 with probability p3 and then go to the terminal RE safely. Obviously, the change of velocity will fail with probability 1-p3. When the desired velocity is not obtained, whether the robot will collide with the obstacle or not is uncertain. If the collision is avoided, the robot will also go to RE successfully.Two typical state transitions are as follows:(1)
SRS_R0→p3,Tr=TSRS_R0&Safe=0SR0_R3.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Deceleration action. Its state switches from SRS_R0 to SR0_R3 with probability p3.(2)
SRS_R0→1-p3,Tr=SRS_R0&Safe=0SER0_R3.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Deceleration action. Its state will change from SRS_R0 to SER0_R3 with probability (1-p3), because the Deceleration action will fail with probability (1-p3).


## 4.2.1. Detour Strategy

The mobile robot moves from its initial positionRS to the reference one R0 and then takes the detour strategy to avoid the obstacle. If the robot rotates to the expected angle, it can move into the desired region R0_R4 successfully (see Figure 3). Otherwise, it may go into another arbitrary region such as R0_R5 (see Figure 3). As stated above, it rotates to the expected angle with probability p1. Therefore, the robot can go into R0_R4 with probability p1, while it will deviate into R0_R5 with probability 1-p1. In the former case, the collision will be effectively avoided and the robot can go to its terminal RE safely, because the detour operation is successful. However, in the latter case, whether the robot will collide with the obstacle or not is still uncertain. If the collision is avoided, the robot will also go to RE successfully. Otherwise, the collision will make the detour operation fail.To help understand the model, four typical state transitions are explained as follows:(1)
SRS_R0→p1,Tr=TRS_R0&Safe=0SR0_R4.When the mobile robot is in the stateSRS_R0 and the value of Safe is equal to 0 (i.e., the obstacle is in the Dangerous Region), the robot will take the detour strategy to switch to the state SR0_R4. The detour operation can be successfully made with probability p1.(2)
SRS_R0→1-p1,Tr=TRS_R0&Safe=0SR0_R5.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot will switch to the state SE0_R5 with probability (1-p1).(3)
SR0_R5→Conflict=1;Tr≔0Collision.When the robot is in the stateSR0_R5 and the value of Conflict is equal to 1 (i.e., the robot collides with the obstacle), the robot will switch to the Collision state.(4)
Collision→Collision.The robot will stay in the Collision state and stop moving.


## 4.2.2. Acceleration Strategy

If the robot locating atR0 takes the Acceleration strategy to avoid collision, it will move to R2 by enhancing its velocity. As stated above, the probability of increasing its velocity to the expected value is p2. Therefore, it can reach R2 with probability p2 and then go to the terminal RE safely. In this strategy, it is easy to infer that the change of velocity will fail with probability 1-p2. When the desired velocity is not obtained, whether the robot will collide with the obstacle or not is uncertain. If the collision is avoided, the robot will also go to RE successfully.Two typical state transitions are explained as follows:(1)
SRS_R0→p2,Tr=TRS_R0&Safe=0SR0_R2.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Acceleration action. Its state switches from SRS_R0 to SR0_R2 with probability p2.(2)
SRS_R0→1-p2,Tr=TRS_R0&Safe=0SER0_R2.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Acceleration action. Its state will change from SRS_R0 to SER0_R2 with probability (1-p2), because the Acceleration action will fail with probability (1-p2).


## 4.2.3. Deceleration Strategy

If the robot locating atR0 takes the Deceleration strategy to avoid collision, it will move to a certain position R5 between R0 and R1 by reducing its velocity. As stated above, the probability of decreasing its velocity to the expected value is p3. Therefore, it can reach R5 with probability p3 and then go to the terminal RE safely. Obviously, the change of velocity will fail with probability 1-p3. When the desired velocity is not obtained, whether the robot will collide with the obstacle or not is uncertain. If the collision is avoided, the robot will also go to RE successfully.Two typical state transitions are as follows:(1)
SRS_R0→p3,Tr=TSRS_R0&Safe=0SR0_R3.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Deceleration action. Its state switches from SRS_R0 to SR0_R3 with probability p3.(2)
SRS_R0→1-p3,Tr=SRS_R0&Safe=0SER0_R3.When the robot is in the stateSRS_R0 and the value of Safe is equal to 0, the robot chooses the Deceleration action. Its state will change from SRS_R0 to SER0_R3 with probability (1-p3), because the Deceleration action will fail with probability (1-p3).


## 5. Probabilistic Analysis and Verification

In this section, we take an example to make probabilistic analysis and verification. The velocities and geometrical parameters of the example are shown in Figure8, where DC and LS represent the diameter of the circle and the side length of the square, respectively.Figure 8
An example of obstacle avoidance.Next, probabilistic analysis is performed in the PRISM software to get the probability-time curves of the three obstacle-avoidance strategies. Then, the corresponding computation is also carried out in MATLAB to verify the effectiveness of the analysis in PRISM. On this basis, the time and energy consumption of the three strategies are calculated in PRISM to help find the optimal strategy.


### 5.1. Mobile Robot Transiting through the Expected States

Here, we consider the cases of the mobile robot moving through the statesSR0_R3 in Detour, SR0_R2 in Acceleration, and SR0_R5 in Deceleration. It is assumed that p1=p2=p3=1.


#### 5.1.1. Probability-Time Curves Given by PRISM

To get the probability-time curves by analysis in PRISM, one has to construct the following PCTL formula at first:(8)Pmax⁡=?FSuccess=1,where the value 1 of Success means that the robot succeeds in avoiding the obstacle.The analysis results corresponding to the three avoidance strategies are shown in Figure9.Figure 9
The probability-time curves of the three obstacle-avoidance strategies.(
1) Detour Strategy. (The rotation radius γ of the robot is prescribed as 1.0 cm.) If the time for the robot to pass the region R0_R4 is less than or equal to 7 s, the obstacle will be successfully avoided.(
2) Acceleration Strategy. If the time to go across the region R0_R2 does not exceed 4 s, the robot is able to avoid collision.(
3) Deceleration Strategy. If the time to pass the region R0_R1 is more than or equal to 21 seconds, the collision can be prevented.


#### 5.1.2. Simulation Results by MATLAB

In this subsection, MATLAB is used to make simulation to verify the correctness of the results obtained by PRISM. To this end, the time of obstacle-avoidance output by PRISM is taken as the input of MATLAB.Nevertheless, how to determine the input time is still a problem needing consideration. In the strategy of Detour or Acceleration, if the robot takes longer time to pass the regionR0_R4 or R0_R2, the probability for it to avoid collision will become smaller. However, shorter time to pass R0_R1 will give rise to smaller obstacle-avoidance probability in the Deceleration mode. Therefore, we choose the maximum time of obstacle avoidance in Detour (i.e., 7 s) or Acceleration (i.e., 4 s) but the minimum one in Deceleration (i.e., 21 s) to make verification in MATLAB.The visualized results of the simulation are provided in Figure10. It is seen that the collision is effectively avoided in each case, which verifies the analysis results in PRISM.Figure 10
Simulation results in MATLAB.
(a)
Detour
(b)
Acceleration
(c)
Deceleration


### 5.2. Mobile Robot Transiting through the Unexpected States

In this subsection, we consider the cases of the mobile robot moving through the statesSR0_R5 in Detour, SER0_R2 in Acceleration, and SER0_R3 in Deceleration.


#### 5.2.1. Verification Results by PRISM

The PCTL formula is(9)Pmax⁡=?FErrorSuccess=1,where the value 1 of ErrorSuccess means that the robot succeeds in avoiding the obstacle finally, even if it goes through the unexpected state.The probability-time curves of the three obstacle-avoidance strategies are shown in Figure11.Figure 11
The probability-time curves of the three obstacle-avoidance strategies.
(a)
Detour withp1=0
(b)
Acceleration
(c)
Deceleration(
1) Detour Strategy. Assume that the expected rotation angle is 45°, but the actual one is only 15° or 30°. Under this condition, the robot will adjust its motion to avoid collisions. Figure 11(a) shows that when the actual rotation angle is 15° or 30° the maximum time to successfully avoid collision is 5 s or 6 s, respectively.(
2) Acceleration. Like in case A, if the time for the robot to reach R2 is less than or equal to 4 s, the obstacle will be avoided (see Figure 11(b)).(
3) Deceleration Strategy. If the time to arrive at R1 is longer than 7 s, the robot can avoid the obstacle (see Figure 11(c)).


#### 5.2.2. Simulation Results by MATLAB

In this subsection, simulations are carried out in MATLAB to verify the analysis results shown in Figure11.(
1) Detour Strategy. Here, the time of obstacle-avoidance output by PRISM is taken as the input of MATLAB. Therefore, when the actual rotation angle is 15° or 30°, we take 5 s or 6 s to perform simulation. Figure 12 shows the visualized results, which obviously verify the results in Figure 11(a).Figure 12
Simulation results in MATLAB.
(a)
Detour with15°
(b)
Detour with30°(
2) Acceleration or Deceleration Strategy. For Acceleration or Deceleration, we take six different values of time and four different values of p2 or p3 to make simulations in MATLAB. In each case, 100 times of simulations are performed to calculate the probability of obstacle avoidance. The results are given in Tables 1 and 2, which are consistent with those shown in Figures 11(b) and 11(c). From this, we come to the conclusion that probabilistic model checking is an effective method to verify the obstacle-avoidance strategies of mobile robots.Table 1
Simulation results of the acceleration strategy.
Time (s)
Probability of obstacle avoidance
p
2
=
0
p
2
=
0.3
p
2
=
0.6
p
2
=
0.9
3
0.999
0.998
0.998
0.997
4
0.998
0.998
0.997
0.996
5
0.8500
0.890
0.940
0.988
6
0.5200
0.690
0.840
0.970
7
0.1800
0.420
0.674
0.926
8
0.0300
0.320
0.600
0.910Table 2
Simulation results of the deceleration strategy.
Time (s)
Probability of obstacle avoidance
p
3
=
0
p
3
=
0.3
p
3
=
0.6
p
3
=
0.9
16
0.02
0.320
0.600
0.910
17
0.05
0.340
0.610
0.930
18
0.16
0.400
0.676
0.924
19
0.52
0.670
0.820
0.960
20
0.87
0.898
0.938
0.989
21
0.98
0.989
0.990
0.999


### 5.3. Minimum Time and Energy Consumption

Here, the minimum time and energy consumption for the robot to go from its initial position to the destination are used to find the optimal obstacle-avoidance strategy. For this purpose, analysis is further performed in PRISM to determine these two parameters for different obstacle-avoidance paths.The PCTL formula corresponding to the minimum time is(10)Pmax⁡=?F≤TDone=1,where the value 1 of Done means the robot reaches the destination safely.The PCTL formula associated with the minimum energy is(11)R“Energy”min⁡=?FDone=1.In addition, the kinetic energy of the robot can be calculated as follows:(12)E1=mv2+Jω22,rotation,E2=mv22,linear  motion,where m is the mass, J is the rotational inertia, v is the linear velocity, and ω is the angular velocity.The analysis results of the minimum time and energy consumption are shown in Table3. In the Detour mode, if actual rotation angle is 45°, the robot arrives at its destination by passing the expected state; otherwise, it reaches the terminal by going through the unexpected state. It is seen that the expected path costs the lowest “minimum energy” but the longest “minimum time,” while the unexpected trajectory (15°) consumes the shortest “minimum time” but the highest “minimum energy.” In the acceleration mode, the expected path (TR0_R2=4) requires the shortest “minimum time” but the highest “minimum energy,” while the unexpected one (TRE0_R2=6) needs the lowest “minimum energy” but the longest “minimum time.” In the Deceleration mode, the expected path (TR0_R3=21) spends the longest “minimum time,” while all the paths expend the same “minimum energy.” Further comparison shows that the Acceleration strategy (TR0_R2=4) is the least time-costing, while the Deceleration one is the least energy-consuming, among all the three kinds of strategies.Table 3
Minimum time and energy consumption.
Methods
Time (s)
Minimum time (s)
Minimum energy (10−7 J)
Detour (45°)
T
R
0
_
R
4
=
5
24
2.2
Detour (30°)
T
R
0
_
R
5
=
5
23
2.4
Detour (15°)
T
R
0
_
R
5
=
5
22
2.6
Acceleration
T
R
0
_
R
2
=
4
19
3.5
Acceleration
T
E
R
0
_
R
2
=
5
20
3.4
Acceleration
T
E
R
0
_
R
2
=
6
21
3.3
Deceleration
T
R
0
_
R
3
=
2
1
40
1.5
Deceleration
T
E
R
0
_
R
3
=
20
39
1.5
Deceleration
T
E
R
0
_
R
3
=
19
38
1.5Finally, it deserves noting that the data in Table3 can help us to find the optimal obstacle-avoidance strategy. For example, if the movement time of the robot is limited, we can choose the Acceleration strategy (TR0_R2=4). If the power supply is not so sufficient, the Deceleration strategy can be selected instead.


## 5.1. Mobile Robot Transiting through the Expected States

Here, we consider the cases of the mobile robot moving through the statesSR0_R3 in Detour, SR0_R2 in Acceleration, and SR0_R5 in Deceleration. It is assumed that p1=p2=p3=1.


### 5.1.1. Probability-Time Curves Given by PRISM

To get the probability-time curves by analysis in PRISM, one has to construct the following PCTL formula at first:(8)Pmax⁡=?FSuccess=1,where the value 1 of Success means that the robot succeeds in avoiding the obstacle.The analysis results corresponding to the three avoidance strategies are shown in Figure9.Figure 9
The probability-time curves of the three obstacle-avoidance strategies.(
1) Detour Strategy. (The rotation radius γ of the robot is prescribed as 1.0 cm.) If the time for the robot to pass the region R0_R4 is less than or equal to 7 s, the obstacle will be successfully avoided.(
2) Acceleration Strategy. If the time to go across the region R0_R2 does not exceed 4 s, the robot is able to avoid collision.(
3) Deceleration Strategy. If the time to pass the region R0_R1 is more than or equal to 21 seconds, the collision can be prevented.


### 5.1.2. Simulation Results by MATLAB

In this subsection, MATLAB is used to make simulation to verify the correctness of the results obtained by PRISM. To this end, the time of obstacle-avoidance output by PRISM is taken as the input of MATLAB.Nevertheless, how to determine the input time is still a problem needing consideration. In the strategy of Detour or Acceleration, if the robot takes longer time to pass the regionR0_R4 or R0_R2, the probability for it to avoid collision will become smaller. However, shorter time to pass R0_R1 will give rise to smaller obstacle-avoidance probability in the Deceleration mode. Therefore, we choose the maximum time of obstacle avoidance in Detour (i.e., 7 s) or Acceleration (i.e., 4 s) but the minimum one in Deceleration (i.e., 21 s) to make verification in MATLAB.The visualized results of the simulation are provided in Figure10. It is seen that the collision is effectively avoided in each case, which verifies the analysis results in PRISM.Figure 10
Simulation results in MATLAB.
(a)
Detour
(b)
Acceleration
(c)
Deceleration


## 5.1.1. Probability-Time Curves Given by PRISM

To get the probability-time curves by analysis in PRISM, one has to construct the following PCTL formula at first:(8)Pmax⁡=?FSuccess=1,where the value 1 of Success means that the robot succeeds in avoiding the obstacle.The analysis results corresponding to the three avoidance strategies are shown in Figure9.Figure 9
The probability-time curves of the three obstacle-avoidance strategies.(
1) Detour Strategy. (The rotation radius γ of the robot is prescribed as 1.0 cm.) If the time for the robot to pass the region R0_R4 is less than or equal to 7 s, the obstacle will be successfully avoided.(
2) Acceleration Strategy. If the time to go across the region R0_R2 does not exceed 4 s, the robot is able to avoid collision.(
3) Deceleration Strategy. If the time to pass the region R0_R1 is more than or equal to 21 seconds, the collision can be prevented.


## 5.1.2. Simulation Results by MATLAB

In this subsection, MATLAB is used to make simulation to verify the correctness of the results obtained by PRISM. To this end, the time of obstacle-avoidance output by PRISM is taken as the input of MATLAB.Nevertheless, how to determine the input time is still a problem needing consideration. In the strategy of Detour or Acceleration, if the robot takes longer time to pass the regionR0_R4 or R0_R2, the probability for it to avoid collision will become smaller. However, shorter time to pass R0_R1 will give rise to smaller obstacle-avoidance probability in the Deceleration mode. Therefore, we choose the maximum time of obstacle avoidance in Detour (i.e., 7 s) or Acceleration (i.e., 4 s) but the minimum one in Deceleration (i.e., 21 s) to make verification in MATLAB.The visualized results of the simulation are provided in Figure10. It is seen that the collision is effectively avoided in each case, which verifies the analysis results in PRISM.Figure 10
Simulation results in MATLAB.
(a)
Detour
(b)
Acceleration
(c)
Deceleration


## 5.2. Mobile Robot Transiting through the Unexpected States

In this subsection, we consider the cases of the mobile robot moving through the statesSR0_R5 in Detour, SER0_R2 in Acceleration, and SER0_R3 in Deceleration.


### 5.2.1. Verification Results by PRISM

The PCTL formula is(9)Pmax⁡=?FErrorSuccess=1,where the value 1 of ErrorSuccess means that the robot succeeds in avoiding the obstacle finally, even if it goes through the unexpected state.The probability-time curves of the three obstacle-avoidance strategies are shown in Figure11.Figure 11
The probability-time curves of the three obstacle-avoidance strategies.
(a)
Detour withp1=0
(b)
Acceleration
(c)
Deceleration(
1) Detour Strategy. Assume that the expected rotation angle is 45°, but the actual one is only 15° or 30°. Under this condition, the robot will adjust its motion to avoid collisions. Figure 11(a) shows that when the actual rotation angle is 15° or 30° the maximum time to successfully avoid collision is 5 s or 6 s, respectively.(
2) Acceleration. Like in case A, if the time for the robot to reach R2 is less than or equal to 4 s, the obstacle will be avoided (see Figure 11(b)).(
3) Deceleration Strategy. If the time to arrive at R1 is longer than 7 s, the robot can avoid the obstacle (see Figure 11(c)).


### 5.2.2. Simulation Results by MATLAB

In this subsection, simulations are carried out in MATLAB to verify the analysis results shown in Figure11.(
1) Detour Strategy. Here, the time of obstacle-avoidance output by PRISM is taken as the input of MATLAB. Therefore, when the actual rotation angle is 15° or 30°, we take 5 s or 6 s to perform simulation. Figure 12 shows the visualized results, which obviously verify the results in Figure 11(a).Figure 12
Simulation results in MATLAB.
(a)
Detour with15°
(b)
Detour with30°(
2) Acceleration or Deceleration Strategy. For Acceleration or Deceleration, we take six different values of time and four different values of p2 or p3 to make simulations in MATLAB. In each case, 100 times of simulations are performed to calculate the probability of obstacle avoidance. The results are given in Tables 1 and 2, which are consistent with those shown in Figures 11(b) and 11(c). From this, we come to the conclusion that probabilistic model checking is an effective method to verify the obstacle-avoidance strategies of mobile robots.Table 1
Simulation results of the acceleration strategy.
Time (s)
Probability of obstacle avoidance
p
2
=
0
p
2
=
0.3
p
2
=
0.6
p
2
=
0.9
3
0.999
0.998
0.998
0.997
4
0.998
0.998
0.997
0.996
5
0.8500
0.890
0.940
0.988
6
0.5200
0.690
0.840
0.970
7
0.1800
0.420
0.674
0.926
8
0.0300
0.320
0.600
0.910Table 2
Simulation results of the deceleration strategy.
Time (s)
Probability of obstacle avoidance
p
3
=
0
p
3
=
0.3
p
3
=
0.6
p
3
=
0.9
16
0.02
0.320
0.600
0.910
17
0.05
0.340
0.610
0.930
18
0.16
0.400
0.676
0.924
19
0.52
0.670
0.820
0.960
20
0.87
0.898
0.938
0.989
21
0.98
0.989
0.990
0.999


## 5.2.1. Verification Results by PRISM

The PCTL formula is(9)Pmax⁡=?FErrorSuccess=1,where the value 1 of ErrorSuccess means that the robot succeeds in avoiding the obstacle finally, even if it goes through the unexpected state.The probability-time curves of the three obstacle-avoidance strategies are shown in Figure11.Figure 11
The probability-time curves of the three obstacle-avoidance strategies.
(a)
Detour withp1=0
(b)
Acceleration
(c)
Deceleration(
1) Detour Strategy. Assume that the expected rotation angle is 45°, but the actual one is only 15° or 30°. Under this condition, the robot will adjust its motion to avoid collisions. Figure 11(a) shows that when the actual rotation angle is 15° or 30° the maximum time to successfully avoid collision is 5 s or 6 s, respectively.(
2) Acceleration. Like in case A, if the time for the robot to reach R2 is less than or equal to 4 s, the obstacle will be avoided (see Figure 11(b)).(
3) Deceleration Strategy. If the time to arrive at R1 is longer than 7 s, the robot can avoid the obstacle (see Figure 11(c)).


## 5.2.2. Simulation Results by MATLAB

In this subsection, simulations are carried out in MATLAB to verify the analysis results shown in Figure11.(
1) Detour Strategy. Here, the time of obstacle-avoidance output by PRISM is taken as the input of MATLAB. Therefore, when the actual rotation angle is 15° or 30°, we take 5 s or 6 s to perform simulation. Figure 12 shows the visualized results, which obviously verify the results in Figure 11(a).Figure 12
Simulation results in MATLAB.
(a)
Detour with15°
(b)
Detour with30°(
2) Acceleration or Deceleration Strategy. For Acceleration or Deceleration, we take six different values of time and four different values of p2 or p3 to make simulations in MATLAB. In each case, 100 times of simulations are performed to calculate the probability of obstacle avoidance. The results are given in Tables 1 and 2, which are consistent with those shown in Figures 11(b) and 11(c). From this, we come to the conclusion that probabilistic model checking is an effective method to verify the obstacle-avoidance strategies of mobile robots.Table 1
Simulation results of the acceleration strategy.
Time (s)
Probability of obstacle avoidance
p
2
=
0
p
2
=
0.3
p
2
=
0.6
p
2
=
0.9
3
0.999
0.998
0.998
0.997
4
0.998
0.998
0.997
0.996
5
0.8500
0.890
0.940
0.988
6
0.5200
0.690
0.840
0.970
7
0.1800
0.420
0.674
0.926
8
0.0300
0.320
0.600
0.910Table 2
Simulation results of the deceleration strategy.
Time (s)
Probability of obstacle avoidance
p
3
=
0
p
3
=
0.3
p
3
=
0.6
p
3
=
0.9
16
0.02
0.320
0.600
0.910
17
0.05
0.340
0.610
0.930
18
0.16
0.400
0.676
0.924
19
0.52
0.670
0.820
0.960
20
0.87
0.898
0.938
0.989
21
0.98
0.989
0.990
0.999


## 5.3. Minimum Time and Energy Consumption

Here, the minimum time and energy consumption for the robot to go from its initial position to the destination are used to find the optimal obstacle-avoidance strategy. For this purpose, analysis is further performed in PRISM to determine these two parameters for different obstacle-avoidance paths.The PCTL formula corresponding to the minimum time is(10)Pmax⁡=?F≤TDone=1,where the value 1 of Done means the robot reaches the destination safely.The PCTL formula associated with the minimum energy is(11)R“Energy”min⁡=?FDone=1.In addition, the kinetic energy of the robot can be calculated as follows:(12)E1=mv2+Jω22,rotation,E2=mv22,linear  motion,where m is the mass, J is the rotational inertia, v is the linear velocity, and ω is the angular velocity.The analysis results of the minimum time and energy consumption are shown in Table3. In the Detour mode, if actual rotation angle is 45°, the robot arrives at its destination by passing the expected state; otherwise, it reaches the terminal by going through the unexpected state. It is seen that the expected path costs the lowest “minimum energy” but the longest “minimum time,” while the unexpected trajectory (15°) consumes the shortest “minimum time” but the highest “minimum energy.” In the acceleration mode, the expected path (TR0_R2=4) requires the shortest “minimum time” but the highest “minimum energy,” while the unexpected one (TRE0_R2=6) needs the lowest “minimum energy” but the longest “minimum time.” In the Deceleration mode, the expected path (TR0_R3=21) spends the longest “minimum time,” while all the paths expend the same “minimum energy.” Further comparison shows that the Acceleration strategy (TR0_R2=4) is the least time-costing, while the Deceleration one is the least energy-consuming, among all the three kinds of strategies.Table 3
Minimum time and energy consumption.
Methods
Time (s)
Minimum time (s)
Minimum energy (10−7 J)
Detour (45°)
T
R
0
_
R
4
=
5
24
2.2
Detour (30°)
T
R
0
_
R
5
=
5
23
2.4
Detour (15°)
T
R
0
_
R
5
=
5
22
2.6
Acceleration
T
R
0
_
R
2
=
4
19
3.5
Acceleration
T
E
R
0
_
R
2
=
5
20
3.4
Acceleration
T
E
R
0
_
R
2
=
6
21
3.3
Deceleration
T
R
0
_
R
3
=
2
1
40
1.5
Deceleration
T
E
R
0
_
R
3
=
20
39
1.5
Deceleration
T
E
R
0
_
R
3
=
19
38
1.5Finally, it deserves noting that the data in Table3 can help us to find the optimal obstacle-avoidance strategy. For example, if the movement time of the robot is limited, we can choose the Acceleration strategy (TR0_R2=4). If the power supply is not so sufficient, the Deceleration strategy can be selected instead.


## 6. Conclusions

The MDP-based probabilistic formal models are constructed for three different kinds of obstacle-avoidance strategies for a mobile robot in an uncertain dynamic environment. The PCTL formulae are then built to perform analysis in the PRISM software, which yields the probability-time curves for the obstacle-avoidance paths. In addition, the time of obstacle-avoidance output by PRISM is taken as input to conduct simulations in MATLAB, which verify the correctness of the results obtained by PRISM. Further, both the minimum time and the energy consumption for the robot to reach its destination under each obstacle-avoidance strategy are obtained by analyses in PRISM. Finally, the time or energy based optimal condition is thereby applied to determine the optimal obstacle-avoidance strategy under diverse circumstances.It deserves noting that the present paper only verifies the probabilistic obstacle-avoidance strategies that involve a mobile robot and a single dynamic obstacle. In practice, there may be more complex obstacle-avoidance conditions. For example, a single mobile robot may encounter several dynamic obstacles, or, even worse, a swarm of mobile robots may have to go across a terrain with multiple dynamic obstacles. These complex cases require more complicated probabilistic formal verifications. The present paper lays a good foundation for these future works.



---

*Source: 837259-2015-10-25.xml*