Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Abstract

We design and implement an efficient model checking algorithm for alternating-time temporal logic (ATL) on turn-based multiplayer stochastic games with weighted transitions. This logic allows us to query about the existence of multiplayer strategies that aim to maximize the probability of game runs satisfying resource-bounded next and until logical operators, while requiring that the accumulated weight along the successful runs does not exceed a given upper bound. Our method relies on a recently introduced formalism of abstract dependency graphs (ADG) and we provide an efficient reduction of our model checking problem to finding the minimum fixed-point assignment on an ADG over the domain of unit intervals extended with certain-zero optimization. As the fixed-point computation on ADGs is performed in an on-the-fly manner without the need of a priori generating the whole graph, we achieve a performance that is comparable with state-of-the-art model checker PRISM-games for finding the exact solutions and sometimes an order of magnitude faster for queries that ask about approximate probability bounds. We document this on a series of scalable experiments from the PRISM-games benchmark that we annotate with weight information.
Original languageEnglish
Title of host publication30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'20)
Number of pages20
PublisherSpringer
Publication date2020
Pages249-268
ISBN (Print)978-3-030-68445-7
ISBN (Electronic)978-3-030-68446-4
DOIs
Publication statusPublished - 2020
Event30th International Symposium on Logic-Based Program Synthesis and Transformation - Bologna (but the event was online), Bologna, Italy
Duration: 7 Sep 20209 Sep 2020
Conference number: 30
https://nms.kcl.ac.uk/maribel.fernandez/LOPSTR2020/

Conference

Conference30th International Symposium on Logic-Based Program Synthesis and Transformation
Number30
LocationBologna (but the event was online)
Country/TerritoryItaly
CityBologna
Period07/09/202009/09/2020
Internet address
SeriesLecture Notes in Computer Science
ISSN0302-9743

Keywords

  • stochastic games, dependecy graphs, verification

Fingerprint

Dive into the research topics of 'Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs'. Together they form a unique fingerprint.

Cite this