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.

---

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.