On the dynamics of delegation, cooperation, and control
Wiebe van der Hoek, Michael Wooldridge · 2005
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 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 affects 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.