PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games

Marta Kwiatkowska; David Parker; Clemens Wiltsche

doi:10.1007/978-3-662-49674-9_35

PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games

Marta Kwiatkowska
, David Parker
, Clemens Wiltsche

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

22 Citations (Scopus)

281 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16)
Editors	Marsha Chechik, Jean-Francois Raskin
Publisher	Springer
Number of pages	6
ISBN (Electronic)	978-3-662-49674-9
ISBN (Print)	978-3-662-49673-2
DOIs	https://doi.org/10.1007/978-3-662-49674-9_35
Publication status	Published - 9 Apr 2016
Event	22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16) - Eindhoven, Netherlands Duration: 2 Apr 2016 → 8 Apr 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9636
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16)
Country/Territory	Netherlands
City	Eindhoven
Period	2/04/16 → 8/04/16

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Access to Document

10.1007/978-3-662-49674-9_35

Kwiatkowska_et_al_PRISM_Games_2.0_LNCS_Accepted
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-49674-9_35
Accepted author manuscript, 274 KBLicence: None: All rights reserved

Cite this

Kwiatkowska, M., Parker, D., & Wiltsche, C. (2016). PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games. In M. Chechik, & J.-F. Raskin (Eds.), Proceedings 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16) (Lecture Notes in Computer Science; Vol. 9636). Springer. https://doi.org/10.1007/978-3-662-49674-9_35

@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",

}

Kwiatkowska, M, Parker, D & Wiltsche, C 2016, PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games. in M Chechik & J-F Raskin (eds), Proceedings 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16). Lecture Notes in Computer Science, vol. 9636, Springer, 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16), Eindhoven, Netherlands, 2/04/16. https://doi.org/10.1007/978-3-662-49674-9_35

PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games. / Kwiatkowska, Marta; Parker, David; Wiltsche, Clemens.
Proceedings 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16). ed. / Marsha Chechik; Jean-Francois Raskin. Springer, 2016. (Lecture Notes in Computer Science; Vol. 9636).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games

AU - Kwiatkowska, Marta

AU - Parker, David

AU - Wiltsche, Clemens

PY - 2016/4/9

Y1 - 2016/4/9

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-49674-9_35

DO - 10.1007/978-3-662-49674-9_35

M3 - Conference contribution

SN - 978-3-662-49673-2

T3 - Lecture Notes in Computer Science

BT - Proceedings 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16)

A2 - Chechik, Marsha

A2 - Raskin, Jean-Francois

PB - Springer

T2 - 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16)

Y2 - 2 April 2016 through 8 April 2016

ER -

PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games

Abstract

Publication series

Conference

UN SDGs

Access to Document

Fingerprint

Cite this