PRISM-games: Verification and Strategy Synthesis for Stochastic Multi-player Games with Multiple Objectives

Marta Kwiatkowska, David Parker, Clemens Wiltsche

Research output: Contribution to journalArticlepeer-review

18 Citations (Scopus)
152 Downloads (Pure)

Abstract

PRISM-games is a tool for modelling, verification and strategy synthesis for stochastic multi-player games. These allow models to incorporate both probability, to represent uncertainty, unreliability or randomisation, and game-theoretic aspects, for systems where different entities have opposing objectives. Applications include autonomous transport, security protocols, energy management systems and many more. We provide a detailed overview of the PRISM-games tool, including its modelling and property specification formalisms, and its underlying architecture and implementation. In particular, we discuss some of its key features, which include multi-objective and compositional approaches to verification and strategy synthesis. We also discuss the scalability and efficiency of the tool and give an overview of some of the case studies to which it has been applied.
Original languageEnglish
Number of pages16
JournalInternational Journal on Software Tools for Technology Transfer
Early online date29 Nov 2017
DOIs
Publication statusE-pub ahead of print - 29 Nov 2017

Keywords

  • Quantitative verification
  • Stochastic games
  • Formal verification

Fingerprint

Dive into the research topics of 'PRISM-games: Verification and Strategy Synthesis for Stochastic Multi-player Games with Multiple Objectives'. Together they form a unique fingerprint.

Cite this