A Logic for Global and Local Announcements

Francesco Belardinelli
(Labortoire IBISC, UEVE and IRIT Toulouse)
Hans van Ditmarsch
(LORIA – CNRS, Université de Lorraine, Vandoeuvre-lès-Nancy, France)
Wiebe van der Hoek
(Department of Computing, University of Liverpool, Liverpool, UK)

In this paper we introduce global and local announcement logic (GLAL), a dynamic epistemic logic with two distinct announcement operators – [φ]^+_A and [φ] ^-_A indexed to a subset A of the set Ag of all agents – for global and local announcements respectively. The boundary case [φ]^+_Ag corresponds to the public announcement of φ, as known from the literature. Unlike standard public announcements, which are model transformers, the global and local announcements are 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.

In Jérôme Lang: Proceedings Sixteenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2017), Liverpool, UK, 24-26 July 2017, Electronic Proceedings in Theoretical Computer Science 251, pp. 28–42.
Published: 25th July 2017.

ArXived at: https://dx.doi.org/10.4204/EPTCS.251.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org