一句话总结

来自印度理工学院达尔瓦德分校和喀拉拉邦国家技术学院的 Phawade 等人提出了 2D-BMC，这是一种新颖的有界模型检测算法，可同时限制执行步数和令牌数量，用于验证无界 Petri 网针对带线性整数算术的线性时序逻辑（LTL_LIA）的性质，支持并发语义，并在复杂性质上优于现有工具。

主要贡献

• 我们提出了 2D-BMC，一种新颖的有界模型检测算法，可同时限制无界 Petri 网的执行长度和令牌数量，支持在并发语义下验证带线性整数算术的 LTL（LTL_LIA）性质。
• 我们为无界 Petri 网的交错执行和并发执行提供了 SMT 编码，允许精确指定基于令牌的不变式和时序性质，超越传统的可达性和覆盖性检查。
• 我们实现并评估了 DCModelChecker 2.0，展示了其在无界网中生成反例的能力，同时保留网结构，并在选定基准测试中展现出与 TAPAAL 和 ITS-Tools 相当的性能。

引言

作者利用有界模型检测（BMC）在并发语义下验证无界 Petri 网，填补了现有工具主要依赖交错执行且仅检查可达性或覆盖性的空白。先前的方法难以捕捉真正的并发性，且缺乏对更丰富时序性质（如可用 LTL 带线性整数算术 LTL_LIA 表达的性质）的支持。其主要贡献是 2D-BMC —— 一种新颖的 BMC 变体，同时限制执行长度和令牌数量 —— 以及两个工具版本（DCModelChecker 1.0 和 2.0），实现了该方法，支持在交错或并发语义下验证 LTL_LIA 性质，同时生成反例用于调试。

方法

作者采用结构化方法，基于 SMT 的有界模型检测对无界 Petri 网进行建模与验证，重点关注并发语义和二维边界。核心方法整合了形式化网语义、SMT 编码和自定义工具链，以处理用 $LTL_{LIA}$LTLLIA​ 表达的时序性质。

建模始于标准 Petri 网形式化：一个三元组 $N = (P, T, F)$N=(P,T,F)，其中 $P$P 是位置集合，$T$T 是迁移集合，$F$F 是定义带可选权重的有向弧的流函数。标记 $M: P \rightarrow \mathbb{N}_0$M:P→N0​ 表示网的状态，指示各位置上的令牌分布。迁移根据启用规则触发：迁移 $t$t 在标记 $M$M 下启用，当且仅当对所有 $p \in P$p∈P，有 $M(p) \geq \text{pre}_N(t, p)$M(p)≥preN​(t,p)。触发后，后继标记 $M'$M′ 按公式 $M'(p) = M(p) - F(p, t) + F(t, p)$M′(p)=M(p)−F(p,t)+F(t,p) 对所有 $p \in P$p∈P 计算。可达图记录从初始标记 $M_0$M0​ 出发的所有可能状态转移。

如下图所示，作者区分了交错语义和并发语义。在交错语义中，每一步仅允许一个迁移触发。相比之下，并发语义允许一个启用迁移的子集 $\tau' \subseteq \tau$τ′⊆τ 同时触发，前提是前位置的令牌总消耗不超过可用令牌。并发触发规则定义为：

该规则支持更紧凑且更真实地表示并行系统行为。

为支持 Z3 等 SMT 求解器进行验证，作者构建了网的符号表示。定义两个关键矩阵：$Wt[m][l]$Wt[m][l] 表示网权重变化（出弧减入弧），$iWt[m][l]$iWt[m][l] 表示入弧权重。迁移函数 $TF$TF 通过组合前提条件（确保触发所需令牌）和后置条件（更新位置标记）构建。对于并发语义，$TF$TF 不强制每步仅触发一个迁移，与交错语义不同。

