PRISM-games: a model checker for stochastic multi-player games. We present PRISM-games, a model checker for stochastic multi-player games, which supports modelling, automated verification and strategy synthesis for probabilistic systems with competitive or cooperative behaviour. Models are described in a probabilistic extension of the Reactive Modules language and properties are expressed using rPATL, which extends the well-known logic ATL with operators to reason about probabilities, various reward-based measures, quantitative properties and precise bounds. The tool is based on the probabilistic model checker PRISM, benefiting from its existing user interface and simulator, whilst adding novel model checking algorithms for stochastic games, as well as functionality to synthesise optimal player strategies, explore or export them, and verify other properties under the specified strategy.

References in zbMATH (referenced in 19 articles , 1 standard article )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Bersani, Marcello M.; Soldo, Matteo; Menghi, Claudio; Pelliccione, Patrizio; Rossi, Matteo: PuRSUE -- from specification of robotic environments to synthesis of controllers (2020)
  2. Fraser, Douglas; Giaquinta, Ruben; Hoffmann, Ruth; Ireland, Murray; Miller, Alice; Norman, Gethin: Collaborative models for autonomous systems controller synthesis (2020)
  3. Gutierrez, Julian; Najib, Muhammad; Perelli, Giuseppe; Wooldridge, Michael: Automated temporal equilibrium analysis: verification and synthesis of multi-player games (2020)
  4. Jamroga, Wojciech; Konikowska, Beata; Kurpiewski, Damian; Penczek, Wojciech: Multi-valued verification of strategic ability (2020)
  5. Zaw, Hein Htoo; Hlaing, Swe Zin: Verifying the gaming strategy of self-learning game by using PRISM-games (2020)
  6. Gutierrez, Julian; Harrenstein, Paul; Perelli, Giuseppe; Wooldridge, Michael: Nash equilibrium and bisimulation invariance (2019)
  7. Jamroga, Wojciech; Malvone, Vadim; Murano, Aniello: Natural strategic ability (2019)
  8. Basset, N.; Kwiatkowska, M.; Wiltsche, C.: Compositional strategy synthesis for stochastic games with multiple objectives (2018)
  9. Drechsler, Rolf (ed.): Formal system verification. State-of the-art and future trends (2018)
  10. Gutierrez, Julian; Harrenstein, Paul; Wooldridge, Michael: Reasoning about equilibria in game-like concurrent systems (2017)
  11. Hahn, Ernst Moritz; Schewe, Sven; Turrini, Andrea; Zhang, Lijun: Synthesising strategy improvement and recursive algorithms for solving 2.5 player parity games (2017)
  12. Chen, Taolue; Primiero, Giuseppe; Raimondi, Franco; Rungta, Neha: A computationally grounded, weighted doxastic logic (2016)
  13. Svoreňová, Mária; Kwiatkowska, Marta: Quantitative verification and strategy synthesis for stochastic games (2016)
  14. Dräger, Klaus; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Ujma, Mateusz: Permissive controller synthesis for probabilistic systems (2015)
  15. Dehnert, Christian; Gebler, Daniel; Volpato, Michele; Jansen, David N.: On abstraction of probabilistic systems (2014)
  16. Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis: PRISM-games: a model checker for stochastic multi-player games (2013)
  17. Kwiatkowska, Marta: Advances in quantitative verification for ubiquitous computing (2013)
  18. Kwiatkowska, Marta; Parker, David: Automated verification and strategy synthesis for probabilistic systems (2013)
  19. Piterman, Nir (ed.); Smolka, Scott A. (ed.): Tools and algorithms for the construction and analysis of systems. 19th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings (2013)