论文标题
量化布尔公告的满意度
Satisfiability of Quantified Boolean Announcements
论文作者
论文摘要
动态认知逻辑考虑了代理人知识的形式表示，以及代理商的知识如何在响应信息性事件的响应中发生变化，例如公开公告。量化有关信息性事件的量化使我们能够询问是否有可能达到某种知识状态，并在合成安全的通信协议中具有重要的应用。但是，对非常简单的信息事件进行量化，公开公告是不可计算的：这种任意的公开公告逻辑，APAL存在一个不可确定的可满足性问题。在这里，我们考虑更简单的信息，称为布尔公告，其中公告仅限于原子命题的布尔组合。该逻辑称为布尔值任意公告逻辑Bapal。伴侣论文为巴帕尔提供了完整的限制性公理化和相关的表达结果。在这项工作中，Bapal的满足性问题被证明是可决定的，并且Bapal也没有有限的模型属性。
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.
