Random Walker

Introduction

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

1. 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.
2. 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.
3. 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.

V1

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.

Model (download)

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.

Overall behaviour

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 RWInfwhich 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.

Left right

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);

Up down

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.

Recorder

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.

Generated PRISM models

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.

4x4 (download)

6x6 (download)

8x8 (download)

10x10 (download)

12x12 (download)

30x30 (download)

Analysis

4x4

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

P1) deadlock free (pass)

!E [ F "deadlock" ]

P2) minimality: is there not possible to cover all areas in less than MxN steps? (yes)

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

P3) minimal path: is there possible to cover all areas just in MxN steps? (yes)

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

P4) minimality: the probability to cover all areas just in 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.

P5) full coverage: the probability to cover all areas in MAX steps?

Exact model checking

P=? [ F visits=M*N]

Result: 0.9745634300800323

Performance:

Bounded property and simulation

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:

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.

6x6

P5) the probability to cover all areas in 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.

8x8

P5) the probability to cover all areas in MAX steps?

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

10x10

P5) the probability to cover all areas in 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.

12x12

P5) the probability to cover all areas in MAX steps?

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

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

30x30

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.

V2

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.

Model

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.

Generated PRISM models

3x3 (download)

4x4 (download)

30x30 (download)

Analysis

Assertions

Now our probabilistic assertion language cannot support this model yet due to the used array v (only simple variables are supported now).

3x3

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

P1) deadlock free (pass)

!E [ F "deadlock" ]

P2) minimality: is there not possible to cover all areas in less than MxN-1 steps? (yes)

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

P3) minimal path: is there possible to cover all areas just in 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) ]

P4) minimality: the probability to cover all areas just in 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.

P5) full coverage: the probability to cover all areas in MAX steps?

Exact model checking

P=? [ F visits=M*N]

Result: 0.9998854856285614

4x4

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

P1) deadlock free (pass)

!E [ F "deadlock" ]

P2) minimality: is there not possible to cover all areas in less than MxN steps? (yes)

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

P3) minimal path: is there possible to cover all areas just in MxN steps? (yes)

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

P4) minimality: the probability to cover all areas just in 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.

P5) full coverage: the probability to cover all areas in MAX steps?

P=? [ F visits=M*N]

Simulation results (option: -sim -simmethod ci -simsamples 1000 -simconf 0.01 -simpathlen 10000) are displayed below.

30x30

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

P5) full coverage: the probability to cover all areas in MAX steps?

Exact model checking

P=? [ F visits=M*N]

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

Bounded property and simulation

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

Simulation results (option: -sim -simmethod ci -simsamples 1000 -simconf 0.01 -simpathlen 200000) are displayed below.

Comparison

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

V3

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

Model

Generated PRISM models

3x3 (download)

Analysis

Assertions

Basic definitions.

Properties.

Simulations.

3x3

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

Assertion: P_E_minimality1

Assertion: P_E_minimality

Assertion: P_minimal_path

Assertion: P_prob_minimal_path

Assertion: P_prob_full_coverage

Assertion: P_E_minimality

Assertion: P_minimal_path

Assertion: P_prob_minimal_path

Assertion: P_prob_full_coverage_bound

Conclusion

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.