Model checking for Coalition Announcement Logic

Galimullin, Rustam; Alechina, Natasha; van Ditmarsch, Hans

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 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.

Citation

Galimullin, R., Alechina, N., & van Ditmarsch, H. (2018, September). Model checking for Coalition Announcement Logic. Presented at KI 2018: Advances in Artificial Intelligence, Berlin, Germany

• Presentation Conference Type: Edited Proceedings
• Conference Name: KI 2018: Advances in Artificial Intelligence
• Start Date: Sep 24, 2018
• End Date: Sep 28, 2018
• Acceptance Date: Jun 17, 2018
• Online Publication Date: Aug 30, 2018
• Publication Date: Aug 30, 2018
• Deposit Date: Nov 28, 2018
• Publicly Available Date: Aug 31, 2019
• Electronic ISSN: 1611-3349
• Publisher: Springer Publishing Company
• Pages: 11-23
• Series Title: Lecture Notes in Computer Science
• Series Number: 11117
• Series ISSN: 1611-3349
• Book Title: KI 2018: Advances in Artificial Intelligence, 41st German Conference on AI, Berlin, Germany, September 24–28, 2018, Proceedings
• ISBN: 978-3-030-00110-0
• DOI: https://doi.org/10.1007/978-3-030-00111-7_2
• Public URL: https://nottingham-repository.worktribe.com/output/1147319
• Publisher URL: https://link.springer.com/chapter/10.1007%2F978-3-030-00111-7_2