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

Marta Kwiatkowska, David Parker, Clemens Wiltsche

Research output: Chapter in Book/Report/Conference proceedingConference contribution

22 Citations (Scopus)
181 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 languageEnglish
Title of host publicationProceedings 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16)
EditorsMarsha Chechik, Jean-Francois Raskin
PublisherSpringer
Number of pages6
ISBN (Electronic)978-3-662-49674-9
ISBN (Print)978-3-662-49673-2
DOIs
Publication statusPublished - 9 Apr 2016
Event22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16) - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9636
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 16)
Country/TerritoryNetherlands
CityEindhoven
Period2/04/168/04/16

Fingerprint

Dive into the research topics of 'PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games'. Together they form a unique fingerprint.

Cite this