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 quantication over information change.

Citation

Galimullin, R., Alechina, N., & van Ditmarsch, H. (2018). Model checking for Coalition Announcement Logic. In F. Trollmann, & A. Turhan (Eds.), KI 2018: Advances in Artificial Intelligence, 41st German Conference on AI, Berlin, Germany, September 24–28, 2018, Proceedings (11-23). Cham: Springer Publishing Company. https://doi.org/10.1007/978-3-030-00111-7_2

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