Model checking for coalition announcement logic

Rustam Galimullin*, Natasha Alechina, Hans van Ditmarsch

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review

Abstract

Coalition Announcement Logic (CAL) studies how a group of agents can enforce a certain outcome by making a joint announcement, regardless of any announcements made simultaneously by the opponents. The logic is useful to model imperfect information games with simultaneous moves. We propose a model checking algorithm for CAL and show that the model checking problem for CAL is PSPACE-complete. We also consider a special positive case for which the model checking problem is in P. We compare these results to those for other logics with quantification over information change.

Original languageEnglish
Title of host publicationKI 2018
Subtitle of host publicationAdvances in Artificial Intelligence - 41st German Conference on AI, 2018, Proceedings
EditorsAnni-Yasmin Turhan, Frank Trollmann
PublisherSpringer Verlag
Pages11-23
Number of pages13
ISBN (Print)9783030001100
DOIs
Publication statusPublished - 2018
Externally publishedYes
Event41st German Conference on Artificial Intelligence, KI 2018 - Berlin, Germany
Duration: 24 Sept 201828 Sept 2018

Publication series

SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11117 LNAI
ISSN0302-9743

Conference

Conference41st German Conference on Artificial Intelligence, KI 2018
Abbreviated titleKI 2018
Country/TerritoryGermany
CityBerlin
Period24/09/1828/09/18

Keywords

  • Coalition announcement logic
  • Dynamic epistemic logic
  • Model checking

Fingerprint

Dive into the research topics of 'Model checking for coalition announcement logic'. Together they form a unique fingerprint.

Cite this