Expressiveness and Nash equilibrium in iterated Boolean games

Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli, Michael Wooldridge

Research output: Contribution to journalArticleResearchpeer-review


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.
Original languageEnglish
Article number3439900
Number of pages38
JournalACM Transactions on Computational Logic
Issue number2
Publication statusPublished - 8 Jun 2021


  • Concurrent games
  • Expressiveness
  • Game theory
  • Logic
  • Multi-agent systems
  • Nash equilibrium

Cite this