Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

Balbiani、van Ditmarsch、Lerouvillois による論文「Axiomatisation for an asynchronous epistemic logic with sending and receiving messages（メッセージの送信と受信を伴う非同期認識論理の公理化）」の詳細な技術的要約を以下に示す。

1. 問題提起

本論文は、動的認識論理（DEL）を用いてマルチエージェントシステムにおける非同期通信をモデル化する課題に取り組んでいる。

• ギャップ: 標準的な DEL（例えば、公開告知論理）は、通信を瞬時かつ同期したものとみなす。つまり、メッセージが送信され、すべてのエージェントによって同時に受信される。これは、送信と受信が異なる時刻に発生する別々の事象である現実世界の分散システムを捉え損なう。
• 具体的な課題: 著者らは、以下の要件を満たす論理を形式化することを目的としている。
  1. エージェントはメッセージの履歴に関して時間的不確実性を持つ（他者が何件のメッセージを受信したか知らない）。
  2. エージェントは世界の状態に関して認識的不確実性を持つ。
  3. 論理は、メッセージの送信（ブロードキャスト）と受信（個々の行為）を区別しなければならない。
  4. システムは、2 つの文脈における妥当性を扱わなければならない。
     • $\epsilon$-妥当性：初期状態（空の履歴）における真。
     • $\ast$-妥当性（常に妥当）：送信と受信の任意の履歴を前提とした、任意の状態における真。

先行研究（特に文献 [4]）は、$\epsilon$-妥当性に対して、動的モダリティを静的認識モダリティに還元する還元システムを用いた公理化（$AA$）を提供した。しかし、この還元アプローチは、システムの状態が履歴の存在によって根本的に変化する（例えば、エージェントが異なる数のメッセージを受信する可能性がある）$\ast$-妥当性に対しては機能しない。

2. 手法

2.1 言語と構文

著者らは、2 種類の動的モダリティを拡張した多エージェント様式論理 $\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$ で実行可能かどうかを決定する関係。これにより以下のことが保証される。
  1. 履歴は有効な列（FIFO）である。
  2. 告知されたすべての式は、そのブロードキャストの時点で真であった。
  3. エージェントは、自分が可能と考える状態においてのみ実行可能な履歴を考慮する。
• 視覚関係 ($\triangleright_a$): エージェント $a$ が何が可能と考えるかを定義する。エージェント $a$ は、実際の履歴 $\alpha$ に対して、$\beta$ において $a$ が受信したメッセージの列が $\alpha$ において受信したものと完全に一致する場合、履歴 $\beta$ を可能とみなす。重要なのは、エージェントは自分がまだ受信していないメッセージを含む履歴を想定しないことである。
• 3 値的な性質: 意味論は、ある程度 3 値論理のように振る舞う。もし履歴が状態 $s$ で実行不可能 ($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^*$

主な貢献は、$\ast$-妥当性（常に妥当）に対する$AA^*$という公理化の提案である。

• 無限性の性質: 以前の還元ベースのシステム $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. 結果

1. 形式システム: 送信/受信モダリティを分離した非同期認識論理に対する、完全かつ健全な無限公理化 ($AA^*$)。
2. 還元メカニズム: empty 式を用いて論理を初期状態に固定し、有限の還元システムの必要性を回避する「常に妥当」を扱うための新しい手法。
3. S5 からの区別: この論理は、標準的な S5 の真理公理 ($K_a \varphi \to \varphi$) を全体的には満たさない。エージェントが履歴が空であることを知っている場合のみ、知識は事実的である。そうでなければ、モダリティはより「一貫した信念」のように振る舞う。
4. 分散コンピューティングとの比較: 意味論は分散システムにおける整合カットの概念と整合するが、実行可能性（真理条件）を論理に直接組み込むことで、矛盾する状態（例：送信前に受信する、または偽の告知を受信する）を防ぐ点で洗練されている。

5. 意義

• 理論的進展: この研究は、同期を前提とする標準的な動的認識論理と、非同期という分散コンピューティングの現実との間のギャップを埋める。送信と受信を、独立したモダリティを持つ別々の非同期事象として扱う、最初の厳密な論理的枠組みを提供する。
• 時間的不確実性の処理: エージェントが他者との通信履歴の長さについて不確実であるという、特定の種類の不確実性を成功裡にモデル化する。これはゴシッププロトコルや分散コンセンサスで一般的なシナリオである。
• 方法的革新: 有限の書き換えを通じて動的性質を静的なものに還元できない論理の公理化に対して、無限規則 ($R^*$) と特定の「リセット」式 (empty) を組み合わせるという新しいテンプレートを提供する。
• 将来の方向性: 論文は、論理をグループ知識（分散知識）や非公開通信に拡張すること、および単一エージェントの公理化問題を解決することを含む、将来の研究への明確な道筋を特定している。

要約すると、本論文は非同期環境における知識の推論に対する堅牢な論理的基盤を確立し、標準的な還元手法は失敗するが、慎重に構築された無限系が非同期メッセージパッシングの完全な複雑さを捉え得ることを証明している。