Consider the behaviour of a robot that traverses an arena performing some task. This could be a behavioural component for the following applications:
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,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.
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;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;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.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements