Satisfiability of Quantified Boolean Announcements
Abstract
Dynamic epistemic logics consider formal representations of agents' knowledge, and how the knowledge of agents changes in response to informative events, such as public announcements. Quantifying over informative events allows us to ask whether it is possible to achieve some state of knowledge, and has important applications in synthesising secure communication protocols. However, quantifying over quite simple informative events, public announcements, is not computable: such an arbitrary public announcement logic, APAL, has an undecidable satisfiability problem. Here we consider even simpler informative events called Boolean announcements, where announcements are restricted to be a Boolean combination of atomic propositions. The logic is called Boolean arbitrary public announcement logic, BAPAL. A companion paper provides a complete finitary axiomatization, and related expressivity results, for BAPAL. In this work the satisfiability problem for BAPAL is shown to decidable, and also that BAPAL does not have the finite model property.
Cite
@article{arxiv.2206.00903,
title = {Satisfiability of Quantified Boolean Announcements},
author = {Hans van Ditmarsch and Tim French and Rustam Galimullin},
journal= {arXiv preprint arXiv:2206.00903},
year = {2025}
}
Comments
The authors regret that the proof of decidability of satisfiability of BAPAL in the previous versions contains errors and they have not been able to correct these errors. We still believe that it is likely that BAPAL is decidable, and we would like to encourage readers to show this independently. The lack of finite model property for BAPAL holds