混合动态逻辑的Ehrenfeucht-Fra?ssé博弈：一种模块化表征初等等价性的新方法

《ACM Transactions on Computational Logic》：Hybrid-Dynamic Ehrenfeucht-Fra?ssé Games

本文为混合动态命题逻辑（HDPL）及其片段提出了一种新颖的、直接的、完全模块化的Ehrenfeucht-Fra?ssé（EF）博弈框架。该框架通过参数化语言特征（如模态算子、混合算子及一阶量词）来刻画初等等价性，并建立了新的模块化Fra?ssé-Hintikka定理。文章深入研究了可数博弈等价（由可数EF博弈决定）与互模拟（bisimulation）及来回系统（back-and-forth systems）之间的关系，证明在特定语言条件下三者等价，并由此推导出Hennessy-Milner定理的类似物，以及可达、像有限（image-finite）Kripke结构上初等等价蕴含同构的重要结论。

　　

混合动态Ehrenfeucht-Fra?ssé博弈

Ehrenfeucht-Fra?ssé（EF）博弈为表征一阶逻辑的初等等价性提供了方法，并通过标准翻译也适用于模态逻辑。本文提出了一种将EF博弈新颖地推广到混合动态逻辑（Hybrid-Dynamic Logics）的方法，该方法直接且完全模块化：通过参数化我们希望包含的混合语言特征，例如模态和混合语言算子以及一阶存在量词。我们利用这些博弈为混合动态命题逻辑（HDPL）及其各种片段建立了一个新的模块化Fra?ssé-Hintikka定理。我们研究了可数博弈等价（由可数EF博弈决定）和互模拟（由可数来回系统决定）之间的关系。通常，前者比后者弱，但在语言的某些条件下，两者是一致的。作为推论，我们得到了Hennessy-Milner定理的类似物。我们还证明了对于可达的像有限Kripke结构，初等等价蕴含同构。

引言

混合逻辑，特别是混合动态逻辑，是表达能力强的模态逻辑，非常适合于描述行为动态：如果某个事物在某个状态下成立，那么另一个事物在从该状态可达的某个状态下成立。混合动态逻辑已应用于反应式和基于事件/数据的系统的规范和建模（例如，[14, 17, 19]）。动态命题逻辑（DPL）的表达能力超越了其混合对应物，但代价是失去了重要的逻辑性质，如紧致性[18]。可能不太为人所知的是，混合动态命题逻辑（HDPL）具有足够的表达能力来描述有限模型（参见例2.5）。

Ehrenfeucht-Fra?ssé（EF）博弈刻画了一阶逻辑中的初等等价性[15]。在本文中，我们为HDPL及其片段提出了一个模块化的EF博弈概念，旨在适应模态逻辑中遇到的各种量化形式。模块化在混合逻辑上下文中的优势在[5]中得到了充分展示。我们应用这个框架来建立混合动态逻辑的Fra?ssé-Hintikka定理[15]，并研究可数博弈等价（由可数EF游戏决定）、ω-互模拟（ω-bisimulations）和来回系统（back-and-forth systems）[3]之间的关系。在EF博弈中，参与者的移动对应于各种类型的（混合）量化，包括对结构化行动的可能性、一阶量化和存储（store），后者为当前状态命名。支持这种形式化的数学结构是博弈板树（gameboard tree）[13]，我们对其进行了边标签的扩展。这类树的作用类似于国际象棋中的棋盘。博弈板树也可以看作表示句子的量词秩，因为节点对应于签名，边表示用变量扩展签名的标签。

在本文中，我们研究了EF博弈的两种版本：有限版本和可数无限版本。在博弈板树上进行的有限EF博弈中的获胜策略，正是由所谓的博弈句子（game sentences）精确描述的，这些句子定义在这样的树上。在文献中，陈述有限EF博弈中的获胜策略恰好由博弈句子描述的结果被称为Fra?ssé-Hintikka定理（定理3.6）；它适用于HDPL的所有片段，包括动态命题逻辑。据我们所知，现有文献中没有出现关于混合或动态逻辑的Fra?ssé-Hintikka定理的证明。该定理的一个直接结果是基于EF博弈的混合动态初等等价性刻画（推论3.7），断言有限EF博弈产生的等价性与初等等价性一致：点模型无法被句子区分。我们进一步表明，由可数无限EF博弈诱导的等价性与ω-互模拟一致，并且在某些条件下，与来回等价性一致。作为应用，我们证明了Hennessy-Milner定理的类似物，并表明对于有根的像有限模型，初等等价性与同构一致。

