Probabilistic model checking for strategic equilibria-based decision making: advances and challenges

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, Rui Yan

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

46 Downloads (Pure)

Abstract

Game-theoretic concepts have been extensively studied in economics to provide insight into competitive behaviour and strategic decision making. As computing systems increasingly involve concurrently acting autonomous agents, game-theoretic approaches are becoming widespread in computer science as a faithful modelling abstraction. These techniques can be used to reason about the competitive or collaborative behaviour of multiple rational agents with distinct goals or objectives. This paper provides an overview of recent advances in developing a modelling, verification and strategy synthesis framework for concurrent stochastic games implemented in the probabilistic model checker PRISM-games. This is based on a temporal logic that supports finite- and infinite-horizon temporal properties in both a zero-sum and nonzero-sum setting, the latter using Nash and correlated equilibria with respect to two optimality criteria, social welfare and social fairness. We summarise the key concepts, logics and algorithms and the currently available tool support. Future challenges and recent progress in adapting the framework and algorithmic solutions to continuous environments and neural networks are also outlined.
Original languageEnglish
Title of host publication47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
EditorsStefan Szeider, Robert Ganian, Alexandra Silva
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl
Number of pages22
Volume241
ISBN (Electronic)978-3-95977-256-3
DOIs
Publication statusPublished - 22 Aug 2022
Event47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) - Vienna, Austria
Duration: 22 Aug 202226 Sept 2022
https://www.ac.tuwien.ac.at/mfcs2022/

Publication series

NameLeibniz International Proceedings in Informatics
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik
ISSN (Electronic)1868-8969

Conference

Conference47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
Country/TerritoryAustria
CityVienna
Period22/08/2226/09/22
Internet address

Keywords

  • Probabilistic model checking
  • equilibria
  • stochastic games

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Probabilistic model checking for strategic equilibria-based decision making: advances and challenges'. Together they form a unique fingerprint.

Cite this