Temporal Boolean Games

Julian Gutierrez

Boolean games form a model of concurrent and multi-agent behaviour in which a number of agents have unique control over a set of Boolean variables. As traditionally defined, in a Boolean game the agents have goals given by propositional logic formulae they want to satisfy. This model, although theoretically interesting, does not take into account the potential dynamic, temporal behaviour of the agents in the game. In this talk, I will present an extension of the basic model of Boolean games where the agents are allowed to have goals given by temporal logic formulae. The talk will focus on the presentation of the model and some complexity results on the computation and verification of the equilibrium properties (for instance, checking the existence of Nash equilibria over plays of infinite length) of these multi-player games.