💻 computer science

Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

本文提出了一种用于异步认知逻辑的无穷公理化系统 AA*，该系统能够处理任意消息发送与接收的历史，通过摒弃归约系统方法以及“未接收任何消息”的假设，对先前的研究进行了推广。

原作者： Philippe Balbiani, Hans van Ditmarsch, Clara Lerouvillois

发布于 2026-04-29

📖 1 分钟阅读☕ 轻松阅读

原作者： Philippe Balbiani, Hans van Ditmarsch, Clara Lerouvillois

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一群朋友试图解开一个谜团，但他们通过一个非常奇怪、故障频发的消息应用进行交流。这个应用存在两个截然不同的问题：

“发送”按钮和“接收”按钮位于不同的星球上。 爱丽丝按下“发送”并不意味着鲍勃会立即收到消息。事实上，鲍勃可能要过几个小时才能收到，或者他可能在爱丽丝甚至还没打完下一句话之前就收到了。
每个人都在猜测时间线。 爱丽丝不知道鲍勃是否已经读了她的消息，是否即将阅读，或者是否完全不知道它的存在。她也不知道鲍勃是否收到了她尚未看到的“其他”消息。

本文旨在构建一套规则手册（一种逻辑），以精确描述爱丽丝在这个混乱的异步世界中究竟知道什么。

核心问题：“快照”与“电影”

在大多数逻辑谜题中，所有人都在同一时刻处于同一页面上。如果爱丽丝说“正在下雨”，每个人都会瞬间听到。这就像给房间拍了一张快照；每个人都看到了相同的画面。

但在现实世界（以及计算机网络）中，交流是一部电影。

发送就像导演大喊“开拍！”
接收就像演员听到指令。
“历史”就是迄今为止发生的所有事情的剧本。

作者菲利普、汉斯和克拉拉提出了这样一个问题：当每个人的“剧本”（消息历史）都不同时，我们该如何编写关于知识的规则手册？

他们创建的两类规则

本文提出了两种不同的编写规则的方式，具体取决于你如何审视这个故事。

1. “全新开始”规则（空历史）

想象这群人刚刚相遇。还没有发送任何消息。“剧本”是空白的。

规则： 如果我们从零开始，我们可以简化规则。我们可以将任何关于“消息发送后会发生什么”的复杂句子，翻译成关于“当前什么为真”的简单句子。
类比： 这就像下国际象棋，你仅根据当前的棋盘就能预测下一步棋。你不需要记住整盘棋的历史就能知道规则。作者将这种系统称为AA。它是一个“归约系统”，意味着它将复杂问题缩减为简单问题。

2. “任意时刻”规则（无限历史）

现在，想象这群人已经交谈了几天。爱丽丝收到了 5 条消息，鲍勃收到了 3 条，查理收到了 7 条。他们都在查看剧本的不同部分。

问题： “全新开始”的规则在这里行不通。你无法简化规则，因为历史太过混乱。爱丽丝可能知道鲍勃不知道的事情，仅仅因为她收到了一条他尚未看到的消息。
新规则： 作者创建了一套新的、复杂得多的规则手册，称为AA*。
难点： 这套规则手册是无限大的。你无法再将复杂句子缩减为简单句子。你必须接受某些规则过于复杂而无法简化这一事实。
“空”检查： 为了使这成为可能，他们发明了一种特殊的“魔法检查”，称为 empty。这个检查询问：“现在的剧本是完全空白的吗？”
- 如果答案是是，我们可以使用简单规则。
- 如果答案是否（在对话进行中通常都是这种情况），我们就必须使用复杂的、无限的规则。

为什么这很难？（“单人”问题）

当组里只有一个人时，本文遇到了瓶颈。

隐喻： 想象爱丽丝是宇宙中唯一的人。她给自己发了一条消息。
问题： 在一个群体中，爱丽丝知道她没有收到消息，因为她没看到它，并且她知道鲍勃可能收到了。但如果爱丽丝是独自一人，她无法区分“我还没收到消息”和“从未发送过消息”。
结果： 作者承认他们尚未解决单人的规则手册问题。他们用于群体的技巧（检查每个人是否知道历史为空）在只有一个人时会失效。他们说：“我们需要一种新方法来解决这个问题，也许以后吧。”

“三值”转折

本文提到了关于“真值”的一个有趣之处。

