💻 computer science

Symbolic Model Checking using Intervals of Vectors

本文介绍了一种针对 Petri 网的新型符号模型检测方法，该方法利用向量上的广义区间来克服状态空间爆炸问题，并通过高效的饱和与聚类技术，在全局 CTL 验证任务中展示了极具前景的性能。

原作者： Damien Morard, Lucas Donati, Didier Buchs

发布于 2026-02-04

📖 1 分钟阅读☕ 轻松阅读

原作者： Damien Morard, Lucas Donati, Didier Buchs

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

以下是使用简单语言和创意类比对该论文进行的解释。

核心问题： “无限图书馆”

想象一下，你正在检查一个图书馆是否遵守某项特定规则，比如“任何人同时不能持有超过 5 本书”。在一个小型图书馆里，你可以直接走遍每一条走廊，数清每个书架上的书。这被称为模型检测（Model Checking）。

然而，在计算机科学中，系统（如软件或红绿灯）就像拥有无限走廊的巨大图书馆。可能的“状态”（即每个书架上有多少本书）增长速度极快，以至于逐一计数变得不再可能。这就是著名的**“状态空间爆炸”（State Space Explosion）**问题。如果你试图列出每一个可能的情况，你的计算机会在完成任务之前就耗尽内存。

旧方法：“范围列表”

为了解决这个问题，研究人员通常使用决策图（Decision Diagrams）。你可以把它想象成不是通过列出每一本书，而是创建一个巨大的、多层级的地图来组织图书馆。

论文的批判： 作者指出，现有的方法类似于拥有一个“区间”列表（例如，“书 1 到 10”，“书 20 到 30”）。但当你同时处理多个书架（维度）时，这些列表会变得非常混乱。这就像试图仅用一维线条来描述一个三维房间；它无法很好地契合。

新思路：“向量区间”

作者提出了一种新的组织图书馆的方法，称为符号向量集（Symbolic Vector Sets）。

类比：“包含与排除”之盒
想象你想在不逐一命名的情况下，描述房间里的一个人群。

旧方法： 你可能会说，“身高在 5 英尺到 6 英尺之间的人。”
新方法（向量区间）： 你会说，“比 A 个人高，且比 B 个人矮的人。”

在本文中，“向量”只是一个代表状态的数字列表（例如，网络中不同位置有多少个令牌/token）。

下界（“必须拥有”）： 一个必须包含的向量集合。（例如，“你必须在这里至少有 2 个令牌，在那里有 1 个令牌”）。
上界（“必须没有”）： 一个必须排除的向量集合。（例如，“你不能在这里有 10 个令牌”）。

这创建了一个有效状态的“盒子”。计算机不再列出盒子内的每一个有效状态，而只是记住边界。

魔法技巧：无需打开盒子即可进行数学运算

这篇论文真正的天才之处不仅在于描述这个盒子，还在于无需打开它去计数，就能对这个盒子进行数学运算。

类比： 想象你有一个装满苹果的盒子。通常，为了增加 5 个苹果，你必须打开盒子，数一下，加上 5 个，然后关上。
论文的方法： 作者创建了特殊的规则（称为同态运算/Homomorphic Operations），让你能够说，“给整个盒子增加 5”，计算机就会瞬间更新“下界”和“上界”标签。它从未真正去数苹果。它只是移动了边界。这使得计算过程极其快速，即使盒子里装有一亿个苹果也是如此。

处理“混乱”部分：规范形式

有时，两种不同的描述实际上可能意味着同一件事。

例子： “比 5 英尺高，比 10 英尺矮” 等同于 “比 5 英尺高，比 10 英尺矮。”
但在复杂的数学运算中，你可能会得到 “比 5 英尺高，比 10 英尺矮” 以及 “比 5 英尺高，比 9 英尺矮，但比 8 英尺高”。这些描述是混乱且冗余的。

作者创建了一种规范形式（Canonical Form）。可以将其视为一种“标准化的身份证”。

无论你如何描述这一群体，计算机都会强制将其转化为一种特定的、唯一的格式。
这防止了计算机浪费时间进行重复计算，或以两种不同的方式存储同一个群体。

“饱和”技巧：跳过步骤

