PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos

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

Abstract

We present a major new release of the PRISM-games model checker, featuring multiple significant advances in its support for verification and strategy synthesis of stochastic games. Firstly, concurrent stochastic games bring more realistic modelling of agents interacting in a concurrent fashion. Secondly, equilibria-based properties provide a means to analyse games in which competing or collaborating players are driven by distinct objectives. Thirdly, a real-time extension of (turn-based) stochastic games facilitates verification and strategy synthesis for systems where timing is a crucial aspect. This paper describes the advances made in the tool's modelling language, property specification language and model checking engines in order to implement this new functionality. We also summarise the performance and scalability of the tool, and describe a selection of case studies, ranging from security protocols to robot coordination, which highlight the benefits of the new features.
Original languageEnglish
Title of host publication32nd International Conference on Computer Aided Verification (CAV 2020), Proceedings
PublisherSpringer
Number of pages12
Publication statusAccepted/In press - 6 Apr 2020
Event32nd International Conference on Computer Aided Verification (CAV 2020) -
Duration: 19 Jul 202024 Jul 2020

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference32nd International Conference on Computer Aided Verification (CAV 2020)
Period19/07/2024/07/20

Fingerprint

Dive into the research topics of 'PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time'. Together they form a unique fingerprint.

Cite this