文献中已经提出了几种混合逻辑的EF博弈变体，但尚未用于混合动态逻辑。例如，[1]中引入了混合时序逻辑的EF博弈，而[16]提出了混合计算树逻辑的EF博弈。值得注意的是，这些工作中混合初等等价性的刻画是直接通过对混合句子复杂度的归纳建立的，而不是作为Fra?ssé-Hintikka定理的推论。

这项工作包含了几个塑造其EF博弈方法的特征：（a）首先，它基于范畴论，这为构建EF博弈（包括博弈板树的概念）提供了一个基础框架。在这种设置下，Spoiler/?belard的移动被适当地限制，从而能够定义博弈句子——精确描述游戏中允许移动的公式。这些博弈句子然后被用来证明初等等价性与Duplicator/?loise的获胜策略的存在性是一致的。（b）其次，博弈板树的使用使得EF博弈能够采用模块化方法。通过选择性地添加或移除条件——对应于所考虑的句子运算符——可以使框架适应特定的逻辑片段。这种灵活性在不需要混合动态逻辑全部表达能力，并且注意力可能仅限于片段（如混合命题逻辑（HPL））的应用中尤其有价值。

其他框架也支持模块化推理。例如，互模拟——通常被视为EF博弈的模态对应物[20]——表现出模块化结构。我们表明ω-互模拟对应于?loise在可数无限EF博弈中的获胜策略。相比之下，来回系统——通常被视为?loise策略的形式化[3]——往往更强。它们与EF博弈的等价性仅当逻辑片段在特定句子运算符下封闭时才成立。这表明来回方法可能隐含地假设了语言中这些运算符的可用性，这可能会影响其在不同逻辑片段间的适应性。每种方法都有其优点和局限性，但最终必须基于预期用途和未来发展做出选择。在这种背景下，我们基于博弈板树并以博弈句子为特征的EF博弈方法，为特定逻辑片段的机械化和工具开发提供了一条途径，尤其是在有限表达力既足够又可取的领域。

文章结构

我们首先在第2节中将HDPL的逻辑框架介绍为一个由句子构造器参数化的语言族。在第3节中，我们描述了HDPL及其片段的有限EF博弈，并证明了一个通用的、模块化的Fra?ssé-Hintikka定理来刻画初等等价性。我们在第4节转向无限EF博弈，并将这些博弈与ω-互模拟和来回系统联系起来；特别是，对于像有限模型，我们得到了HPL无量词片段的Hennessy-Milner定理，并证明了有根的、初等等价的模型是同构的。我们在第5节得出结论。

HDPL

签名

签名的形式为（Nom, Bin, Prop），其中（Nom, Bin）是一个单类一阶签名，由一组称为名词（nominals）的常量Nom和一组二元关系符号Bin组成，Prop是一组命题符号。我们让Σ范围描述为上述形式的签名。类似地，对于任何索引i，我们让Σ_i范围描述为形式为（Nom_i, Bin_i, Prop）的签名，其中（Nom_i, Bin_i）是类似上述定义的形式为（Nom_i, Bin_i）的单类一阶签名。签名态射σ: Σ → Σ' 由一个一阶签名态射σ_FO: (Nom, Bin) → (Nom', Bin') 和一个函数σ_Prop: Prop → Prop' 组成。通过添加一个新名词i对Σ的扩展记为Σ(i)，产生包含ι: Σ → Σ(i)。我们用|Sig_HDPL|表示HDPL签名范畴。

模型

在签名Σ上定义的模型是标准的Kripke结构M = (W^M, (R^M)_R∈Bin, V^M)，使得：

(1) (W^M, (R^M)_R∈Bin) 是Σ上的一阶结构。我们用|M|表示M的论域，并称|M|的元素为状态、可能世界或节点。可达关系包括将Bin中的二元关系符号解释到M中，即对于每个二元关系符号R∈Bin，R^M是一个可达关系。

(2) V^M是从状态集|M|到命题逻辑模型类（即命题符号的子集）的映射。

我们让M和N范围描述为形式为(W^M, (R^M)_R∈Bin, V^M)和(W^N, (R^N)_R∈Bin, V^N)的Kripke结构。类似地，对于任何索引i，我们让M_i和N_i范围描述为形式为(W^M_i, (R^M_i)_R∈Bini, V^M_i)和(W^N_i, (R^N_i)_R∈Bini, V^N_i)的Kripke结构。两个Kripke结构M和N之间的同态h: M → N 是一个一阶同态h: (|M|, (R^M)_R∈Bin) → (|N|, (R^N)_R∈Bin)，使得对于所有状态w∈|M|，有V^M(w) = V^N(h(w))。

事实2.1. 对于任何签名Σ，Σ-同态在明显的多类函数复合下构成一个范畴Mod(Σ)。

