💻 computer science

Methods for Efficient Unfolding of Colored Petri Nets

本文提出了两种基于静态分析的互补技术，通过识别等效颜色并排除不可达颜色，显著减小了着色佩特里网展开后的规模，并在 2021 年模型检测竞赛中展现出比现有工具更优的展开网规模和查询成功率。

原作者： Alexander Bilgram, Peter G. Jensen, Thomas Pedersen, Jiri Srba, Peter H. Taankvist

发布于 2026-04-08

📖 1 分钟阅读☕ 轻松阅读

原作者： Alexander Bilgram, Peter G. Jensen, Thomas Pedersen, Jiri Srba, Peter H. Taankvist

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

这篇文章介绍了一种让计算机“读懂”复杂系统模型的新方法。为了让你轻松理解，我们可以把这篇论文的核心内容想象成**“整理一个超级拥挤的仓库”**的故事。

1. 背景：什么是“彩色”Petri 网？

想象一下，你有一个巨大的仓库（这就是Petri 网），里面有很多货架（位置）和传送带（转换）。

普通仓库（P/T 网）： 货架上只有一种颜色的箱子。
彩色仓库（CPN，即本文的主角）： 为了节省空间，人们发明了一种“彩色”仓库。货架上可以放红、蓝、绿等各种颜色的箱子。规则是：只有特定颜色的箱子才能通过特定的传送带。

这种“彩色”设计非常聪明，它让模型看起来很小、很整洁，人类工程师很容易看懂。但是，当计算机想要验证这个仓库是否安全（比如会不会发生拥堵或火灾）时，它无法直接处理“颜色”这种抽象概念。计算机必须把“彩色仓库”**展开（Unfolding）**成一个巨大的“单色仓库”——也就是把每一个颜色的箱子都变成独立的、具体的箱子。

问题出现了： 如果颜色有 100 种，展开后的仓库可能会变成原来的 100 倍甚至 1000 倍大！这就像为了数清楚 100 种不同颜色的乐高积木，你不得不把每一块都拆下来单独放在地上，结果地面瞬间被铺满，计算机根本跑不动（内存爆炸）。

2. 核心方案：两种“整理术”

作者提出了两种聪明的“整理术”，旨在在展开之前，先帮计算机把仓库“瘦身”。

方法一：颜色合并术（Color Quotienting）——“找替身”

场景： 假设仓库里有 100 种不同深浅的蓝色箱子（从深蓝到浅蓝）。
观察： 经过仔细检查，计算机发现：在这个仓库的规则里，深蓝色和浅蓝色箱子 behave（表现）完全一样。它们都能通过同一条传送带，去同一个地方，做同样的事。
操作： 既然它们表现一样，何必区分得这么细？我们可以给这 100 种蓝色箱子发一张“通用通行证”，把它们归为一类，统称为“蓝色组”。
效果： 原本需要展开 100 个蓝色箱子，现在只需要展开 1 个代表“蓝色组”的箱子。这大大减少了仓库的规模，而且不会改变仓库运行的逻辑。

比喻： 就像你在学校点名。如果 30 个学生都穿一样的校服，你不需要叫出每个人的名字（张三、李四...），你只需要喊一声“穿蓝校服的同学”，他们都会回应。这就把 30 次点名变成了 1 次。

方法二：颜色过滤术（Color Approximation）——“去伪存真”

场景： 仓库里有一个货架，理论上可以放红色、蓝色、绿色、黄色...直到紫色的 100 种箱子。
观察： 但是，根据仓库的入口规则（初始状态）和传送带的限制，实际上只有红色和蓝色箱子能到达这个货架。绿色、黄色...那些颜色虽然理论上存在，但永远不可能出现在这个货架上。
操作： 计算机在展开前，先算一算：“嘿，这个货架永远不会有绿色箱子，那我们就别为绿色箱子准备位置了！”
效果： 直接砍掉那些永远不会出现的“幽灵颜色”，只展开真正会用到颜色的部分。

比喻： 就像你要去旅行，行李箱里理论上可以装任何颜色的衣服。但你查了天气预报，目的地只有晴天。于是你决定：“既然永远用不到雨衣，那就不带雨衣了。” 这样你的行李箱（展开后的模型）就轻了很多。

3. 结果：又快又好

