PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games
We present a new release of PRISM-games, a tool for veri- fication 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 consumpti...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Udgivet: |
Springer
2016
|
| _version_ | 1826286669713637376 |
|---|---|
| author | Kwiatkowska, M Wiltsche, C Parker, D |
| author_facet | Kwiatkowska, M Wiltsche, C Parker, D |
| author_sort | Kwiatkowska, M |
| collection | OXFORD |
| description | We present a new release of PRISM-games, a tool for veri- fication 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. |
| first_indexed | 2024-03-07T01:47:11Z |
| format | Conference item |
| id | oxford-uuid:98d1374d-c0a3-4aa0-bf9c-67c9ddf1182b |
| institution | University of Oxford |
| last_indexed | 2024-03-07T01:47:11Z |
| publishDate | 2016 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:98d1374d-c0a3-4aa0-bf9c-67c9ddf1182b2022-03-27T00:09:44ZPRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic gamesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:98d1374d-c0a3-4aa0-bf9c-67c9ddf1182bSymplectic Elements at OxfordSpringer2016Kwiatkowska, MWiltsche, CParker, DWe present a new release of PRISM-games, a tool for veri- fication 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. |
| spellingShingle | Kwiatkowska, M Wiltsche, C Parker, D PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games |
| title | PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games |
| title_full | PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games |
| title_fullStr | PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games |
| title_full_unstemmed | PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games |
| title_short | PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games |
| title_sort | prism games 2 0 a tool for multi objective strategy synthesis for stochastic games |
| work_keys_str_mv | AT kwiatkowskam prismgames20atoolformultiobjectivestrategysynthesisforstochasticgames AT wiltschec prismgames20atoolformultiobjectivestrategysynthesisforstochasticgames AT parkerd prismgames20atoolformultiobjectivestrategysynthesisforstochasticgames |