A tool for the automated verification of Nash equilibria in concurrent games

Alexis Toumi, Julian Gutierrez, Michael Wooldridge

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

23 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computing – ICTAC 2015
Subtitle of host publication12th International Colloquium Cali, Colombia, October 29–31, 2015 Proceedings
EditorsMartin Leucker, Camilo Rueda, Frank D. Valencia
Place of PublicationCham Switzerland
Number of pages12
ISBN (Electronic)9783319251509
ISBN (Print)9783319251493
Publication statusPublished - 2015
Externally publishedYes
EventInternational Colloquium on Theoretical Aspects of Computing 2015 - Cali, Colombia
Duration: 29 Oct 201531 Oct 2015
Conference number: 12th

Publication series

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


ConferenceInternational Colloquium on Theoretical Aspects of Computing 2015
Abbreviated titleICTAC 2015
Internet address

Cite this