Iterated Games with LDL Goals on Finite Traces. Gutierrez, J., Perelli, G., & Wooldridge, M. In Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, May 8-12, 2017, pages 696–704, 2017.
Paper abstract bibtex Linear Dynamic Logic on finite traces (LDL_f) 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 LDL_f. 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 LDL_f goals are considered, in the setting we study—iterated Boolean games with goals over finite traces (iBG_f)—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 LDL_f objectives is regular, and provides complexity results for the associated automata constructions.
@inproceedings
{
C-GPW17,
author = {Julian Gutierrez and Giuseppe Perelli and Michael Wooldridge},
title = {Iterated Games with LDL Goals on Finite Traces.},
abstract = {Linear Dynamic Logic on finite traces (LDL_f) 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 LDL_f. 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 LDL_f goals are considered, in the setting we study---iterated Boolean games with goals over finite traces (iBG_f)---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 LDL_f objectives is regular, and provides complexity results for the associated automata constructions.},
booktitle = {Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, {AAMAS} 2017, S{\~{a}}o Paulo, Brazil, May 8-12, 2017},
pages = {696--704},
year = {2017},
url_paper = {https://dl.acm.org/doi/10.5555/3091125.3091225},
}