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

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

Authors

Colleges, School and Institutes

External organisations

  • University of Oxford

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.

Details

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
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)
CountryNetherlands
CityEindhoven
Period2/04/168/04/16