对于任何签名态射σ: Σ → Σ'，还原函子Mod(σ): Mod(Σ') → Mod(Σ)定义如下：Σ'-模型M的还原Mod(σ)(M)是M_|σ = (W^M_|σFO, (R^M_|σFO)_R∈Bin, V^M_|σProp)，其中(W^M_|σFO, (R^M_|σFO)_R∈Bin)是一阶逻辑中M跨σ_FO的还原，并且对于所有状态w∈|M|，V^M_|σProp(w)是命题逻辑中V^M(w)跨σ_Prop的还原。Σ'-同态h: M → N的还原Mod(σ)(h)是一阶同态h: (|M|, (R^M)_R∈Bin') → (|N|, (R^N)_R∈Bin')。由于对于所有状态w∈|M|，有V^M(w) = V^N(h(w))，我们得到V^M_|σProp(w) = V^N_|σProp(h(w))对于所有状态w∈|M|，这意味着Mod(σ)(h)是良定义的。如果σ是包含，我们也写M_|Σ表示Mod(σ)(M)。

事实2.2. Mod: Sig_HDPL → Cat是一个函子，对于每个签名态射σ和每个Σ'-同态h，有Mod(σ)(h) = h，其中Cat是所有范畴的范畴。

行动

签名Σ上的行动集Act(Σ)由以下文法定义：

α ::= R | α ∪ α | α; α | α*

其中R是名词上的二元关系。行动在Kripke结构M中被解释为可能世界之间的可达关系。这是通过扩展名词上二元关系符号的解释来完成的：

(1) 对于Bin中的所有二元关系R，有[R] = R^M。

(2) [α ∪ β] = [α] ∪ [β]（并集）。

(3) [α; β] = [α] diagrammatically composed with [β]（关系的图解复合）。

(4) [α] = ([α])（关系的自反传递闭包）。

句子

令X为一组变量名。签名Σ的变量是一个对(x, Σ)，其中x是一个变量名。注意，所有变量(x, Σ)都不同于Σ中的所有符号。变量(x, Σ)沿签名态射σ: Σ → Σ'的翻译是(x, Σ')。签名Σ上的句子集Sen(Σ)由以下文法定义：

φ ::= p | i | ?φ | ∧Φ | ∨Φ | @_iφ | ?α?φ | ↓x.φ | ?x.φ

其中p是命题符号，i是名词，Φ是Σ上句子的有限集，x是Σ的变量，α是Σ上的行动，并且φ是Σ上的句子。句子?α?φ读作“在行动α之后φ成立”（可能性），@_iφ读作“在状态i处φ成立”（检索），↓x.φ读作“φ成立且当前状态绑定到x”（存储）。我们将使用通常的缩写：φ → ψ 表示 ?φ ∨ ψ，φ ? ψ 表示 (φ → ψ) ∧ (ψ → φ)，∧Φ 表示 ?∨{?φ | φ ∈ Φ}。每个签名态射σ: Σ → Σ' 诱导一个句子翻译Sen(σ): Sen(Σ) → Sen(Σ')，以归纳方式将Σ-句子φ中的每个符号根据σ替换为Σ'中的符号。

值得注意的是，量化句子?x.φ（其中x是Σ的变量）沿σ: Σ → Σ'的翻译是?x'.Sen(σ(x))(φ)，其中x'是x的翻译，而σ(x): Σ(x) → Σ'(x')是σ的扩展，将x映射到其翻译x'。

事实2.3. Sen: Sig_HDPL → Set是一个函子，其中Set是所有集合的范畴。

这种方法有助于防止给定签名内变量和常量之间的冲突。此外，可以干净地定义替换，避免需要侧条件。当没有混淆的危险时（例如，变量名是签名的元素之一），我们仅通过其名称来标识变量。这意味着签名包含ι: Σ → Σ'决定了句子集的包含Sen(ι): Sen(Σ) → Sen(Σ')。

局部满足关系

句子φ在签名Σ上的模型M和世界w上的局部满足关系通过句子的结构归纳定义：

— M, w ? p 当且仅当在命题逻辑中p ∈ V^M(w)，即p ∈ V^M(w)。

— M, w ? i 当且仅当 w = i^M。

— M, w ? ?φ 当且仅当 非 M, w ? φ。

— M, w ? ∧Φ 当且仅当 对于所有φ ∈ Φ，有 M, w ? φ。

— M, w ? @_iφ 当且仅当 M, i^M ? φ。

— M, w ? ?α?φ 当且仅当 存在某个v使得(w, v) ∈ [α] 且 M, v ? φ。

— M, w ? ↓x.φ 当且仅当 M', w ? φ，

其中M'是M到Σ(x)的唯一扩展，将x解释为w。

— M, w ? ?x.φ 当且仅当 存在