Model checking for coalition announcement logic

Abstract

This talk is based on joint work with Rustam Galimullin and Hans van Ditmarsh, published in the German Conference on Artificial Intelligence (KI 2018). First I will introduce background and motivation for the work. I will introduce multi-agent Epistemic Logic (EL) for representing knowledge of (idealised) agents, Public Announcement Logic (PAL) for modelling knowledge change after truthful announcements, Group Announcement Logic (GAL) for modelling what kinds of changes in other agents’ knowledge a group of agents can effect, and Coalition Announcement Logic (CAL) which is the main subject of the talk. 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. It is also useful for devising protocols of announcements that will increase some knowledge of some agents, but also preserve other agents’ ignorance with respect to some information (in other words, preserve privacy of the announcers). The main new technical result in the talk is a model checking algorithm for CAL, that is, an algorithm for evaluating a CAL formula in a given finite model. The model-checking problem for CAL is PSPACE-complete, and the protocol requires polynomial space (but exponential time). DOI: 10.21146/2074-1472-2018-24-2-59-69