"Symbolic Verification and Strategy Synthesis for Turn-based Stochastic Games" - Supporting Material

Paper: "Symbolic Verification and Strategy Synthesis for Turn-based Stochastic Games"
Marta Kwiatkowska, Gethin Norman, David Parker, and Gabriel Santos

A representative selection of the (turn-based) stochastic game benchmarks used in the paper are listed below.

• avoid: AV10_10.prism AV.props.prism
• dice: dice10.prism dice.props.prism
• hallway: hallway5_5.prism hallway.props.prism
• investors: two_investors.prism two_investors.props.prism
• repudiation: repudiation_honest.prism repudiation_honest.props.prism
• task graph task_graph_prob_fault.prism task_graph.props.prism
• safenav: with_robot_8x8_A.prism game_property.props.prism

For a more complete set, see the PRISM benchmark suite.

An improved version of the symbolic implementation presented in the paper is now part of PRISM-games.