Expressiveness and Nash Equilibrium in Iterated Boolean Games
Abstract
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.