作者把这两种方法结合了起来，并在一个名为 TAPAAL 的工具中实现。他们拿 2021 年国际模型检测大赛（Model Checking Contest）中的真实难题来测试。

比大小： 他们的“整理术”生成的仓库，比目前世界上最先进的其他工具生成的仓库要小得多（很多情况下小了一个数量级，也就是小了 10 倍）。
比速度： 虽然他们多做了“整理”工作，但因为这个仓库变小了太多，计算机验证起来反而更快，或者至少没有变慢。
比成绩： 在回答关于仓库安全的各种问题时，他们的方法多解决了 4% 的问题。在计算机领域，这 4% 的提升意味着他们能解开那些其他工具因为“内存不够”而解不开的难题。

4. 总结

这就好比：
以前，计算机要检查一个复杂的系统，就像要把一本字典里的每一个字都抄写一遍才能检查拼写，结果抄写过程太慢，纸也不够用。
现在，作者发明了两种技巧：

合并同类项： 把长得一样、用法一样的字合并成一个符号。
删减废话： 把那些在这个句子里根本不会出现的字直接删掉。

结果就是，计算机只需要抄写很少的一部分内容，就能快速、准确地完成检查任务。这不仅节省了时间和空间，还让计算机能处理以前根本处理不了的超级复杂系统。

一句话总结： 这是一篇关于如何给复杂的计算机模型“瘦身”的论文，通过智能地合并和过滤信息，让计算机能更快、更省地解决难题。

论文技术总结：高效展开有色佩特里网的方法

论文标题：Methods for Efficient Unfolding of Colored Petri Nets
发表期刊：Fundamenta Informaticae 189(3-4) : 297–320 (2022)
作者：Alexander Bilgram, Peter G. Jensen, Thomas Pedersen, Jiří Srba, Peter H. Taankvist (奥尔堡大学)

1. 研究背景与问题 (Problem)

背景：
有色佩特里网（Colored Petri Nets, CPN）是对传统位置/变迁（Place/Transition, P/T）网的扩展，通过引入“颜色”（Color）来紧凑地表示分布式系统。CPN 允许每个库所（Place）拥有颜色域，令牌（Token）具有特定颜色，弧（Arc）和变迁（Transition）带有表达式和守卫（Guard）。

核心问题：
虽然 CPN 模型紧凑且易于人类阅读，但许多验证工具（如模型检测器）仅支持 P/T 网。因此，需要将 CPN 展开（Unfolding） 为等价的 P/T 网。

展开机制：CPN 中的每个库所根据颜色域展开为多个 P/T 库所，每个变迁根据满足守卫的变量绑定展开为多个 P/T 变迁。
挑战：如果颜色域较大，展开后的 P/T 网规模会呈指数级爆炸，导致内存溢出或计算时间过长，甚至无法完成展开。现有的展开工具（如 MCC, Spike, ITS-Tools）在处理某些大型基准测试模型（如 Model Checking Contest 中的 FamilyReunion 和 DrinkVendingMachine）时仍面临困难。

目标：
提出基于静态分析的新方法，在展开前减少 CPN 的规模，从而显著降低展开后 P/T 网的大小，同时保持验证的正确性。

2. 方法论 (Methodology)

作者提出了两种互补的静态分析技术，并集成在模型检测工具 TAPAAL 中：

方法 A：颜色商化 (Color Quotienting)

核心思想：识别行为等价的令牌颜色。如果两个不同的颜色在网的整个执行过程中产生双模拟（Bisimilar）行为，可以将它们归并为一个等价类。
实现机制：
1. 稳定划分（Stable Partition）：定义库所颜色域的划分 $\delta$ 。如果两个标记（Marking）在划分下的等价类中令牌数量总和相等，则称它们等价。
2. 稳定性检查：通过迭代细化算法（类似分区细化），确保对于任何变迁，如果两个等价标记能触发该变迁，则它们产生的后继标记也必须等价。
3. 构建商网：将等价的颜色合并为一个代表颜色，将等价的绑定合并。这减少了需要展开的颜色数量和绑定数量。
优势：直接减少展开后的库所和变迁数量，特别是当模型中存在大量对称或冗余颜色时。

方法 B：颜色近似 (Color Approximation)

