www.prismmodelchecker.org
[KPW16] Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), volume 9636 of LNCS, pages 560-566, Springer. April 2016. [pdf] [bib] [Introduces version 2.0 of the PRISM-games tool.]
Downloads:  pdf pdf (274 KB)  bib bib
Notes: The original publication is available at www.springerlink.com.
Abstract. 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.

Publications