Consider the behaviour of a robot that traverses an arena performing some task. This could be a behavioural component for the following applications:

- A robotic member of a bomb-disposal unit, given the task of detecting explosive material, must traverse a suspect arena “sniffing” for molecules of explosives. As the robot gently inhales air, a fluorescing polymer stops glowing if even a single molecule is detected.
- A robot contributing to a search-and-rescue mission traverses the area looking for signs of survival in a building. The robot is equipped with a microphone and vibration sensors.
- A floor-cleaning robot must pass over the floor, vacuuming as it goes.

There are two obvious strategies for the robot’s traversal of a given area: (a) build a map of the arena and then use this to carry out the traversal; (b) use a two-dimensional random walk to traverse the area. The first alternative is probably more expensive than the second, because of the need for cameras and sensors. It is not obvious which is quicker: the random walk will not produce an optimal traversal, but the cartographer robot has a planning stage before starting its traversal. Some robots employ a hybrid combination of both strategies.

The robot that we consider uses the random walk strategy. For simplicity, we consider a rectangular arena divided up in some way appropriate for the robot: the effective sniffing area for explosives; the microphone and vibration sensor range for detecting survivors; or the width of the vacuum cleaner’s brushes. We start by considering a square grid.

This case study aims to show how to model and verify the probabilistic behaviour of the robot with the random walk strategy. In addition, considering the state space size of this 30x30 squares, we show how to use statistic model checking as a complement to accurate model checking to design an enough battery capacity in order to cover whole area.

This version uses multi-way synchronisations of the `move`

event and the `rcrd`

event, but the multi-way synchronisation is not supported in RoboChart yet. Please see V2 for another model that uses two-way synchronisation only. Please see another example “Internal mail delivery robot” that uses the similar two-way synchronisation.

Our model is parametrised by the dimensions and we instantiate our analysis to a 30 × 30 square grid, representing 100 square meters for an iRobot Roomba vacuum cleaner. Although the discretisation of the continuous arena is an idealisation, the area under consideration is realistic, given battery capacities for such robots.

Our statechart model of the robot’s controller is divided into two orthogonal parts: one part carries out a one-dimensional random walk of the grid in the *x-axis*, and the other part carries out a one-dimensional random walk in the *y-axis*. The two parts have the same essential behaviour and the interaction between them produces the required two-dimensional random walk.

The overall behaviour of the robot is specified in the module `random_walker`

.

It is composed of one robotic platform and three controllers. These controllers synchronise on two events: `move`

and `rcrd`

. The robotic platform `RW_RP`

provides an interface `RWInf`

which has three constants

`MAX`

: the maximum number of moves, which corresponds to the capacity of the battery in the robot,`M`

: the width of the grid,`N`

: the height of the grid.

and three varaibles

`x`

: current position in the*x-axis*,`y`

: current position in the*y-axis*,`steps`

: the total number of moves that the robot has taken since it started.

Three constrollers:

`left_rightC`

: the controller for the*x-axis*,`up_downC`

: the controller for the*y-axis*,`recorderC`

: the controller to record those parts of the grid visited by the robot and total number of moves.

Each controller has one state machine inside.

The left right state machine `left_right`

has one local variable `lrh`

and its type is the enumeration `LRH`

denoting moving direction.

`lt`

for the left direction,`rt`

for the right direction,- and
`vt`

for staying in current location. It is idling, allowing the possibility of the other controller driving up or down the*y-axis*. The robot enters this mode only at the extreme ends of the`x-axis`

.

The state machine has only one state `LR`

. Various transitions denote different moves in the *x-axis*. It is worth noting that each transition has a trigger `move`

and an event `rcrd`

to allow the state machine synchronise with other controllers.

`Initialisation`

(`0`

in the diagram): initially, the robot starts at the left corner (`x=1`

) and its direction is`vt`

;`Idle left`

(`1`

): when it is idling (`lrh==vt`

), in its left end (`x==1`

), and doesn’t reach the maximum number of moves (`steps<MAX`

), it could either move right and increase`x`

