Automated temporal equilibrium analysis: Verification and synthesis of multi-player games

Julian Gutierrez*, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)


In the context of multi-agent systems, the rational verification problem is concerned with checking which temporal logic properties will hold in a system when its constituent agents are assumed to behave rationally and strategically in pursuit of individual objectives. Typically, those objectives are expressed as temporal logic formulae which the relevant agent desires to see satisfied. Unfortunately, rational verification is computationally complex, and requires specialised techniques in order to obtain practically useable implementations. In this paper, we present such a technique. This technique relies on a reduction of the rational verification problem to the solution of a collection of parity games. Our approach has been implemented in the Equilibrium Verification Environment (EVE) system. The EVE system takes as input a model of a concurrent/multi-agent system represented using the Simple Reactive Modules Language (SRML), where agent goals are represented as Linear Temporal Logic ([Formula presented]) formulae, together with a claim about the equilibrium behaviour of the system, also expressed as an [Formula presented] formula. EVE can then check whether the [Formula presented] claim holds on some (or every) computation of the system that could arise through agents choosing Nash equilibrium strategies; it can also check whether a system has a Nash equilibrium, and synthesise individual strategies for players in the multi-player game. After presenting our basic framework, we describe our new technique and prove its correctness. We then describe our implementation in the EVE system, and present experimental results which show that EVE performs favourably in comparison to other existing tools that support rational verification.

Original languageEnglish
Article number103353
JournalArtificial Intelligence
Publication statusPublished - Oct 2020


  • Bisimulation invariance
  • Model checking
  • Multi-agent systems
  • Nash equilibrium
  • Rational verification
  • Synthesis
  • Temporal logic

ASJC Scopus subject areas

  • Language and Linguistics
  • Linguistics and Language
  • Artificial Intelligence


Dive into the research topics of 'Automated temporal equilibrium analysis: Verification and synthesis of multi-player games'. Together they form a unique fingerprint.

Cite this