Grid World Robot



This case study considers an n×n grid world with a robot moving from the bottom left corner to the top right corner, first along the bottom edge and then along the right edge. The time taken by the robot to move from one square to another is exponentially distributed. There is a janitor moving randomly around the grid (initially in the top right hand corner), and the robot cannot move into a square occupied by the janitor. The robot also randomly sends a signal to the base station.

Grid world

Solution Method:

Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. In this case study we compare the two solution techniques when applied to the verification of time-bounded until formulae in the temporal stochastic logic CSL.

The verification of time-bounded CSL formulae can be reduced to transient analysis [BHHK00a]. Efficient numerical solution techniques, such as uniformisation [Jen53, Gra77], for transient analysis of CTMCs have been existed for decades and are well-understood. Younes and Simmons [YS02] have proposed a statistical approach for verifying time-bounded CSL formulae, based on acceptance sampling and discrete event simulation.

Although the algorithm of Younes and Simmons [YS02] can handle CSL formulae with nested probabilistic operators, the way in which it is done requires in the worst case that the nested formula be verified in each state along a sample path. The numerical approach, on the other hand, can verify the nested formula for all states simultaneously at the same (asymptotic) cost as verifying the formula for a single state. This is a clear advantage when dealing with nested probabilistic operators.

We therefore propose a mixed approach, where statistical sampling is used to verify the outermost probabilistic operator, while numerical techniques are used to verify the nested probabilistic operators. We can mix the numerical and statistical techniques by assuming that the result of the numerical technique holds with certainty. The nested formulae are first verified for all states using numerical methods. When verifying a path formula over a sample path we only need to read the value for each state along the path without any additional verification effort for the nested formulae. The cost for verifying the nested components of a formula is exactly the same for the mixed approach as for the numerical approach, but the use of sampling for the outermost probabilistic operator can provide a solution faster than a numerical computation.

Further details on the comparison between the different methods is available in [YKNP04, YKNP06].

The PRISM Model

Our PRISM model of the system comprises 2 modules, one for the robot and one for the janitor. Below we give the PRISM language description for the system. Note that to change the size of the grid one need only set the value of the constant n appearing at the start of the description.

// Hakan Younes/gxn/dxp 04/05/04


const int n; // size of the grid
const double mr = 1; // rate that the robot moves
const double mj = 2; // rate that the janitor moves
const double cr1 = 1/10; // rate to send a signal to the base station
const double cr2 = 1/2; // rate for communication completion

// the following formulae return 1 or 0 depending on whether
// the janitor can move in that direction or not
formula right = min(1,max(n-x2,0));
formula left = min(1,max(x2-1,0));
formula up = min(1,max(n-y2,0));
formula down = min(1,max(y2-1,0));

// total number of moves the janitor randomly picks from
formula moves = right+left+up+down;

module robot
	x1 : [1..n] init 1; // x position of robot
	y1 : [1..n] init 1; // y position of robot
	c  : [0..1] init 0; // status of signal
	[] x1<n & c=0 & !(x1+1=x2 & y1=y2) -> mr : (x1'=x1+1); // moves right
	[] x1=n & y1<n & c=0 & !(x1=x2 & y1+1=y2) -> mr : (y1'=y1+1); // moves up
	[] c=0 -> cr1 : (c'=1); // send signal
	[] c=1 -> cr2 : (c'=0); // finish communicating

module janitor
	x2 : [1..n] init n; // x position of janitor
	y2 : [1..n] init n; // y position of janitor
	[] !(y2=n | (y2+1=y1 & x2=x1)) -> mj/moves : (y2'=y2+1); // moves up 
	[] !(y2=1 | (y2-1=y1 & x2=x1))  -> mj/moves : (y2'=y2-1); // moves down
	[] !(x2=1 | (x2-1=x1 & y2=y1))  -> mj/moves : (x2'=x2-1); // moves left
	[] !(x2=n | (x2+1=x1 & y2=y1)) -> mj/moves : (x2'=x2+1); // moves right

View: printable version          Download: robot.sm

Model Statistics

The tables below shows statistics and construction times of the models when the size of the grid (n) varies. The tables include:

  • the number of states and transitions in the CTMC representing the model;
  • both the number of nodes and leaves of the MTBDD which represents the model;
  • the construct time which equals the time taken for the system description to be parsed and converted to the MTBDD representing it, and the time to perform reachability, identify the non-reachable states and filter MTBDD accordingly;
  • the number of iterations required to find the reachable states (which is performed via a BDD based fixpoint algorithm).

Note that this construction is only required when using the numerical method, as when using the statistical approach, all that we need to store during verification is the current state.

n:   Model:   MTBDD:   Construction:
States: Transitions: Nodes: Leaves: Time (s): Iter.s:
220 53 68 50.0016
4216 921 267 50.01 14
81904 9,377 627 50.08 30
1615840 82,737 1,326 50.37 62
32128960 691,793 2,749 51.75 126
641.0e+06 5.7e+06 5,716 58.37 254
1288.3e+06 4.6e+07 11,963539.18510

Experimental Results

The objective is for the robot to reach the goal square at top right corner within 100 time units with probability at least 0.9, while maintaining at least a 0.5 probability of periodically communicating with the base station. The CSL formula:

P>=0.9 [ (P>=0.5 [ true U<=7 communicate ]) U<=100 goal ]

expresses the given objective.

In the numerical method we set the truncation error to 1e-6 (stop iterating when the relative error between the iteration vectors is less than 1e-6). On the other hand, when using the statistical approach, the parameters α, β, and δ can be used to trade accuracy for efficiency (see [YS02] for details on these parameters). In the experiments we set α=β=1e-2 and vary δ.

We now report on the results when using the mixed and the numerical approaches. Note that in both methods the inner bounded until (P>=0.5 [ true U<=7 communicate ]) is verified using the numerical approach. The table and graph below compare the overall model checking times of the two approaches (the iterations and samples correspond to those used to verify the outer bounded until).

n:   Numerial   Statistical
δ=0.0025 δ=0.005 δ=0.01
time (s): iterations: average time (s): average no.
average time (s): average no.
average time (s): average no.
20.0011470.261828 0.124414 0.058207
40.01 3361.262828 0.626414 0.31 207
80.23 34410.572186 5.5431141.62.865582.4
163.97 3465.005474.42.938246.5 1.834120.5
3226.5 3379.353270.17.482133.4 6.54963.6
64202.533047.37144.945.9771.3 45.3034.7
1281677 326355.4 92 354.546 354.223

graph of results

Case Studies