Quantitative Verification and Strategy Synthesis for Stochastic Games

This page provides supplementary material for paper "Quantitative Verification and Strategy Synthesis for Stochastic Games", by Marta Kwiatkowska and Maria Svorenova, accompanying semi-plenary talk at ECC'16.

Example

Here are PRISM-games files used for the illustrative example modelling a car autonomously reacting to hazards in an urban area:

• Model: car.prism
• Properties: car.props

Here are stochastic memory update strategies generated for multi-objective properties:

• Multi-objective total reward property (Example 5): multi_total_reward_3457.txt
• Multi-objective probabilistic LTL property (Example 6): multi_prob_ltl_0702.txt
• Mixed multi-objective property (Example 7): multi_mixed_0701357.txt

Site hosted at the Department of Computer Science, University of Oxford