💻 computer science

A Forward-Only Construction of Semilinear Inductive Invariants for VAS

本文介绍了一种针对向量加法系统（Vector Addition Systems）的新型单向半线性归纳不变性构造方法，该方法仅从源配置中推导不变性，从而产生了与系统结构相一致的更具规范性的结果，并为将这些技术扩展到诸如分支向量加法系统（Branching VAS）等非对称模型提供了途径。

原作者： Clotilde Bizière, Jérôme Leroux, Grégoire Sutre

发布于 2026-06-26

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Clotilde Bizière, Jérôme Leroux, Grégoire Sutre

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

大局观：“我能不能到达那里？”的问题

想象你有一个机器人在一个巨大的仓库里（这就是向量加法系统，简称 VAS）。机器人从一个特定的位置（源点）出发，拥有一系列可以进行的动作，比如“向前走 2 步”、“向左走 1 步”或“向上走 3 步”。

计算机科学家们提出的核心问题是：机器人在永远不会撞墙（即进入负数区域）的前提下，能否到达一个特定的目标位置（目标点）？

几十年来，我们已知这个问题是可以找到答案的（它是“可判定的”），但寻找答案的方法非常复杂。由 Jérôme Leroux 在 2010 年代提出的一种著名方法，就像是一场“拔河比赛”。

旧方法：拔河比赛（前后兼顾）

Leroux 最初的方法试图通过同时从两个方向来解决问题：

向前： 它想象机器人从源点出发可能到达的所有位置。
向后： 它想象如果我们将机器人的动作反向运行，哪些位置能够到达目标点。

该方法不断扩展这两个列表，直到它们在中间相遇，或者证明它们永远不会接触。如果它们永远不会接触，则意味着目标点是不可达的。

这种方法的缺陷：

它很混乱： 它创建的“证明”（称为归纳不变性）高度依赖于起点和你要检查的具体目标点。如果你稍微改变一下目标点，整个证明就会随之改变。
它缺乏结构性： 因为它依赖于目标点，所以这个证明并不能真正告诉你关于机器人仓库本身的性质。这就像是通过观察一件特定家具的位置来描述房间的形状，而不是通过观察墙壁。
它在复杂系统上会失效： 作者指出，这种“拔河”方法在处理更复杂的系统——**分支向量加法系统（Branching VAS）**时会崩溃（在这种系统中，机器人可以分裂成两个机器人并在稍后合并它们）。在这些系统中，你无法轻易地向后运行，因为“历史”会像树一样纠缠在一起，而不是一条直线。

新方法：单行道（仅限向前）

本文作者提出了一种更简洁、更清晰的新方法来解决这个问题。他们不再从目标点向后看，而是只从源点向前看。

类比：建造围栏
想象你想证明机器人无法进入一个禁区（目标点）。

旧方法： 你尝试从起点建一个围栏，而另一个人尝试从禁区建一个围栏，然后你们在中间汇合，看看围栏是否碰头。
新方法： 你从源点出发，建造一个围栏，将机器人可能到达的所有范围都圈起来。你不断扩张这个围栏，直到它变成一面完美的、坚实的墙。
- 如果你的围栏自然地停在禁区之前，你就得到了你的证明。
- 至关重要的一点是，这个围栏的构建仅基于仓库的规则和起始点。它并不关心禁区在哪里。

为什么这很重要：“周期性”的发现

论文针对一种特殊的仓库类型——周期性 VAS（Periodic VAS） 提出了一个特定的发现。

它是什么？ 想象一个机器人的动作具有完美对称性的仓库。如果机器人可以从 A 点移动到 B 点，那么它也可以从 B 点移动到 C 点，且模式会永远重复（就像时钟或日历一样）。
旧方法的缺陷： 当旧的“拔河”方法试图为这些周期性仓库建造围栏时，围栏往往看起来参差不齐且不规则。它可能会包含某个点，却漏掉了正好“一个周期”之外的点，从而破坏了仓库原本完美的重复模式。
新方法的优势： 作者提出的这种“仅限向前”的新方法构建的围栏尊重模式。如果仓库是周期的，那么这个围栏（不变性）也是周期的。它看起来就像一个完美的、重复的网格。

主要结论

逻辑更简单： 你不需要通过从目标点向后看来证明某物是不可达的。你只需要向前看起始点即可。
更好的证明： 该新方法生成的证明是“规范的（canonical）”，这意味着它们是系统本身特有的，而不依赖于你正在测试的具体目标点。它们反映了系统的真实结构。
保留模式： 对于会自我重复的系统（周期性系统），新方法保证了证明也会随之重复，而旧方法经常在这方面失败。
未来的潜力： 由于这种方法不依赖于“向后运行”（这在分支系统中是无法实现的），它为解决分支向量加法系统（即过程会分裂和合并的系统）的可达性问题打开了大门，这目前仍是计算机科学领域的一个重大未解之谜。

简而言之

作者用一种精简的单向构建，取代了复杂的双向猜测游戏。他们创造了一个工具，用来为系统的行为建立“围栏”，确保这些围栏的形状能完美契合系统自身的内部逻辑，从而使证明“某事无法到达”变得更加容易。

技术摘要：针对向量加法系统（VAS）的前向单向半线性归纳不变性构造

