Reasoning About the Transfer of Control

We present DCL-PC: a logic for reasoning about how the abilities of agents and coalitions of agents are altered by transferring control from one agent to another. The logical foundation of DCL-PC is CL-PC, a logic for reasoning about cooperation in which the abilities of agents and coalitions of agents stem from a distribution of atomic Boolean variables to individual agents – the choices available to a coalition correspond to assignments to the variables the coalition controls. 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 control of variable p to agent j’; as usual in dynamic logic, these atomic programs may be combined using sequence, iteration, choice, and test operators to form complex programs. By combining such dynamic transfer programs with cooperation modalities, it becomes possible to reason about how the po...

• Type: Journal
• Year: 2010
• Where: JAIR
• Authors: Wiebe van der Hoek, Dirk Walther, Michael Wooldridge
• Keywords: Coalition, Dynamic Logic, JAIR 2010, Logic