Department of Computer Science

Foraging Robot

Introduction

We present an example, originally due to Jansen et al. in “A Probabilistic Extension of UML Statecharts”, but reinterpreted here. We consider a robot equipped with an idealised randomising device with two states that are equally likely to occur; the device generates an outcome from a flip event in every time step. The robot uses the device to decide whether to terminate or to continue a particular activity (here, foraging). For reasons of its own, the robot may choose to ignore the outcome of the device. Finally, the robot considers only a limited number of times whether to continue foraging. We call this number N and leave it loosely defined. Our simple modelling objective is to explore different values for N that give us a high probability of terminating.

Model (download)

The RoboChart model is shown below.

The only state machine FgSTM defines a constant N and a variable flips. There are two states FORAGE and STOP in the state machine.

One possibility in the FORAGE state is for the flip event to occur and the robot to remain in the FORAGE state; this models the robot ignoring the randomising device. The other possibility is available only if the number of choices has not been exhausted (flips < N). In this case, the robot controller proceeds to a probabilistic choice between two equally likely alternatives. One alternative is to move into the STOP state, which it signals with the stop event; the other alternative is to return to the FORAGE state, signalling this with the forage event. In both cases, the controller keeps track of the number of choices made. Note that, if in the FORAGE state flips < N, then the behaviour is nondeterministic: the robot controller might take either flip alternative. There is only one transition available in the STOP state: the flip event keeps the controller in the STOP state; this transition is included to model the fact that flip occurs in every time step, even when the controller has terminiated.

Analysis with assertion language

We use the probabilistic assertion language of RoboChart. The assertion language finally will be translated to the PRISM’s property langauge, but the assertion language is a more user-friendly way to verify probabilistic properties. Information about how to use the probabilistic assertion language can be found in RoboChart and RoboTool reference manuals.

Generated PRISM model (download)

Used configuration file.

Assertions (download)

The assertion file that is used for verification is shown below.

Reports

The verification results are displayed in the report below.


Results of analysis of assertions in foraging.assertions using PRISM

Assertion: P_deadlock_free

Assertion Const States Transitions Time Result
P_deadlock_free foraging::foraging::stm_ref0::N=2 16 20 0.001 seconds true
P_deadlock_free foraging::foraging::stm_ref0::N=4 30 38 0.002 seconds true
P_deadlock_free foraging::foraging::stm_ref0::N=6 44 56 0.001 seconds true
P_deadlock_free foraging::foraging::stm_ref0::N=8 58 74 0.002 seconds true
P_deadlock_free foraging::foraging::stm_ref0::N=10 72 92 0.002 seconds true
P_deadlock_free foraging::foraging::stm_ref0::N=12 86 110 0.002 seconds true
P_deadlock_free foraging::foraging::stm_ref0::N=14 100 128 0.001 seconds true
P_deadlock_free foraging::foraging::stm_ref0::N=16 114 146 0.002 seconds true
P_deadlock_free foraging::foraging::stm_ref0::N=18 128 164 0.001 seconds true
P_deadlock_free foraging::foraging::stm_ref0::N=20 142 182 0.001 seconds true

Assertion: P_nonterminate

Assertion Const States Transitions Time Result
P_nonterminate foraging::foraging::stm_ref0::N=2 16 20 0.007 seconds false
P_nonterminate foraging::foraging::stm_ref0::N=4 30 38 0.011 seconds false
P_nonterminate foraging::foraging::stm_ref0::N=6 44 56 0.013 seconds false
P_nonterminate foraging::foraging::stm_ref0::N=8 58 74 0.012 seconds false
P_nonterminate foraging::foraging::stm_ref0::N=10 72 92 0.012 seconds false
P_nonterminate foraging::foraging::stm_ref0::N=12 86 110 0.019 seconds false
P_nonterminate foraging::foraging::stm_ref0::N=14 100 128 0.019 seconds false
P_nonterminate foraging::foraging::stm_ref0::N=16 114 146 0.018 seconds false
P_nonterminate foraging::foraging::stm_ref0::N=18 128 164 0.018 seconds false
P_nonterminate foraging::foraging::stm_ref0::N=20 142 182 0.027 seconds false

Assertion: P_min_terminate

Assertion Const States Transitions Time Result
P_min_terminate foraging::foraging::stm_ref0::N=2 16 20 0.004 seconds 0.0
P_min_terminate foraging::foraging::stm_ref0::N=4 30 38 0.005 seconds 0.0
P_min_terminate foraging::foraging::stm_ref0::N=6 44 56 0.007 seconds 0.0
P_min_terminate foraging::foraging::stm_ref0::N=8 58 74 0.004 seconds 0.0
P_min_terminate foraging::foraging::stm_ref0::N=10 72 92 0.004 seconds 0.0
P_min_terminate foraging::foraging::stm_ref0::N=12 86 110 0.005 seconds 0.0
P_min_terminate foraging::foraging::stm_ref0::N=14 100 128 0.005 seconds 0.0
P_min_terminate foraging::foraging::stm_ref0::N=16 114 146 0.005 seconds 0.0
P_min_terminate foraging::foraging::stm_ref0::N=18 128 164 0.005 seconds 0.0
P_min_terminate foraging::foraging::stm_ref0::N=20 142 182 0.008 seconds 0.0

Assertion: P_max_terminate

Assertion Const States Transitions Time Result
P_max_terminate foraging::foraging::stm_ref0::N=2 16 20 0.005 seconds 0.75
P_max_terminate foraging::foraging::stm_ref0::N=4 30 38 0.008 seconds 0.9375
P_max_terminate foraging::foraging::stm_ref0::N=6 44 56 0.012 seconds 0.984375
P_max_terminate foraging::foraging::stm_ref0::N=8 58 74 0.013 seconds 0.99609375
P_max_terminate foraging::foraging::stm_ref0::N=10 72 92 0.015 seconds 0.9990234375
P_max_terminate foraging::foraging::stm_ref0::N=12 86 110 0.018 seconds 0.999755859375
P_max_terminate foraging::foraging::stm_ref0::N=14 100 128 0.017 seconds 0.99993896484375
P_max_terminate foraging::foraging::stm_ref0::N=16 114 146 0.021 seconds 0.9999847412109375
P_max_terminate foraging::foraging::stm_ref0::N=18 128 164 0.022 seconds 0.9999961853027344
P_max_terminate foraging::foraging::stm_ref0::N=20 142 182 0.031 seconds 0.9999980926513672

Assertion: R_min_stop

Assertion Const States Transitions Time Result
R_min_stop foraging::foraging::stm_ref0::N=10 72 92 0.012 seconds Infinity

Assertion: R_max_stop

Assertion Const States Transitions Time Result
R_max_stop foraging::foraging::stm_ref0::N=10 72 92 0.005 seconds Infinity

The P_max_terminate result is also shown in the diagram below.

Conclusion

This example shows how to use RoboChart to model and verify probabilistic behaviour of a simple device using RoboTool.

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500