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.

翻译：动态认知逻辑研究智能体知识的正式表示，以及智能体的知识如何响应信息性事件（如公开宣告）而变化。对信息性事件进行量化使我们能够询问是否可能达到某种知识状态，这在合成安全通信协议中具有重要应用。然而，即使对相当简单的信息性事件（即公开宣告）进行量化也是不可计算的：这类任意公开宣告逻辑（APAL）具有不可判定的可满足性问题。本文研究一种更简单的信息性事件，称为布尔宣告，其中宣告被限制为原子命题的布尔组合。该逻辑称为布尔任意公开宣告逻辑（BAPAL）。一篇配套论文为BAPAL提供了完备的有穷公理化系统及相关表达能力结果。本工作证明BAPAL的可满足性问题是可判定的，同时指出BAPAL不具备有限模型性质。