核心思想：过近似（Overapproximation）计算每个库所中可能出现的颜色集合，排除那些在初始标记下永远无法到达的颜色。
实现机制：
1. 颜色扩展函数：定义一个函数 $E$ ，从初始标记的颜色集合开始，根据弧表达式和守卫条件，迭代计算可能传播到各库所的颜色。
2. 不动点计算：计算该函数的最小不动点，得到每个库所可达颜色的上界集合。
3. 剪枝：在展开时，仅针对这些“可达”颜色生成库所和变迁。如果某个绑定依赖于不可达的颜色，则该绑定被剔除。
优势：处理那些由于守卫条件或初始状态限制而实际上无法触发的部分，减少无效展开。

组合策略

两种方法可以结合使用（Method A+B）：先进行颜色近似剔除不可达颜色，再对剩余颜色进行商化归并，从而获得最大的规模缩减效果。

3. 主要贡献 (Key Contributions)

提出两种新颖的静态分析技术：
- 颜色商化：基于双模拟理论，将行为等价的颜色归并，证明了商化后的网与原网双模拟等价（Bisimilar）。
- 颜色近似：基于可达性分析，精确计算并剔除不可达颜色，证明了缩减后的网在可达片段上与原网同构。
算法实现与优化：
- 设计了高效的算法（如 Stabilize 算法）来计算稳定划分，并针对整数 CPN（Integer CPN）提出了基于区间（Interval）的紧凑表示，避免了对单个颜色的显式枚举，提高了计算效率。
- 在 TAPAAL 工具链中实现了完整的展开器。
全面的实验评估：
- 在 2021 年模型检测竞赛（Model Checking Contest, MCC）的基准测试集上进行了广泛测试。
- 与当前最先进的展开工具（MCC/TINA, ITS-Tools, Spike）进行了对比。

4. 实验结果 (Results)

实验在 AMD Epyc 7642 处理器、15GB 内存、5 分钟超时的环境下进行，对比了 2021 MCC 竞赛中的 213 个模型。

展开能力（覆盖范围）：
- 组合方法（A+B）成功展开了 203 个模型，是所有工具中覆盖最广的。
- 其中，有 3 个模型（DrinkVendingMachine48, 76, 98）是其他任何工具都无法展开的，这主要归功于颜色商化方法。
- 相比之下，Spike 展开 170 个，Tapaal 基础版 192 个，ITS-Tools 193 个，MCC 195 个。
展开网规模（Size Reduction）：
- 在 213 个模型中，组合方法生成的展开网规模比所有其他工具都小或相等。
- 对于 144 个模型，其规模严格小于其他工具。
- 对于 45 个模型，规模缩减了至少一个数量级（Order of Magnitude）。
展开时间（Performance）：
- 尽管引入了复杂的静态分析，展开时间并未成为瓶颈。
- 在最慢的 80 个模型中，组合方法的运行时间比 ITS-Tools 和 MCC 快了近一个数量级，且比 Spike 快得多。
- 证明了高级静态分析的开销远小于其带来的规模缩减收益。
模型检测查询解答率（Query Verification）：
- 使用展开后的网进行查询验证（共 20,448 个查询）。
- 组合方法（A+B）成功解答了 15,924 个查询（77.9%），比 MCC（73.9%）高出 4%，比 ITS-Tools（72.0%）高出 5.9%。
- 这直接证明了更小的展开网规模使得模型检测器能够处理更多复杂的查询。

5. 意义与结论 (Significance & Conclusion)

理论意义：证明了通过静态分析（双模拟归并和可达性分析）可以在不损失语义等价性的前提下，显著压缩有色佩特里网的展开规模。
工程价值：
- 解决了现有工具在处理大规模 CPN 模型时的“指数爆炸”瓶颈。
- 使得原本无法展开或无法验证的大型工业级/竞赛级模型变得可验证。
- 在 TAPAAL 中的实现展示了该方法在实际工具中的高效性和实用性。
未来展望：作者计划将这种方法与直接应用于有色网的结构性归约（Structural Reduction）技术相结合，进一步挖掘优化潜力。

总结：该论文通过创新的“颜色商化”和“颜色近似”技术，成功解决了有色佩特里网展开过程中的规模爆炸问题。实验表明，该方法在展开速度、展开网规模以及最终模型检测查询的解答率上，均全面超越了当前最先进的工具，为复杂分布式系统的形式化验证提供了强有力的支持。