liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Tractable model checking for fragments of higher-order coalition logic
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab. Linköping University, The Institute of Technology.
Institute of Informatics, Warsaw University.
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab. Linköping University, The Institute of Technology.
2011 (English)In: Proceedings of the 10th International Conference on Autonomous Agents and Multiagent Systems - Volume 2 / [ed] Liz Sonenberg, Peter Stone, Kagan Tumer, Pinar Yolum, Richland: AAAI Press, 2011, p. 743-750Conference paper, Published paper (Refereed)
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.

Place, publisher, year, edition, pages
Richland: AAAI Press, 2011. p. 743-750
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-72698ISBN: 0-9826571-6-1 (print)ISBN: 978-0-9826571-6-4 (print)OAI: oai:DiVA.org:liu-72698DiVA, id: diva2:461565
Conference
The 10th International Conference on Autonomous Agents and Multiagent Systems
Available from: 2011-12-05 Created: 2011-12-05 Last updated: 2018-01-12

Open Access in DiVA

No full text in DiVA

Other links

http://dl.acm.org/citation.cfm?id=2031723

Authority records

Doherty, PatrickSzalas, Andrzej

Search in DiVA

By author/editor
Doherty, PatrickSzalas, Andrzej
By organisation
KPLAB - Knowledge Processing LabThe Institute of Technology
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 277 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf