Expressiveness and Nash Equilibrium in Iterated Boolean Games

We introduce and investigate a novel notion of expressiveness related to temporal logics and game theoretic properties of multi-agent systems. We focus on iterated Boolean games, where each agent i has a goal γi, represented using (a fragment of) Linear Temporal Logic (LTL). The goal γi captures agent i's preferences: the models of γi represent system behaviours that would satisfy i, and each player is assumed to act strategically, taking into account the goals of other players, in order to bring about computations satisfying their goal. In this setting, we apply the standard game-theoretic concept of Nash equilibria: the Nash equilibria of an iterated Boolean game can be understood as a (possibly empty) set of computations, each computation representing one way the system could evolve if players chose strategies in Nash equilibrium. Such an equilibrium set of computations can be understood as expressing a temporal property---which may or may not be expressible within a particular LTL fragment. The new notion of expressiveness that we study is then as follows: What LTL properties can be expressed by the Nash equilibria of games in which agent goals are expressed in LTL fragments? We formally define and investigate this notion of expressiveness and some related issues, for a range of LTL fragments.

Full Article (PDF , ACM)