[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.]
|
Notes:
The original publication is available at link.springer.com.
|
Links:
[Google]
[Google Scholar]
|
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.
|