Rational verification: from model checking to equilibrium checking

Michael Wooldridge, Julian Gutierrez, Paul Harrenstein, Enrico Marchioni, Giuseppe Perelli, Alexis Toumi

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

44 Citations (Scopus)


Rational verification is concerned with establishing whether a given temporal logic formula φ is satisfied in some or all equilibrium computations of a multi-agent system - that is, whether the system will exhibit the behaviour φ under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the framework of rational verification, we present formal models through which rational verification can be studied, and survey the complexity of key decision problems.We give an overview of a prototype software tool for rational verification, and conclude with a discussion and related work.

Original languageEnglish
Title of host publicationProceedings of the Thirtieth AAAI Conference on Artificial Intelligence
EditorsDale Schuurmans, Michael Wellman
Place of PublicationPalo Alto CA USA
PublisherAssociation for the Advancement of Artificial Intelligence (AAAI)
Number of pages7
ISBN (Electronic)9781577357605
Publication statusPublished - 2016
Externally publishedYes
EventAAAI Conference on Artificial Intelligence 2016 - Phoenix Convention Center, Phoenix, United States of America
Duration: 12 Feb 201617 Feb 2016
Conference number: 30th


ConferenceAAAI Conference on Artificial Intelligence 2016
Abbreviated titleAAAI 2016
Country/TerritoryUnited States of America
Internet address


  • multi-agent systems
  • game theory
  • temporal logic
  • model checking
  • equilibrium checking
  • rational verification
  • synthesis

Cite this