当计算机尝试寻找所有可能的状态时，它有时会陷入循环，反复检查同样的东西（就像在迷宫中转圈圈）。

解决方案： 他们使用了一种名为**饱和（Saturation）**的技术。
类比： 想象你正在用一桶水填满一个容器。你不需要检查每一滴水来判断桶是否满了，你只需要不断倾倒，直到水位不再上升为止。一旦水平稳定下来，你就知道完成了。
在论文中，这允许计算机实现跨越。如果增加“容量”（一个位置可以容纳多少令牌）不会改变结果，计算机就会跳过中间步骤，直接跳向答案。

结果：击败竞争对手

作者通过一项涉及复杂“佩特里网”（Petri Nets，一种用于模拟交通灯或生物过程等系统的图表）的著名竞赛（MCC 2022）测试了他们的工具（称为 SVSKit）。

挑战： 其中一个特定的测试（“昼夜节律钟/Circadian Clock”）的容量达到了 100,000。这是一个巨大的数字。
竞赛情况： 其他顶尖工具耗时超过一小时，并且未能解决所有问题。
结果： 作者的工具在约 30 分钟内解决了所有问题。
原因： 因为他们不是在计数每一个可能的情况（这会耗费永恒的时间），而是直接操作这些“盒子”（区间）。

总结

这篇论文介绍了一种检查复杂系统是否安全的新方法。他们不再列出每一个可能的场景（对于大型系统来说这是不可能的），而是使用由最小值和最大值定义的智能盒子——“向量区间”。他们发明了数学规则来操作这些盒子，而不必打开它们，并建立了一套“标准化”系统来保持整洁。这使得他们能够解决其他工具认为过于庞大的问题。

技术摘要：基于向量区间的符号模型检测

1. 问题陈述

模型检测是一种稳健的形式化验证技术，用于确保软件和硬件系统符合规范。然而，它受到状态空间爆炸问题的严重阻碍，即状态和转移的数量随系统规模呈指数级增长。在全局模型检测（global model checking）中，这一挑战尤为突出，其目标是识别满足计算树逻辑（CTL）公式的所有状态，而非仅仅验证单个配置。

现有的技术，如决策图（DDs）、抽象和偏序归约，虽然缓解了这一问题，但随着模型变得更加复杂，它们也面临着局限性。具体而言，标准的基于区间的处理方法（例如区间决策图）将向量集合编码为向量的区间（vectors of intervals）。本文认为，对于 Petri 网，一种更有效的方法是将向量集合编码为向量的广义区间（intervals of vectors），而非向量的区间。这种区别至关重要，因为向量空间通常涉及非全序的偏序关系，使得简单的区间定义不再适用。

2. 方法论

作者提出了一种名为符号向量集（Symbolic Vector Sets, SVS）的新型符号结构，用于对 Petri 网的标记（markings）进行编码。该方法建立在三个核心支柱之上：

2.1. 符号向量与集合

一个符号向量被定义为一个对 $(a, b)$ ，其中 $a$ 和 $b$ 是向量（标记）的集合。

包含 ( $a$ )： 标记 $q$ 属于该符号向量，如果它包含了 $a$ 中的所有向量（在非严格偏序 $\subseteq_f$ 下）。
排除 ( $b$ )： 标记 $q$ 属于该符号向量，如果它不包含 $b$ 中的任何向量。
泛化： 这将自然数区间 $[a, b]$ （其中 $a \le x \le b$ ）推广到了向量。由于向量之间并不总是可比的，该结构需要一组下界（ $a$ ）和一组上界（ $b$ ），而不是单一的边界。

一个符号向量集是这些符号向量的集合，代表了它们底层标记集的并集。

2.2. 规范形式与操作

为了确保效率并避免冗余，作者为符号向量和集合定义了一个规范形式（canonical form）。其关键特性包括：

唯一性： 每个标记集都有且仅有一个规范表示。
同态操作： 文中定义了同构操作（并、交、差、补），这些操作直接作用于符号结构，而无需将其解码为单个标记。
可合并性与可共享性： 为了维持规范性，作者引入了关系来确定何时两个符号向量可以合并，或者是否存在“可共享”的组件。这涉及到一个词典序全序，用以解决非全序中的歧义，从而确保对重叠约束的处理具有确定性。