验证目标是 $LTL_{LIA}$LTLLIA​，即扩展了位置令牌计数上整数算术的线性时序逻辑。公式由原子比较（如 $(\#p < \#q)$(#p<#q)）和时序算子（X, F, G, U）构成。为应用有界模型检测，作者引入二维边界 $k = \lambda + \kappa$k=λ+κ，其中 $\lambda$λ 限制执行步数，$\kappa$κ 限制令牌总数。有界语义将状态空间限制在长度为 $\lambda$λ 且最多含 $\kappa$κ 个令牌的执行路径上。

2D-BMC 编码 $[\mathcal{M}, \psi]_{\langle \lambda, \kappa \rangle}$[M,ψ]⟨λ,κ⟩​ 将网模型的 SMT 编码 $[\mathcal{M}]_{\langle \lambda, \kappa \rangle}$[M]⟨λ,κ⟩​ 与否定性质 $\psi = \neg \phi$ψ=¬ϕ 的编码 $[\psi]_{\langle \lambda, \kappa \rangle}^0$[ψ]⟨λ,κ⟩0​（无环路径）或 $l[\psi]_{\langle \lambda, \kappa \rangle}^0$l[ψ]⟨λ,κ⟩0​（含回环至状态 $l$l 的路径）结合。模型编码递归构建：$[\mathcal{M}]_{\langle 0, \kappa \rangle}$[M]⟨0,κ⟩​ 编码初始状态及令牌边界，$[\mathcal{M}]_{\langle \lambda, \kappa \rangle}$[M]⟨λ,κ⟩​ 通过添加迁移关系 $T(s_{\lambda-1}, s_{\lambda})$T(sλ−1​,sλ​) 和新状态的令牌边界扩展。

如下图所示，2D-BMC 算法通过递增 $k$k 探索状态空间，对每个 $k$k 迭代所有可能的 $(\lambda, \kappa)$(λ,κ) 对。对每对组合，构建并检查 SMT 公式。若可满足，返回反例轨迹；若不可满足，增加边界。

如下图所示，工具架构接受 PNML 格式的 Petri 网和 $LTL_{LIA}$LTLLIA​ 性质。预处理模块基于 ANTLR 构建，解析并验证输入，构建内部数据结构。核心模型检测器应用 2D-BMC 算法，为 Z3 生成 SMT 约束。求解器返回 UNSAT（性质在边界内成立）或 SAT 并附带反例轨迹（性质被违反）。

工作流始于将性质 $\phi$ϕ 否定为 $\psi$ψ 并初始化边界 $k=0$k=0。对每个 $k$k，迭代所有和为 $k$k 的 $(\lambda, \kappa)$(λ,κ) 对，构建相应 SMT 公式并查询 Z3。搜索持续至找到反例或达到外部终止边界。此系统性探索确保在有界状态空间内全面验证。

实验

• 通过与 ITS-Tools 在 LTLFireability 性质上对比验证 DCModelChecker 2.0 的正确性，达到 90% 工具置信度，对假性质结果一致确认其可靠性。
• 展示了验证超出 MCC 表达能力的 FireabilityCardinality 性质的能力，显示更高边界下反例发现率增加。
• 成功验证其他工具（ITS-Tools、TAPAAL）仅报告为假的无界 Petri 网，而 DCModelChecker 2.0 提供反例轨迹。
• 验证了 LTL_LIA 中的合成不变式，这是 MCC 工具和 DCModelChecker 1.0 均不具备的能力，扩展了可验证性质的范围。
• 当前工具因反例生成开销在性能上落后于最先进工具，未来工作将聚焦并发语义和优化编码。

作者使用 DCModelChecker 2.0 验证无界 Petri 网，并与 DCModelChecker 1.0、ITS-Tools 和 TAPAAL 比较性能，显示 DCModelChecker 2.0 一致返回带反例轨迹的假性质，同时与其他工具结果一致。结果表明，DCModelChecker 2.0 执行时间慢于 ITS-Tools 和 TAPAAL，但通过反例生成提供额外诊断价值。尽管当前性能受限，该工具处理无界网并生成轨迹的能力使其成为互补选项。

作者使用 DCModelChecker 2.0 验证 LTLFireability 性质并与 ITS-Tools 对比，通过比较两者对假性质结果一致或 DCModelChecker 2.0 返回反例的情况，达到 0.90 的工具置信度。结果表明，DCModelChecker 2.0 在大多数情况下正确识别假性质，但当 ITS-Tools 报告为真时会产生一些错误输出。该工具的 2D-BMC 策略不完备，如 UNSAT 结果可能在更高边界下变为假。