LiU Electronic Press
Full-text not available in DiVA
Author:
Doherty, Patrick (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab) (Linköping University, The Institute of Technology)
Dunin-Keplicz, Barbara (Institute of Informatics, Warsaw University)
Szalas, Andrzej (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab) (Linköping University, The Institute of Technology)
Title:
Tractable model checking for fragments of higher-order coalition logic
Department:
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab
Linköping University, The Institute of Technology
Publication type:
Conference paper (Refereed)
Language:
English
In:
Proceedings of the 10th International Conference on Autonomous Agents and Multiagent Systems - Volume 2
Editor:
Liz Sonenberg, Peter Stone, Kagan Tumer, Pinar Yolum
Conference:
The 10th International Conference on Autonomous Agents and Multiagent Systems
Place of publ.: Richland Publisher: AAAI Press
Pages:
743-750
Year of publ.:
2011
URI:
urn:nbn:se:liu:diva-72698
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-72698
ISBN:
0-9826571-6-1, 978-0-9826571-6-4
Subject category:
Computer Science
Abstract(en) :

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 introduced a means of succinctly expressing quantification over coalitions without compromising the computational complexity of model checking in CL by introducing Quantified Coalition Logic (QCL). QCL introduces a separate 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 using the diamond operator are logically equivalent to second-order formulas. This permits us to isolate and define well-behaved expressive fragments of second-order logic amenable to model-checking in PTime. To do this, we appeal to techniques used in deductive databases and quantifier elimination. In addition, we take advantage of the monotonicity of the effectivity function resulting in exponentially more succinct representation of models. The net result is identification of highly expressible fragments of a generalized HCL where model checking can be done efficiently in PTime.

Available from:
2011-12-05
Created:
2011-12-05
Last updated:
2011-12-12
Statistics:
30 hits