技术摘要：通过符号模型性质判定一阶逻辑片段的可判定性结果

问题陈述

一阶逻辑（FOL）是一种强大的形式化方法，用于为具有无界域的系统（例如涉及链表或树形数据结构的系统）指定验证条件。然而，FOL 通常是不可判定的。虽然有限模型性质（即每个可满足公式都有一个有限模型）意味着可判定性，但许多有用的 FOL 片段并不具备这一性质；它们可能仅允许无限模型。因此，依赖 FOL 的验证工具可能无法为无效公式找到反模型，导致用户无法获得可操作的反馈。

现有的可判定片段，如分层公式（SF）片段（EPR 的多排序变体），通过对量词交替图施加严格的无环约束来保证有限模型性质。这些约束对于建模复杂系统往往过于严格，需要用户付出大量精力来调整规范。本文致力于解决为那些不享有有限模型性质的 FOL 片段建立可判定性的挑战，具体针对那些在特定排序上允许量词交替图中存在自环的片段，前提是满足某些序论限制。

方法论

作者提出了一种符号结构的推广，该结构最初在 [15] 中使用线性整数算术（LIA）引入，现推广至任意具有标准模型的基理论。

1. 广义符号结构

符号结构是对潜在无限一阶结构的有限表示。它由以下部分组成：

• 节点： 一组有限节点，表示基理论 $T$ 的标准模型中域的子集。
• 约束公式： 每个节点关联一个 $T$ 语言中的公式，用于定义其所代表的元素集合。
• 符号解释： 常量、函数和关系的解释是使用 $T$ 中的项和公式以符号方式定义的。

符号结构的关键性质在于，模型检查（确定一个结构是否满足某个公式）可归约为基理论 $T$ 中公式的有效性。如果 $T$ 是可判定的，那么符号结构的模型检查也是可判定的。

2. 符号模型性质

本文针对特定的 FOL 片段建立了符号模型性质。如果一个片段中的每个可满足公式都在某个可判定基理论上拥有一个满足性的符号结构，则该片段具备此性质。由于此类结构的模型检查是可判定的，该性质的存在意味着该片段的可满足性问题是可判定的。

3. 有序自环（OSC）族

作者定义了一个名为**有序自环（OSC）**的片段族，该族由特定排序 $s_\infty$ 上的严格序关系 $\prec$ 的公理化 $\alpha$ 参数化。

• 对 SF 的放宽： OSC 通过放宽无环要求扩展了分层公式片段。它允许函数符号在排序 $s_\infty$ 上引入自环（循环），前提是量词交替图中不包含其他循环。
• 基理论： 本文使用了两种主要的基理论：
  • 线性整数算术（LIA）： 用于全序。
  • 可判定的字符串理论（STR）： 用于前缀序。

4. 证明构造

可判定性证明遵循一个通用的“证明食谱”，即从公式 $\phi$ 的任意模型 $M$ 构造一个符号模型 $S$。该构造涉及以下步骤：

1. 划分： 根据原子公式满足情况将 $M$ 的域划分为等价类。这些类成为符号结构的节点。
2. 解释： 定义常量、一元关系和序 $\prec$ 的解释，以“观察” $M$ 中满足的原子公式。
3. 处理混合序原子： 核心难点在于满足混合序原子（例如 $f(x) \prec g(x)$）和序公理 $\alpha$。这是通过在基理论中定义节点（摘要节点）和函数项的特定内部形状来实现的。
   • 对于全序（tot），摘要节点被建模为双向无限直线（整数），从而允许项排序的“通用有限可嵌入性”。
   • 对于前缀序（pref），摘要节点被建模为“通用树”（具有特定分支因子的双向无限树），以适应前缀序的非线性性质。

主要贡献

1. 符号结构的广义定义： 本文提供了针对任何具有标准模型的基理论的符号结构的参数化定义，推广了此前仅限于 LIA 的工作。
2. 引入 OSC 族： 定义了有序自环片段族，该族通过允许在特定公理下对有序排序进行自环，扩展了分层公式。
3. 新的可判定性结果： 作者证明了 OSC 族内若干新片段的可判定性，具体包括：
   • OSC[pref]： 前缀有序自环，使用字符串理论。该片段用于建模无环树形数据结构和共享链表中的可达性。
   • 带后继/前驱的变体： 结合全序/前缀序与保证后继存在（prosucc）或前驱存在（regpred）公理的片段。
4. 通用证明框架： 提出了一种统一的证明技术，为这些片段构造符号模型，证明了可满足性可归约为相应可判定基理论（LIA 或 STR）中公式的有效性。
5. 实现： 实现了一个概念验证工具，扩展了开源 FEST 库，以支持通用符号结构，包括基于字符串理论的模型检查。

结果

本文确立了以下片段的可满足性问题是可判定的（其中 $\alpha$ 为序公理）：

• $\alpha \in \{ \text{tot}, \text{tot} \land \text{prosucc}, \text{tot} \land \text{regpred}, \text{pref}, \text{pref} \land \text{prosucc}, \text{pref} \land \text{regpred} \}$。

tot 的结果重述了先前的工作 [15]，而 pref 及其变体的结果是新的。OSC[pref] 的可判定性尤为显著，因为它处理了那些不具备有限模型性质但可以使用字符串理论以符号方式表示的结构。

意义与主张

本文主张，这项工作提供了一种超越有限模型性质的可判定性新途径。通过利用符号结构，它使得能够验证那些由于缺乏有限反模型而此前难以处理的具有无界域的系统。

• 理论影响： 它弥合了有限模型性质与无限模型表示之间的差距，表明即使当无限模型是必要的，只要它们能被可判定的基理论所捕捉，仍可实现可判定性。
• 实践相关性： OSC[pref] 片段直接解决了涉及树形数据结构和共享链表的常见验证场景，这些场景在严格分层的片段中难以建模。
• 通用性： 该框架设计为可扩展至其他基理论和序关系，暗示了发现更多可判定片段的路径。

作者指出，虽然判定过程将可满足性归约为基理论中公式的有效性（对于字符串理论而言，这可能是非初等的），但主要贡献在于确立可判定性以及在验证失败时生成符号反模型的能力。该实现作为这一方法可行性的概念验证。