Asynchronous Announcements
This work addresses the challenge of formalizing asynchronous message exchange in distributed systems for researchers in logic and multi-agent systems, representing an incremental extension of existing public announcement logic.
The paper tackles the problem of modeling asynchronous communication in multi-agent systems by proposing an epistemic logic where truthful announcements are sent publicly but received individually and in order, leading to beliefs that may not be truthful due to delays. It provides a complete axiomatization for this logic, showing equivalence to formulas without dynamic modalities, and includes an example from distributed computing.
We propose a multi-agent epistemic logic of asynchronous announcements, where truthful announcements are publicly sent but individually received by agents, and in the order in which they were sent. Additional to epistemic modalities the logic contains dynamic modalities for making announcements and for receiving them. What an agent believes is a function of her initial uncertainty and of the announcements she has received. Beliefs need not be truthful, because announcements already made may not yet have been received. As announcements are true when sent, certain message sequences can be ruled out, just like inconsistent cuts in distributed computing. We provide a complete axiomatization for this \emph{asynchronous announcement logic} (AA). It is a reduction system that also demonstrates that any formula in $AA$ is equivalent to one without dynamic modalities, just as for public announcement logic. A detailed example modelling message exchanging processes in distributed computing in $AA$ closes our investigation.