在普通逻辑中，一个陈述要么为真，要么为假。
在这个异步世界中，一个陈述可以是未定义的。
类比： 想象爱丽丝正在等待一个包裹。
- 如果包裹到了，陈述“我有包裹”为真。
- 如果包裹丢了，它就是假。
- 但如果包裹正在运输途中，而她不知道它是正在送来还是已经丢失，那么这个陈述就是未定义的。
作者的逻辑谨慎地处理了这种“未定义”状态。这不仅仅是一个错误；它是异步知识运作方式的一个基本组成部分。

总结

本文是一次数学尝试，旨在描绘当你不知道别人知道什么，也不知道他们何时获得信息时，你所知道的内容。

如果你从头开始： 你可以简化规则。
如果你正处于混乱的对话中： 你需要一套庞大且无限的、无法简化的规则集。
如果你独自一人： 当前的规则会失效，我们需要新的想法。

作者成功地为群体构建了“无限规则手册”（AA*），证明了即使在消息在不同时间到达的混乱、异步世界中，我们仍然可以在逻辑上描述每个人都知道什么。

以下是 Balbiani、van Ditmarsch 和 Lerouvillois 的论文《带有消息发送与接收的异步认知逻辑的公理化》的详细技术总结。

1. 问题陈述

本文探讨了在动态认知逻辑（DEL）中利用多智能体系统对异步通信进行建模的挑战。

差距所在： 标准的 DEL（例如公共宣告逻辑）将通信视为瞬时且同步的：消息被发送并被所有智能体同时接收。这无法捕捉现实世界分布式系统中的情况，即发送和接收是发生在不同时间的独立事件。
具体挑战： 作者旨在形式化一种逻辑，其中：
1. 智能体对消息历史存在时间不确定性（他们不知道其他人接收了多少消息）。
2. 智能体对世界状态存在认知不确定性。
3. 该逻辑必须区分消息的发送（广播）与消息的接收（个体行动）。
4. 系统必须处理两种语境下的有效性：
  - $\epsilon$ -有效性：在初始状态（空历史）下的真值。
  - $\ast$ -有效性（恒真性）：在给定任何发送和接收历史的情况下，在任何状态下的真值。

先前的工作（特别是参考文献 [4]）使用归约系统（将动态模态归约为静态认知模态）为 $\epsilon$ -有效性提供了公理化（$AA $）。然而，这种归约方法对$ \ast$-有效性失效，因为一旦存在历史，系统的性质就会发生根本性变化（例如，智能体可能接收了不同数量的消息）。

2. 方法论

2.1 语言与语法

作者定义了一种语言 $\mathcal{L}$ ，在多方模态逻辑的基础上扩展了两种类型的动态模态：

广播： $\langle \varphi \rangle \psi$ （公式 $\varphi$ 被宣告/广播；随后 $\psi$ 成立）。
接收： $\langle a \rangle \psi$ （智能体 $a$ 接收其队列中的下一条消息；随后 $\psi$ 成立）。
历史词： 智能体和公式的序列（例如 $p.a.q$ ）表示事件序列。历史是一个词，其中对于每个智能体，接收的消息数量从未超过发送的消息数量（FIFO 约束）。

2.2 语义

语义定义在配对 $(s, \alpha)$ 上，其中 $s$ 是克里普克模型中的状态， $\alpha$ 是历史词。

可执行性（ $\triangleright\triangleleft$ ）： 一种关系，用于确定历史 $\alpha$ $α$ 是否可在状态 $s$ $s$ 中执行。这确保了：
1. 历史是有效序列（FIFO）。
2. 所有被宣告的公式在其广播时刻均为真。
3. 智能体仅考虑那些在他们认为可能的状态中可执行的历史。
视图关系（ $\triangleright_a$ ）： 定义了智能体 $a$ 认为可能的事物。如果智能体 $a$ 在历史 $\beta$ 中接收的消息序列与其在历史 $\alpha$ 中接收的完全匹配，则智能体 $a$ 认为相对于实际历史 $\alpha$ ，历史 $\beta$ 是可能的。关键在于，智能体不会设想包含他们尚未接收到的消息的历史。
三值色彩： 语义的行为类似于三值逻辑。如果历史在状态中不可执行（ $s \not\triangleright\triangleleft \alpha$ ），则公式在该配对中既不为真也不为假，尽管该逻辑保留了标准的有效性。

2.3 “空”公式

