Iterated Boolean games for rational verification

Tong Gao, Julian Gutierrez, Michael Wooldridge

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

6 Citations (Scopus)


Rational verification is the problem of understanding what temporal logic properties hold of a multi-Agent system when agents are modelled as players in a game, each acting rationally in pursuit of personal preferences. More specifically, rational verification asks whether a given property, expressed as a temporal logic formula, is satisfied in a computation of the system that might be generated if agents within the system choose strategies for selecting actions that form a Nash equilibrium. We show that, when agents are mod-elled using the Simple Reactive Modules Language, a widely-used system modelling language for concurrent and multi-Agent systems, this problem can be reduced to a simpler query: Whether some iterated game-in which players have control over a finite set of Boolean variables and goals expressed as Linear Temporal Logic (LTL) formulae-has a Nash equilibrium. To better understand the complexity of solving this kind of verification problem in practice, we then study the two-player case for various types of LTL goals, present some experimental results, and describe a general technique to implement rational verification using MCMAS, a model checking tool for the verification of concurrent and multi-Agent systems.

Original languageEnglish
Title of host publicationProceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems
EditorsSanmay Das, Ed Durfee
Place of PublicationNew York NY USA
PublisherAssociation for Computing Machinery (ACM)
Number of pages9
ISBN (Electronic)9781510855076
Publication statusPublished - 2017
Externally publishedYes
EventInternational Conference on Autonomous Agents and Multiagent Systems 2017 - Sao Paulo, Brazil
Duration: 8 May 201712 May 2017
Conference number: 16th (Proceedings)


ConferenceInternational Conference on Autonomous Agents and Multiagent Systems 2017
Abbreviated titleAAMAS 2017
CitySao Paulo
Internet address


  • Formal verification
  • Iterated boolean games
  • Linear temporal logic
  • Nash equilibria
  • Strategy logic

Cite this