问题陈述
向量加法系统（VAS，也称为 Petri 网）的可达性问题是无限状态系统理论中的一个核心决策问题。虽然 Kosaraju 和 Mayr 在 20 世纪 80 年代确立了其可判定性，但其计算复杂度在数十年间一直悬而未决，直到最近才被证明是 Ackermann 完全（Ackermann-complete）的。Leroux 引入的一种重要的替代可判定性方法，通过半线性归纳不变性来表征不可达性。该方法依赖于一种“往复式”（back-and-forth）方案，即同时从源点进行前向过近似扩展，并从目标点进行后向过近似扩展。

然而，现有方法存在两个主要局限性：

对称性依赖： 该构造依赖于 VAS 的对称性，即运行过程可以反转。这种对称性在非对称模型（如分支向量加法系统 BVAS）中会失效，因为 BVAS 的执行过程是树状而非线性序列，这使得将 Leroux 的方法扩展到 BVAS 变得十分困难。
缺乏规范性： 所得的不变量在源点和目标点之间具有同等的依赖性。在许多验证场景中，源点是固定的而目标点是变化的；一个产生的不变量随目标点变化而剧烈变动的方法，其规范性较低，且难以与系统的内在结构建立联系。此外，对于周期性 VAS 等特定子类，Leroux 的方法不能保证所得的不变量具有周期性。

方法论
作者提出了一种新的前向单向构造方法来构建半线性归纳不变性。与往复式方法不同，该方法仅通过构建从初始配置集（ $C_0$ ）出发的集合来构建不变性，而不需要从目标点进行后向推理。

其核心技术组成部分包括：

周期性 VAS： 作者定义了一类可达集是周期性的（对加法封闭且包含零向量）的 VAS。他们证明了通过增加一个计数器，可以将一般 VAS 的可达性问题归约为周期性 VAS 的可达性问题。
几乎半线性集与线性化： 该方法利用了 VAS 可达集作为“几乎半线性”集的几何特征。这些集合被分解为“几乎线性”集（ $b + P$ ），随后通过一个称为“线性化”（$lin(L)$）的过程被过近似为线性集。
内部向量： 本文引入的一个新概念是周期集的“内部向量”。这些向量允许算法通过将向量推入原集合来精细化近似，从而确保构造的不变量既与目标集不相交，又保持周期性。
算法构造： 文中提出了一个算法（算法 1），该算法迭代地精细化一个半线性周期集 $Inv $。在每次迭代中，它识别当前集合的前向可达性与集合本身之间的差异，将此差异分解为几乎线性组件，并将特定的平移线性化结果添加到$ Inv$ 中。由于每次迭代时差异集的“空间维度”都会严格减少，因此证明了该算法的终止性。

主要贡献

前向单向构造： 作者引入了一种构造半线性归纳不变性的方法，该方法主要取决于从源点出发的可达配置。这使得产生的不变量更具规范性，并且更好地与系统的结构保持一致。
周期性 VAS 的周期性不变性： 论文证明了对于周期性 VAS，如果可达集与一个半线性目标集不相交，则存在一个同时与目标集不相交的周期性半线性归纳不变性。这与以往的方法形成对比，后者即使对于周期性系统也可能产生非周期性的不变量。
向周期性 VAS 的归约： 作者提供了周期性 VAS 的有效特征描述，并证明了普通 VAS 的可达性问题可以归约为周期性 VAS 的可达性问题。因此，普通 VAS 的半线性不变性可以从为减少后的周期性系统所构造的周期性不变性中导出。
通过 Oracle 进行存在性证明： 该构造是以带有 Oracle 调用（用于线性化和向量选择）的形式呈现的算法。本文建立了所需向量的存在性并证明了过程的终止性，为周期性半线性不变性的存在提供了构造性证明。

结果

定理 4.5： 周期性 VAS $(A, C_0)$ 的可达集与半线性集 $C_{bad}$ 的交集为空，当且仅当存在一个周期性半线性归纳不变性 $I$ 使得 $I \cap C_{bad}$ 为空。
终止性与正确性： 只要满足 Oracle 调用，所提出的算法就会终止并返回一个与目标集不相交的半线性周期不变性。终止性由 $Post^*_A(Inv) \setminus Inv$ 的空间维度的严格递减所保证。
示例： 论文通过示例说明了该方法在何种情况下能产生独立于特定目标配置的不变量（不同于往复式方法），并在周期性 VAS 的情况下能产生往复式方法无法产生的周期性不变量。

意义与主张
作者声称，这种前向单向方法是向**分支向量加法系统（BVAS）**扩展不变性技术的迈进。由于 BVAS 缺乏进行后向推理所需的对称性（初始配置位于执行树的叶节点，目标位于根节点），因此依赖对称性的往复式方法难以推广。通过纯粹从源点构造不变性，作者表明其方法更适合解决 BVAS 的可达性问题。

论文还讨论了在语法向量加法系统（GVAS）背景下的“半线性归纳不变性”属性，并推测类似的属性可能成立，但这仍是一个有待进一步研究的开放领域。这项工作被定位为对 VAS 可达性结构理解的一次理论进步，提供了一个能够尊重特定系统模型不对称性的、更具规范性的验证工具。