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

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

Standard

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

Harvard

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

APA

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

Vancouver

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

Author

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

Bibtex

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

}

RIS

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 -