Iterated games with LDL goals over finite traces

Julian Gutierrez, Giuseppe Perelli, Michael Wooldridge

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

11 Citations (Scopus)


Linear Dynamic Logic on finite traces (LDLF) is a powerful logic for reasoning about the behaviour of concurrent and multi-Agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on LDLF. This study builds upon a generalisation of Boolean games, a logic-based game model of multi-Agent systems where players have goals succinctly represented in a logical way. Because LDLF goals are considered, in the setting we study-iterated Boolean games with goals over finite traces (iBGf)-players' goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace. In particular, using alternating automata, the paper investigates automata-Theoretic approaches to the characterisation and verification of (pure strategy Nash) equilibria, shows that the set of Nash equilibria in games with LDLF objectives is regular, and provides complexity results for the associated automata constructions.

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


  • Automata
  • Boolean games
  • Nash equilibria
  • Temporal logics

Cite this