Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

Philippe Balbiani, Hans van Ditmarsch, Clara Lerouvillois

TL;DR

This paper extends dynamic epistemic logic to asynchronous messaging by separating sending and receiving actions and tracking histories of actions, formalizing $\epsilon$-validities and $\ast$-validities. It introduces $\mathbf{AA}^{\ast}$, an infinitary axiomatisation for $\ast$-validities, and proves completeness via a canonical-model construction based on maximal consistent theories and the history-executability framework. Unlike prior $AA$, $AA^{\ast}$ does not reduce dynamic modalities to purely epistemic ones and relies on an execution-based semantics with an $\mathsf{empty}$ witness to manage histories when there are at least two agents. The work also clarifies the relation to PAL and three-valued semantics, discusses the single-agent limitations, and outlines future directions such as group epistemic modalities and non-public communication.

Abstract

We investigate a public announcement logic for asynchronous public announcements wherein the sending of the announcements by the environment is separated from the reception of the announcements by the individual agents. Both come with different modalities. In the logical semantics, formulas are interpreted in a world of a Kripke model but given a history of prior announcements and receptions of announcements that already happened. An axiomatisation AA for such a logic has been given in prior work, for the formulas that are valid when interpreted in the Kripke model before any such announcements have taken place. This axiomatisation is a reduction system wherein one can show that every formula is equivalent to a purely epistemic formula without dynamic modalities for announcements and receptions. We propose a generalisation AA* of this axiomatisation, for the formulas that are valid when interpreted in the Kripke model given any history of prior announcements and receptions of announcements. It does not extend the axiomatisation AA, for example it is no longer valid that nobody has received any announcement. Unlike AA, this axiomatisation AA* is infinitary and it is not a reduction system.

Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

TL;DR

This paper extends dynamic epistemic logic to asynchronous messaging by separating sending and receiving actions and tracking histories of actions, formalizing -validities and -validities. It introduces , an infinitary axiomatisation for -validities, and proves completeness via a canonical-model construction based on maximal consistent theories and the history-executability framework. Unlike prior , does not reduce dynamic modalities to purely epistemic ones and relies on an execution-based semantics with an witness to manage histories when there are at least two agents. The work also clarifies the relation to PAL and three-valued semantics, discusses the single-agent limitations, and outlines future directions such as group epistemic modalities and non-public communication.

Abstract

We investigate a public announcement logic for asynchronous public announcements wherein the sending of the announcements by the environment is separated from the reception of the announcements by the individual agents. Both come with different modalities. In the logical semantics, formulas are interpreted in a world of a Kripke model but given a history of prior announcements and receptions of announcements that already happened. An axiomatisation AA for such a logic has been given in prior work, for the formulas that are valid when interpreted in the Kripke model before any such announcements have taken place. This axiomatisation is a reduction system wherein one can show that every formula is equivalent to a purely epistemic formula without dynamic modalities for announcements and receptions. We propose a generalisation AA* of this axiomatisation, for the formulas that are valid when interpreted in the Kripke model given any history of prior announcements and receptions of announcements. It does not extend the axiomatisation AA, for example it is no longer valid that nobody has received any announcement. Unlike AA, this axiomatisation AA* is infinitary and it is not a reduction system.

Paper Structure

This paper contains 11 sections, 42 theorems, 25 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. The logic of asynchronous announcements
  3. Syntax
  4. Structures
  5. Semantics
  6. Some properties of the semantics
  7. Axiomatisation $\textbf{AA}^\ast$
  8. Completeness of $\textbf{AA}^\ast$
  9. Single-agent case
  10. Comparison to other works
  11. Conclusion and future research

Key Result

Lemma 5

Let $\alpha$ be a word over $\mathcal{A} \cup \mathcal{L}_{aa}$ and $\beta \sqsubseteq \alpha$ a prefix of $\alpha$. If $\alpha$ is a history, then $\beta$ is also a history.

Figures (2)

  • Figure 1: The announcement $p\vee q$ is sent, after which first Alice and then Bill receives it. States are labelled with the valuations of $p$ and $q$. States that are indistinguishable for an agent are linked with a label for that agent. We omit reflexive arrows.
  • Figure :

Theorems & Definitions (91)

  • Definition 1: Language $\mathcal{L}_{aa}$
  • Definition 2: Words
  • Definition 3: Prefix
  • Definition 4: History
  • Lemma 5
  • proof
  • Definition 6: View relation
  • Example 7
  • Proposition 8
  • Definition 9: Epistemic model
  • ...and 81 more