TY - JOUR
T1 - Expressiveness and Nash equilibrium in iterated Boolean games
AU - Gutierrez, Julian
AU - Harrenstein, Paul
AU - Perelli, Giuseppe
AU - Wooldridge, Michael
N1 - Funding Information:
This is an extensively revised and reorganised version of our paper that was presented at the 15th International Conference on Autonomous Agents and Multiagent Systems (AAMAS’16) [Gutierrez et al. 2016]. All authors acknowledge with gratitude the financial support of ERC Advanced Investigator Grant 291528 (“RACE”) at the University of Oxford. Paul Harrenstein was also supported in part by ERC Starting Grant 639945 (“ACCORD”) also at the University of Oxford. Michael Wooldridge and Paul Harrenstein furthermore acknowledge the financial support of the Alan Turing Institute in London. Giuseppe Perelli acknowledges the support of the project ERC Advanced Grant 834228 (“WhiteMech”) and the EU ICT-48 2020 project TAILOR (No. 952215). Authors’ addresses: J. Gutierrez, Department of Data Science and AI. 26 Ancora Imparo Way, Clayton campus, Melbourne, Australia; email: [email protected]; P. Harrenstein, Department of Computer Science, University of Oxford. Wolfson Building, Parks Road, Oxford OX1 3QD, UK; email: [email protected]; G. Perelli, Department of Computer, Automation, and Business Engineering. Via Ariosto, 25, Rome, Italy; email: [email protected]; M. Woldridge, Department of Computer Science, University of Oxford. Wolfson Building, Parks Road, Oxford OX1 3QD, UK; email: [email protected]. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. © 2021 Association for Computing Machinery. 1529-3785/2021/06-ART8 $15.00 https://doi.org/10.1145/3439900
Publisher Copyright:
© 2021 Association for Computing Machinery.
PY - 2021/6/8
Y1 - 2021/6/8
N2 - We define and investigate a novel notion of expressiveness for temporal logics that is based on game theoretic equilibria of multi-agent systems. We use iterated Boolean games as our abstract model of multi-agent sys- tems [Gutierrez et al. 2013, 2015a]. In such a game, each agent i has a goal γi , represented using (a fragment of) Linear Temporal Logic (LTL). The goal γi captures agent i’s preferences, in the sense that the models of γi represent system behaviours that would satisfy i. Each player controls a subset of Boolean variables Φi , and at each round in the game, player i is at liberty to choose values for variables Φi in any way that she sees fit. Play continues for an infinite sequence of rounds, and so as players act they collectively trace out a model for LTL, which for every player will either satisfy or fail to satisfy their goal. Players are assumed to act strategically, taking into account the goals of other players, in an attempt to bring about computations satisfying their goal. In this setting, we apply the standard game-theoretic concept of (pure) Nash equilibria. The (possibly empty) set of Nash equilibria of an iterated Boolean game can be understood as inducing a set of computations, each computation representing one way the system could evolve if players chose strategies that together constitute a Nash equilibrium. Such a set of equilibrium computations expresses a temporal property—which may or may not be expressible within a particular LTL fragment. The new notion of expres- siveness that we formally define and investigate is then as follows: What temporal properties are characterised by the Nash equilibria of games in which agent goals are expressed in specific fragments of LTL? We formally define and investigate this notion of expressiveness for a range of LTL fragments. For example, a very natural question is the following: Suppose we have an iterated Boolean game in which every goal is represented using a particular fragment L of LTL: is it then always the case that the equilibria of the game can be characterised within L? We show that this is not true in general.
AB - We define and investigate a novel notion of expressiveness for temporal logics that is based on game theoretic equilibria of multi-agent systems. We use iterated Boolean games as our abstract model of multi-agent sys- tems [Gutierrez et al. 2013, 2015a]. In such a game, each agent i has a goal γi , represented using (a fragment of) Linear Temporal Logic (LTL). The goal γi captures agent i’s preferences, in the sense that the models of γi represent system behaviours that would satisfy i. Each player controls a subset of Boolean variables Φi , and at each round in the game, player i is at liberty to choose values for variables Φi in any way that she sees fit. Play continues for an infinite sequence of rounds, and so as players act they collectively trace out a model for LTL, which for every player will either satisfy or fail to satisfy their goal. Players are assumed to act strategically, taking into account the goals of other players, in an attempt to bring about computations satisfying their goal. In this setting, we apply the standard game-theoretic concept of (pure) Nash equilibria. The (possibly empty) set of Nash equilibria of an iterated Boolean game can be understood as inducing a set of computations, each computation representing one way the system could evolve if players chose strategies that together constitute a Nash equilibrium. Such a set of equilibrium computations expresses a temporal property—which may or may not be expressible within a particular LTL fragment. The new notion of expres- siveness that we formally define and investigate is then as follows: What temporal properties are characterised by the Nash equilibria of games in which agent goals are expressed in specific fragments of LTL? We formally define and investigate this notion of expressiveness for a range of LTL fragments. For example, a very natural question is the following: Suppose we have an iterated Boolean game in which every goal is represented using a particular fragment L of LTL: is it then always the case that the equilibria of the game can be characterised within L? We show that this is not true in general.
KW - Concurrent games
KW - Expressiveness
KW - Game theory
KW - Logic
KW - Multi-agent systems
KW - Nash equilibrium
UR - http://www.scopus.com/inward/record.url?scp=85127375910&partnerID=8YFLogxK
U2 - 10.1145/3439900
DO - 10.1145/3439900
M3 - Article
SN - 1529-3785
VL - 22
JO - ACM Transactions on Computational Logic
JF - ACM Transactions on Computational Logic
IS - 2
M1 - 3439900
ER -