Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Undecidability of Quantified Announcements

Thomas Ågotnes, Hans van Ditmarsch, Tim French

TL;DR

This work proves the undecidability of quantified announcement logics APAL, GAL, and CAL by reducing an undecidable tiling problem to their satisfiability via a grid-encoding construction implemented with two agents. A SAT$_oldsymbol{ au}$-type encoding enforces a checkerboard grid and tile-adjacency constraints, with local and global conditions realized through tailored formulas; due to the logics' different quantifications, the authors develop $n$-$oldsymbol{ ext{Pi}}$-bisimulation based approximations (CB$_{APA}$, CB$_{GA}$, CB$_{CA}$) to simulate the necessary global grid properties for APAL, GAL, and CAL. They establish both directions of the reduction: if $oldsymbol{ au}$ can tile the plane, a corresponding model satisfies SAT$_oldsymbol{ au}$ together with the CB constraints; conversely, satisfiability of SAT$_oldsymbol{ au}$ and the checkerboard constraints yields a valid tiling. The paper also notes that the single-agent fragments are decidable and discusses potential decidable variants and broader implications for epistemic planning and security protocols.

Abstract

This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents (this group may be a proper subset of the set of all agents) all of which are simultaneously (and publicly) making known announcements. So this is more restrictive than APAL. Finally, CAL is as GAL except that we now quantify over anything the agents not in that group may announce simultaneously as well. The logic CAL therefore has some features of game logic and of ATL. We show that when there are multiple agents in the language, the satisfiability problem is undecidable for APAL, GAL, and CAL. In the single agent case, the satisfiability problem is decidable for all three logics. This paper corrects an error to the submitted version of Undecidability of Quantified Announcements, identified by Yuta Asami . The nature of the error was in the definition of the formula $cga(X)$ (see Subsection 5.2) which is corrected in this version.

The Undecidability of Quantified Announcements

TL;DR

This work proves the undecidability of quantified announcement logics APAL, GAL, and CAL by reducing an undecidable tiling problem to their satisfiability via a grid-encoding construction implemented with two agents. A SAT-type encoding enforces a checkerboard grid and tile-adjacency constraints, with local and global conditions realized through tailored formulas; due to the logics' different quantifications, the authors develop --bisimulation based approximations (CB, CB, CB) to simulate the necessary global grid properties for APAL, GAL, and CAL. They establish both directions of the reduction: if can tile the plane, a corresponding model satisfies SAT together with the CB constraints; conversely, satisfiability of SAT and the checkerboard constraints yields a valid tiling. The paper also notes that the single-agent fragments are decidable and discusses potential decidable variants and broader implications for epistemic planning and security protocols.

Abstract

This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents (this group may be a proper subset of the set of all agents) all of which are simultaneously (and publicly) making known announcements. So this is more restrictive than APAL. Finally, CAL is as GAL except that we now quantify over anything the agents not in that group may announce simultaneously as well. The logic CAL therefore has some features of game logic and of ATL. We show that when there are multiple agents in the language, the satisfiability problem is undecidable for APAL, GAL, and CAL. In the single agent case, the satisfiability problem is decidable for all three logics. This paper corrects an error to the submitted version of Undecidability of Quantified Announcements, identified by Yuta Asami . The nature of the error was in the definition of the formula (see Subsection 5.2) which is corrected in this version.
Paper Structure (5 sections, 1 theorem, 3 equations, 2 figures)

This paper contains 5 sections, 1 theorem, 3 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Overview of the paper
  3. Syntax and semantics
  4. Tilings
  5. $n$-Bisimulation

Key Result

Lemma 4.2

Let $\Pi$ be a finite set of propositional atoms. Suppose that $M = (S,\sim, V)$ and $s\in S$. Then for all $n$, there is some $\mathcal{L}_{el}$ formula, $\phi$, such that for all $t\in S$, $M_t\models\phi$ if and only if $t\in\|s\|_{n}^\Pi$.

Figures (2)

  • Figure 1: Top transition: An announcement of the value of $p\vee q$ that cannot be made by Anne or Bill. Middle transition: Anne announces the value of $p$. Bottom transitions: Bill announces the value of $q$, after which Anne announces the value of $p$.
  • Figure 2: An informal representation of the scenario in Example \ref{['finApproxEG']}. The $\phi$-world is the root of the structure, the link from the root to the $b$-accessible world is dotted, whereas the links to $a$-accessible worlds are dashed. As the $\psi_i$ become increasingly complex, the structures attached to $v_{\psi_i}$ (from left to right) become an increasingly accurate approximation of the real structure in $u$.

Theorems & Definitions (6)

  • Example 2.1
  • Example 2.2
  • Definition 3.1
  • Definition 4.1
  • Lemma 4.2
  • proof