一项核心的技术创新是定义了一个公式 empty：
$\text{empty} := \bigwedge_{a \in A} [a]\bot \land \bigwedge_{a,b \in A} K_a [b]\bot$
该公式刻画了历史为空（ $\alpha = \epsilon$ ）的状态。它断言没有人接收过任何消息，且所有人都知道这一点。这仅在多智能体设置中（ $|A| \ge 2$ ）才可能实现。

3. 主要贡献

3.1 公理化 $AA^*$

主要贡献是提出了 $AA^*$ ，这是针对 $\ast$ -有效性（恒真性）的公理化系统。

无穷性本质： 与之前基于归约的系统 $AA $不同，$ AA^*$ 是无穷的。它无法将动态模态归约为静态模态，因为公式的真值取决于具体的历史。
规则 $(R^*)$ ： 该系统包含一条无穷规则：
- 前提： 对于所有词 $\alpha$ ， $\text{empty} \to [\alpha]\varphi$ 是可推导的。
- 结论： $\varphi$ 是可推导的。
  该规则通过 empty 公式将历史“重置”为空，从而有效地将 $\ast$ -有效性归约为 $\epsilon$ -有效性。
公理： 该系统包含以下公理：
- 知识与动态模态的分配律。
- 可执行性条件（例如，只有发送了消息才能接收）。
- 原子永存性（原子的真值不改变）。
- 针对异步环境中知识的特定公理： $\text{empty} \to (K_a \varphi \leftrightarrow ([\alpha]\bot \lor \bigvee_{\alpha \triangleright_a \beta} K_a [\beta]\varphi))$ 。

3.2 完备性与可靠性

可靠性： 作者证明了 $AA^*$ 中的每个定理都是 $\ast$ -有效的。
完备性： 他们证明了每个 $\ast$ -有效的公式都是 $AA^*$ 的定理。证明使用了基于极大一致理论的典范模型构造。一个重大的技术障碍是定义典范模型上的可达关系，以确保它们仅在限制为包含 empty 的理论时才构成等价关系。

3.3 单智能体局限性

本文严谨地证明了所提出的方法在单智能体情况下失效。

在单智能体系统中，智能体总是知道他们接收了所有已看到的消息。不存在一个等价于 empty 的公式，能够区分空历史与智能体已接收所有消息的非空历史。
因此，在单智能体情况下，通过 empty 将 $\ast$ -有效性归约为 $\epsilon$ -有效性是不可能的。作者将单智能体情况的公理化作为一个未解决的问题留待未来研究。

4. 结果

形式系统： 针对带有独立发送/接收模态的异步认知逻辑，提出了一个完备且可靠的无穷公理化系统（ $AA^*$ ）。
归约机制： 一种新颖的方法，利用 empty 公式将逻辑锚定回初始状态，从而处理“恒真性”，无需有限归约系统。
与 S5 的区别： 该逻辑在全局上不满足标准的 S5 真值公理（ $K_a \varphi \to \varphi$ ）。只有当智能体知道历史为空时，知识才是事实性的。否则，该模态的行为更像“一致信念”。
与分布式计算的比较： 该语义与分布式系统中的**一致割（consistent cuts）**概念相一致，但通过直接将可执行性（真值条件）纳入逻辑，对其进行了细化，从而防止了不一致的状态（例如，在消息发送之前接收消息，或接收虚假的宣告）。

5. 意义

理论进展： 这项工作弥合了标准动态认知逻辑（假设同步）与分布式计算现实（异步）之间的差距。它提供了第一个严格的逻辑框架，将发送和接收视为具有独立模态的不同异步事件。
处理时间不确定性： 它成功建模了一种特定类型的不确定性，即智能体不确定相对于他人而言通信历史的长度，这种场景在流言协议和分布式共识中很常见。
方法论创新： 结合使用无穷规则（ $R^*$ ）和特定的“重置”公式（empty），为公理化那些无法通过有限重写归约为静态性质的动态逻辑提供了新模板。
未来方向： 论文指出了清晰的未来研究路径，包括将逻辑扩展到群体知识（分布式知识）、非公开通信，以及解决单智能体公理化问题。

总之，本文建立了一个稳健的逻辑基础，用于推理异步环境中的知识，证明了虽然标准的归约技术会失效，但精心构建的无穷系统可以捕捉异步消息传递的全部复杂性。