This case study is based on [CKSW13] and is concerned with strategy synthesis for an autonomous vehicle in an urban setting.

Strategy synthesis for two UK villages is provided. Running

python generate.py 1  # islip
python generate.py 2  # charlton

generates the model and properties. Additionally scripts are generated to run the strategy synthesis. Executing

islip.sh
charlton.sh

starts PRISM-games and outputs the respective strategies.

For an overview, see: http://www.veriware.org/autonomous.php

=====================================================================================

[CKSW13]
Taolue Chen, Marta Kwiatkowska, Aistis Simaitis and Clemens Wiltsche.
Synthesis for Multi-Objective Stochastic Games: An Application to Autonomous Urban Driving.
In Proc. 10th International Conference on Quantitative Evaluation of SysTems (QEST'13), volume 8054 of LNCS, pages 322-337, Springer. August 2013.