Title: Relaxing Exclusive Control in Boolean Games,
Abstract: In the typical framework for boolean games (BG) each player can change the
truth value of some propositional atoms, while attempting to make her goal
true. In standard BG goals are propositional formulas, whereas in iterated BG
goals are formulas of Linear Temporal Logic. Both notions of BG are
characterised by the fact that agents have exclusive control over their set of
atoms, meaning that no two agents can control the same atom. In the present
contribution we drop the exclusivity assumption and explore structures where an
atom can be controlled by multiple agents. We introduce Concurrent Game
Structures with Shared Propositional Control (CGS-SPC) and show that they ac-
count for several classes of repeated games, including iterated boolean games,
influence games, and aggregation games. Our main result shows that, as far as
verification is concerned, CGS-SPC can be reduced to concurrent game structures
with exclusive control. This result provides a polynomial reduction for the
model checking problem of specifications in Alternating-time Temporal Logic on
CGS-SPC.