On the logic of cooperation and propositional control

Cooperation logics have recently begun to attract attention within the multi-agent systems community. Using a cooperation logic, it is possible to represent and reason about the strategic powers of agents and coalitions of agents in game-like multi-agent systems. These powers are generally assumed to be implicitly defined within the structure of the environment, and their origin is rarely discussed. In this paper, we study a cooperation logic in which agents are each assumed to control a set of propositional variables-the powers of agents and coalitions then derive from the allocation of propositions to agents. The basic modal constructs in this Coalition Logic of Propositional Control (cl-pc) allow us to express the fact that a group of agents can cooperate to bring about a certain state of affairs. After motivating and introducing cl-pc, we provide a complete axiom system for the logic, investigate the issue of characterising control in cl-pc with respect to the underlying power structures of the logic, and formally investigate the relationship between cl-pc and Pauly's Coalition Logic. We then show that the model checking and satisfiability problems for cl-pc are both pspace-complete, and conclude by discussing our results and how cl-pc sits in relation to other logics of cooperation.