EVE: A Tool for Temporal Equilibrium Analysis

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

*Corresponding author for this work

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

19 Citations (Scopus)


We present EVE (Equilibrium Verification Environment), a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems. In EVE, systems are modelled using the Simple Reactive Module Language (SRML) as a collection of independent system components (players/agents in a game) and players’ goals are expressed using Linear Temporal Logic (LTL) formulae. EVE can be used to automatically check the existence of pure strategy Nash equilibria in such concurrent and multi-agent systems and to verify which temporal logic properties are satisfied in the equilibria.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis. ATVA 2018
EditorsChao Wang, Shuvendu K. Lahiri
Number of pages7
ISBN (Electronic)9783030010904
ISBN (Print)9783030010898
Publication statusPublished - 2018
Event16th International Symposium on Automated Technology for Verification and Analysis 2018 - Los Angeles, United States
Duration: 7 Oct 201810 Oct 2018

Publication series

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


Conference16th International Symposium on Automated Technology for Verification and Analysis 2018
Abbreviated titleATVA 2018
Country/TerritoryUnited States
CityLos Angeles

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'EVE: A Tool for Temporal Equilibrium Analysis'. Together they form a unique fingerprint.

Cite this