by 1, or stay with equal probability (`0.5`

);`Idle right`

(`2`

): when it is idling (`lrh==vt`

), in its right end (`x==M`

), and doesn’t reach the maximum number of moves (`steps<MAX`

), it could either move left and decrease`x`

by 1, or stay with equal probability (`0.5`

);`Left decision`

(`3`

): when it is moving left (`lrh==lt`

) but reachs its left end (`x==1`

), it could either turn around and move right, or idle with equal probability (`0.5`

);`Right decision`

(`4`

): when it is moving right (`lrh==rt`

) but reachs its right end (`x==M`

), it could either turn around and move left, or idle with equal probability (`0.5`

);`Right move`

(`5`

): when it is moving right (`lrh==rt`

) but hasn’t reached its right end (`x<M`

), it will continuously move right;`Left move`

(`6`

): when it is moving left (`lrh==lt`

) but hasn’t reached its left end (`x>1`

), it will continuously move left;`Terminate`

(`7`

): the final operation models termination when the number of steps has reached the maximum allowed (`steps==MAX`

);

The up down state machine is symmetric to the left right state machine, except that `N`

and `y`

will be used instead of `M`

and `x`

in `left_right`

.

The `record`

state machine has a local variable `v`

which is a two-dimension array (sequence of sequence) to record visited grids.

- Initially,
`steps`

is set to 0, all MxN grids in`v`

are set to not visited (0) except the bottom left grid because the robot starts at this grid.`mk2DArrayDefault`

is a function defined to return a sequence of sequence with its MxN grids set to 0; - Each normal move starts at the state
`REC2`

with synchronisation on`move`

. Its outgoing transition to`REC1`

increases`steps`

, then returns to`REC2`

by synchronising on`rcrd`

as well as updating the grid as visited; - After it reachs the maximum number of moves allowed, it will terminate by being taken into
`REC3`

.

The configuration file should be modified accordingly for different square size. `MAX_SEQ_INS=4`

should be updated to the bigger one of `M`

and `N`

.

Constants: `M=4, N=4, MAX=100`

`pass`

)```
!E [ F "deadlock" ]
```

`MxN`

steps? (`yes`

)```
!E [ F visits=M*N & steps<(M*N) ]
```

`MxN`

steps? (`yes`

)```
E [ F visits=M*N & steps=(M*N) ]
```

`MxN`

steps? (`1.52587890625E-5`

)```
P=? [ F visits=M*N & steps=(M*N) ]
```

It is very unlikely to cover all areas just in `MxN`

steps.

`MAX`

steps?```
P=? [ F visits=M*N]
```

Result: 0.9745634300800323

Performance:

Item | Number |
---|---|

States | 40901958 |

Transitions | 68833377 |

Time for model construction | 1357.583 seconds/23 minutes |

Time for model checking | 31396.768 seconds/8.72 hours |

The verification above has shown that model checking is time intensive. Actually it is also CPU and memory intensive. For the models with big state spaces, it may be not possible to carry out model checking. Even just for 4x4 grid, it takes about 9 hours to finish. One possible way to improve time consumed is to bound property. For example, the property below is interpreted as “the possibility to visit all areas in its first 10000 time units”. Since each transition in DTMC models takes one time unit, this bound `F<=10000`

also denotes the number of transitions taken.

```
P=? [ F<=10000 visits=M*N]
```

Statistic model checking, that uses simulation to approximate results of properties, is an alternative to exact model checking. Especially for large state spaces it is very useful to get approximate results of properties and analyse basic trend.

Using statistic model checking in PRISM, for the bounded property the approximate relation between the possibility to cover all areas and `MAX`

is shown in the diagram below.

As can be seen, when `MAX`

is larger than 130, the result is bigger than 0.99. Therefore, the robot is very likely to cover all areas if its battery allows it to run more than 130 moves before out of power.

Performance:

Item | Number |
---|---|

