A Logic for Global and Local Announcements

TL;DR

This paper introduces GLAL, a dynamic epistemic logic with global and local announcement operators, allowing for more nuanced state updates and increased expressiveness over traditional public announcement logic.

Contribution

The paper presents a novel logic with pointed model transformers for announcements, distinguishes bisimilarity notions, and proves decidability and greater expressiveness than existing public announcement logic.

Findings

GLAL can distinguish modally bisimilar states.

GLAL's update semantics produce tree-like models.

The satisfiability problem for GLAL is decidable.

Abstract

In this paper we introduce {\em global and local announcement logic} (GLAL), a dynamic epistemic logic with two distinct announcement operators -- $[\phi]^+_A$ and $[\phi]^-_A$ indexed to a subset $A$ of the set $Ag$ of all agents -- for global and local announcements respectively. The boundary case $[\phi]^+_{Ag}$ corresponds to the public announcement of $\phi$, as known from the literature. Unlike standard public announcements, which are {\em model transformers}, the global and local announcements are {\em pointed model transformers}. In particular, the update induced by the announcement may be different in different states of the model. Therefore, the resulting computations are trees of models, rather than the typical sequences. A consequence of our semantics is that modally bisimilar states may be distinguished in our logic. Then, we provide a stronger notion of bisimilarity and we show that it preserves modal equivalence in GLAL. Additionally, we show that GLAL is strictly more expressive than public announcement logic with common knowledge. We prove a wide range of validities for GLAL involving the interaction between dynamics and knowledge, and show that the satisfiability problem for GLAL is decidable. We illustrate the formal machinery by means of detailed epistemic scenarios.