Room 327

Asynchronous announcements

Hans van Ditmarch

CNRS-INRIA-LORIA, Nancy, France

*** PLEASE NOTE CHANGE IN TIME: SEMINAR IS AT 2 PM ***
We propose a multi-agent epistemic logic of asynchronous announcements, where truthful announcements are publicly sent but individually received by agents uncertain about atomic propositions describing the state of the world, and about each other's uncertainty. Additional to epistemic modalities, the logic therefore contains two types of dynamic modalities, namely for sending messages and for receiving messages. The semantics defines truth relative to the current state of reception of messages for all agents, where we assume that messages are received in the order in which they are being sent. What an agent knows is a function of her initial uncertainty and of the messages she has received so far. More precisely: after an announcement an agent knows that a proposition is true, if and only if on condition of the truth of that announcement, the agent knows that after that announcement and after any number of other agents also receiving it, the proposition is true. Knowledge need not be truthful, because some messages that were already sent may not yet have been received by the knowing agent, so that her knowledge may be outdated. Interestingly, messages that are announcements may result in partial synchronization, namely when an agent learns from receiving an announcement that prior announcements must already have been received by other agents.

We show that on multi-agent epistemic models (with arbitrary accessibility relations), each formula in asynchronous announcement logic is equivalent to a formula in basic multi-agent modal logic, and we provide a complete axiomatization, and also on the class of S5 models (for initial uncertainty of agents). We then determine the complexity of model checking and of satisfiability. As is maybe to be expected, your uncertainty about other agents having received messages increases the complexity of the logic in comparison to standard public announcement logic.

This is joint work with Philippe Balbiani and Ramanujam.


further information:

Hans van Ditmarsch is a long-term visitor at ReLaX from January until June 2018. ReLaX is an international joint research unit of CNRS, Université de Bordeaux, École Normale Supérieure Paris-Saclay, Chennai Mathematical Institute and the Institute of Mathematical Sciences. As a CNRS unit, ReLaX is CNRS UMI 2000. It is attached to the INS2I (Institute for Information Sciences). ReLaX was created on January 1, 2017. Its director is Madhavan Mukund. Its deputy director is Pascal Weil.