Tractable model checking for fragments of higher-order coalition logic
Patrick Doherty, Barbara Dunin‐Kȩplicz, Andrzej Szałas · 2011
A number of popular logical formalisms for representing and reasoning about the abilities of teams or coalitions of agents have been proposed beginning with the Coalition Logic (CL) of Pauly. Ågotnes et al intro-duced a means of succinctly expressing quantification over coalitions with-out compromising the computational complexity of model checking in CL by introducing Quantified Coalition Logic (QCL). QCL introduces a sepa-rate logical language for characterizing coalitions in the modal operators used in QCL. Boella et al, increased the representational expressibility of such formalisms by introducing Higher-Order Coalition Logic (HCL), a monadic second-order logic with special set grouping operators. Tractable fragments of HCL suitable for efficient model checking have yet to be identified. In this paper, we relax the monadic restriction used in HCL and restrict ourselves to the diamond operator. We show how formulas us-ing the diamond operator are logically equivalent to second-order formulas.