A tool for the automated verification of Nash equilibria in concurrent games. Reactive Modules is a high-level specification language for concurrent and multi-agent systems, used in a number of practical model checking tools. Reactive Modules Games is a game-theoretic extension of Reactive Modules, in which concurrent agents in the system are assumed to act strategically in an attempt to satisfy a temporal logic formula representing their individual goal. The basic analytical concept for Reactive Modules Games is Nash equilibrium. In this paper, we describe a tool through which we can automatically verify Nash equilibrium strategies for Reactive Modules Games. Our tool takes as input a system, specified in the Reactive Modules language, a representation of players’ goals (expressed as CTL formulae), and a representation of players strategies; it then checks whether these strategies form a Nash equilibrium of the Reactive Modules Game passed as input. The tool makes extensive use of conventional temporal logic satisfiability and model checking techniques. We first give an overview of the theory underpinning the tool, briefly describe its structure and implementation, and conclude by presenting a worked example analysed using the tool.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Gutierrez, Julian; Najib, Muhammad; Perelli, Giuseppe; Wooldridge, Michael: Automated temporal equilibrium analysis: verification and synthesis of multi-player games (2020)
- Gutierrez, Julian; Harrenstein, Paul; Perelli, Giuseppe; Wooldridge, Michael: Nash equilibrium and bisimulation invariance (2019)
- Jamroga, Wojciech; Malvone, Vadim; Murano, Aniello: Natural strategic ability (2019)
- Gutierrez, Julian; Perelli, Giuseppe; Wooldridge, Michael: Imperfect information in reactive modules games (2018)
- Gutierrez, Julian; Harrenstein, Paul; Wooldridge, Michael: Reasoning about equilibria in game-like concurrent systems (2017)
- Gutierrez, Julian; Harrenstein, Paul; Wooldridge, Michael: From model checking to equilibrium checking: reactive modules for rational verification (2017)
- Svoreňová, Mária; Kwiatkowska, Marta: Quantitative verification and strategy synthesis for stochastic games (2016)
- Toumi, Alexis; Gutierrez, Julian; Wooldridge, Michael: A tool for the automated verification of Nash equilibria in concurrent games (2015)