On the Dynamics of Delegation, Cooperation, and Control: A Logical Account

We present dcl-pc: a dynamic logic of delegation and cooperation. The logical foundation of dcl-pc is cl-pc, a logic for reasoning about cooperation in which the powers of agents and coalitions of agents stem from a distribution of atomic Boolean variables to individual agents -- the choices available to coalitions in cl-pc correspond to the possible truth assignments to the propositions they control. The basic modal constructs of cl-pc are of the form "coalition C can cooperate to bring about #". dcl-pc extends cl-pc with dynamic logic modalities in which atomic programs are of the form "agent i gives proposition p to agent j". By combining these dynamic delegation operators with cooperation modalities, it is possible to reason about delegation and how it a#ects the power structure within a society. We give two alternative semantics for the logic, (a "direct" semantics, in which we directly represent the distributions of atomic propositions to agents, and a more conventional Kripke semantics) , and prove that these semantics are equivalent. We then present a sound and complete axiomatization, and investigate the computational complexity of the model checking and satisfiability problems for dcl-pc