2.3. Petri 网上的 CTL 模型检测

该框架将这些结构应用于具有有限容量的 Petri 网。

前驱操作（Pre-Operation）： 全局模型检测的核心是 pre 操作，用于计算前驱标记。作者定义了一个作用于符号向量集的符号 pre 操作，处理了转移的可逆性和容量约束。
不动点评估： CTL 公式（如 $EF$, $EG$, $EU$）通过在符号向量集上进行不动点计算（最小和最大不动点）来进行评估。公式的满足性通过检查标记是否属于最终生成的符号向量集来确定。

2.4. 优化

饱和（Saturation）： 为了应对不动点计算中中间解变得过大的“峰值效应”，作者实现了一种饱和策略。这包括迭代容量边界并利用先前结果来计算后续步骤，从而显著减少了中间符号向量的数量。
聚类（Clustering）： 文中提到了聚类作为一种潜在的可达性优化手段，即将较小的向量组合在一起，尽管这被标注为一个有待未来进行形式化描述的概念。

3. 核心贡献

新型编码： 引入了符号向量集，这是一种将区间推广到向量的结构，专门设计用于处理 Petri 网标记的非全序特性。
形式化规范化： 对符号向量和集合进行了严谨的规范形式定义，包括唯一性证明以及能够保持规范性的同态操作（并、交、差、补）的开发。
全局模型检测框架： 提供了一套完整的形式化方法，用于使用这些符号结构在 Petri 网上评估 CTL 公式，包括符号 pre 操作的定义。
饱和算法： 将饱和原理（源自其他符号技术）应用于符号向量集的背景下，以减轻不动点迭代过程中的计算峰值。
实现（SVSKit）： 一个实现了该理论的 Swift 库，并在来自模型检测大赛（MCC）2022 的基准测试中进行了测试。

4. 结果

作者使用 SVSKit 工具在 MCC 2022 的示例（特别是 Circadian Clock 模型）上评估了其方法。

饱和对可扩展性的影响： 在 Circadian Clock 模型（14 个 place，16 个 transition）上的实验表明，饱和至关重要。如果没有饱和，计算时间会随 place 容量呈指数级增长（容量为 6 时超过 5 小时）。使用饱和后，对于容量 2 及以上的情况，计算时间保持恒定（约 3.2 秒），且符号向量的数量保持稳定。
处理大规模状态空间： 该工具成功处理了容量高达 $N=100,000$ 的情况，编码了约 $10^{84}$ 个标记，而最终仅生成了 26 个符号向量。
基准测试性能： 在 MCC 2022 的 CTL 可达性（fireability）类别中，现有工具（GreatSPN, ITS-Tools, Tapaal）未能能在 60 分钟限制内回答所有 16 个查询（Tapaal 回答了 9/16）。SVSKit 方法在约 30 分钟内解决了全部 16 个查询。
局限性： 作者承认当前的实现面临可扩展性挑战，主要是由于规范化操作的最坏情况复杂度为 $O(n!)$ 。效率高度依赖于这些操作的实现，并且由于这些约束，该工具在基准测试中被限制在相对较小的 Petri 网上。

5. 意义与主张

本文声称通过从“向量的区间”转向“向量的区间”，为现有的符号模型检测技术提供了一种极具前景的替代方案。

理论贡献： 它提供了一个在偏序下操作向量集的正式代数框架，填补了文献中此类结构长期停滞的空白（参考了 30 年前的原始“谓词结构”）。
实际可行性： 结果表明，该方法处理无限或极大状态空间的能力可能比显式枚举更高效，并且在特定的全局模型检测任务（特别是涉及大容量的任务）中可能优于现有工具。
未来方向： 作者谦虚地指出，当前实现仍需改进，特别是优化规范化操作。他们提出了未来的工作方向，包括局部模型检测（将方法扩展到 Petri 网之外的模型）以及集成（将此方法与决策图结合，认为两者是正交的，可以实现混合化）。

论文总结道，尽管目前的实现存在局限性，但符号向量集的理论基础和初步实验结果验证了其在全局模型检测中的潜力。