We present a new release of PRISM-games, a tool for verification and strategy synthesis for stochastic games. PRISM-games 2.0 significantly extends its functionality by supporting, for the first time: (i) long-run average (mean-payoff) and ratio reward objectives, e.g., to express energy consumption per time unit; (ii) strategy synthesis and Pareto set computation for multi-objective properties; and (iii) compositional strategy synthesis, where strategies for a stochastic game modelled as a composition of subsystems are synthesised from strategies for individual components using assume-guarantee contracts on component interfaces. We demonstrate the usefulness of the new tool on four case studies from autonomous transport and energy management.
CITATION STYLE
Kwiatkowska, M., Parker, D., & Wiltsche, C. (2016). PRISM-Games 2.0: A tool for multi-objective strategy synthesis for stochastic games. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9636, pp. 560–566). Springer Verlag. https://doi.org/10.1007/978-3-662-49674-9_35
Mendeley helps you to discover research relevant for your work.