The Undecidability of Quantified Announcements

TL;DR

This paper proves that the satisfiability problem is undecidable for several logics involving quantification over public announcements when multiple agents are involved, but remains decidable with a single agent.

Contribution

It establishes the undecidability of APAL, GAL, and CAL logics with multiple agents and corrects a previous error in their definitions.

Findings

Undecidability of satisfiability for APAL, GAL, and CAL with multiple agents.

Decidability of these logics when only a single agent is involved.

Correction of an error in the previous version's formula definition.

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.