PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games
Research output: Chapter in Book/Report/Conference proceeding › Conference 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 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 |
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 | Netherlands |
City | Eindhoven |
Period | 2/04/16 → 8/04/16 |