Simulation method | CI (Confidence Interval) |

confidence | 0.01 |

number of samples | 1000 |

max path length | 10000 |

Time for statistic model checking | 5 minutes for `MAX` from [10:20:190] (10 values) |

Time for statistic model checking (one) | 30 seconds |

For `MAX=100`

, the probability obtained through simulation is *0.974*. It is very close to its exact result *0.9745634300800323*. It is worth noting that the time for simulation (30 seconds) is much less than that of model checking (8.7 hours). Therefore, simulation is a good way to tackle state space explosion of this model.

`MAX`

steps?```
P=? [ F<=10000 visits=M*N]
```

For 6x6 squares, in order to get the same probability (over 0.99), `MAX`

should be around or over 400.

`MAX`

steps?```
P=? [ F<=10000 visits=M*N]
```

`MAX`

steps?We use different bound time units in the formulas below.

```
P=? [ F<=10000 visits=M*N]
P=? [ F<=50000 visits=M*N]
```

As can be seen from the diagram above, different bound time units have a slight impact on the results. The bigger the bound time unit is, the more accurate the result is.

`MAX`

steps?```
P=? [ F<=10000 visits=M*N]
```

With increasing room size, the difference of results between different bound time units is widen.

Eventually for the 30x30 grid, we choose two bounded time units: *200,000* and *1,000,000*.

From the diagram, we see that the results from the bounded *200,000* are very close to that of *1,000,000*. When `MAX`

is larger than 30,000 steps, the probability to cover all areas in `MAX`

steps is very high. The model checking time of one `MAX`

value for both *200,000* and *1,000,000* is approximately 250 minutes.

After we get a trend, we can determine a concrete value for `MAX`

, such as 30,000 above. Then we fix this value, but increase the number of samples and the bounded time unit in the property in order to get a relatively more accurate result.

Similar to “Internal mail delivery robot” that splits `move & update`

into `move`

then `update`

, this version also uses the same way to split `move & rcrd`

into `move`

then `rcrd`

.

In stead of three-way synchronisation of the `move`

event and the `rcrd`

event, this model only uses two-way synchronisation that RoboChart is able to support now. We still use the `move`

event to synchronise between `left_rightC`

and `up_downC`

as seen in the diagram below. But instead of `rcrd`

, we split it into `rcrd_x`

(synchronisation with `left_rightC`

) and `rcrd_y`

(synchronisation with `up_downC`

).

The `left_right`

state machine is shown below. As seen in the diagram, all transitions from probabilistic junctions have a sequential action `rcrd_start; rcrd_end`

in the end of their actions. Accordingly, `up_down`

will be updated in the same way. For brevity, it is omitted here.

The `recorder`

is also updated (see the diagram below). It is worth noting that the state machine starts to update `steps`

and `v`

after synchronisations with both `left_right`

and `up_down`

on `rcrd_x_start`

and `rcrd_y_start`

separately, then finishes updating by synchronisations with `left_right`

and `up_down`

on the events `rcrd_x_start`

and `rcrd_y_start`

separately.

Now our probabilistic assertion language cannot support this model yet due to the used array `v`

(only simple variables are supported now).

Constants: `M=3, N=3, MAX=100`

`pass`

)```
!E [ F "deadlock" ]
```

`MxN-1`

steps? (`yes`

)```
!E [ F visits=M*N & steps<(M*N-1) ]
```

`MxN-1`

steps? (`yes`

)Initially the robot is at the location (1,1) and this is marked as visited without movement. Therefore, it is possible to visit all areas in just 8 moves. But for 4x4, such pathes don’t exist. The most optimised pathes need to visit at least one area twice in order to cover all areas.

```
E [ F visits=M*N & steps=(M*N-1) ]
```

`MxN`

steps? (`9.765626E-4`

)```
P=? [ F visits=M*N & steps=(M*N-1) ]
```

It is very unlikely to cover all areas just in `MxN`

steps.

`MAX`

steps?```
P=? [ F visits=M*N]
```

