@inproceedings{ed5f60089aef472cbf26f36a8b3d73f6,
title = "PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games",
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.",
author = "Marta Kwiatkowska and David Parker and Clemens Wiltsche",
year = "2016",
month = apr,
day = "9",
doi = "10.1007/978-3-662-49674-9_35",
language = "English",
isbn = "978-3-662-49673-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
editor = "Marsha Chechik and Jean-Francois Raskin",
booktitle = "Proceedings 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16)",
note = "22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16) ; Conference date: 02-04-2016 Through 08-04-2016",
}