Result: 0.9998854856285614

Constants: `M=4, N=4, MAX=100`

`pass`

)```
!E [ F "deadlock" ]
```

`MxN`

steps? (`yes`

)```
!E [ F visits=M*N & steps<(M*N) ]
```

`MxN`

steps? (`yes`

)```
E [ F visits=M*N & steps=(M*N) ]
```

`MxN`

steps? (`1.52587890625E-5`

)```
P=? [ F visits=M*N & steps=(M*N) ]
```

It is very unlikely to cover all areas just in `MxN`

steps.

`MAX`

steps?```
P=? [ F visits=M*N]
```

Simulation results (option: `-sim -simmethod ci -simsamples 1000 -simconf 0.01 -simpathlen 10000`

) are displayed below.

Constants: `M=30, N=30, MAX=6000`

`MAX`

steps?```
P=? [ F visits=M*N]
```

It is not possible to model-check this model due to its state space size.

```
P=? [ F<=400000 visits=M*N]
```

Simulation results (option: `-sim -simmethod ci -simsamples 1000 -simconf 0.01 -simpathlen 200000`

) are displayed below.

Compared to the results of the first model in 4x4, the results of this model V2 are consistent.

Similar to “Internal mail delivery robot”, this version also changes the direction of connections.

Basic definitions.

Properties.

Simulations.

Constants: `M=3, N=3, MAX=100`

Assertion | Const | Const | Const | states: | transitions: | result: | checkTime: |
---|---|---|---|---|---|---|---|

P_E_minimality1 | N=3 | M=3 | MAX=100 | 7175565 | 13527160 | true | 0.137 seconds |

Assertion | Const | Const | Const | states: | transitions: | result: | checkTime: |
---|---|---|---|---|---|---|---|

P_E_minimality | N=3 | M=3 | MAX=100 | 7175565 | 13527160 | true | 0.825 seconds |

Assertion | Const | Const | Const | states: | transitions: | result: | checkTime: |
---|---|---|---|---|---|---|---|

P_minimal_path | N=3 | M=3 | MAX=100 | 7175565 | 13527160 | true | 4.398 seconds |

Assertion | Const | Const | Const | states: | transitions: | result: | checkTime: |
---|---|---|---|---|---|---|---|

P_prob_minimal_path | N=3 | M=3 | MAX=100 | 7175565 | 13527160 | 9.765625E-4 | 12.049 seconds |

Assertion | Const | Const | Const | states: | transitions: | result: | checkTime: |
---|---|---|---|---|---|---|---|

P_prob_full_coverage | N=3 | M=3 | MAX=100 | 7175565 | 13527160 | 0.999882695038118 | 1328.976 seconds |

Assertion | Const | Const | Const | states: | transitions: | result: | checkTime: |
---|---|---|---|---|---|---|---|

P_E_minimality | N=3 | M=3 | MAX=100 | true |

Assertion | Const | Const | Const | states: | transitions: | result: | checkTime: |
---|---|---|---|---|---|---|---|

P_minimal_path | N=3 | M=3 | MAX=100 | true |

Assertion | Const | Const | Const | states: | transitions: | result: | checkTime: |
---|---|---|---|---|---|---|---|

P_prob_minimal_path | N=3 | M=3 | MAX=100 | Error: Approximation is not precise enough to get a result. |

Assertion | Const | Const | Const | states: | transitions: | result: | checkTime: |
---|---|---|---|---|---|---|---|

P_prob_full_coverage_bound | N=3 | M=3 | MAX=100 | true |

This case study shows how our RoboTool could be used to analyse the probabilistic behaviour of RoboChart models to facilitate design of robotic systems. Especially, for large models when exact model checking is not applicable, statistic model checking could be used to get an approximate result. Though the results are not exactly accurate, they still could provide a guidance for designs and finally narrow down design spaces.

Deramore Lane, University of York, Heslington, York, YO10 5GH, UK

Tel: 01904 325500

University of York legal statements