When checking concurrent software using a finite-state model, we face a formidable state explosion problem. One solution to this problem is dependence-based program slicing, whose use can effectively reduce verification time. It is orthogonal to other model-checking reduction techniques. However, when slicing concurrent programs for model checking, there are conversions between multiple irreplaceable models, and dependencies need to be found for variables irrelevant to the verified property, which results in redundant computation. To resolve this issue, we propose a Program Dependence Net (PDNet) based on Petri net theory. It is a unified model that combines a control-flow structure with dependencies to avoid conversions. For reduction, we present a PDNet slicing method to capture the relevant variables' dependencies when needed. PDNet in verifying linear temporal logic and its on-demand slicing can be used to significantly reduce computation cost. We implement a model-checking tool based on PDNet and its on-demand slicing, and validate the advantages of our proposed methods.

翻译：在对并发软件进行有限状态模型检验时，会遭遇严峻的状态爆炸问题。基于依赖的程序切片是解决该问题的一种有效途径，能够显著缩减验证时间，且与其他模型检验精简技术具有正交性。然而，在面向模型检验对并发程序实施切片时，需在多个不可替代模型间进行转换，并且需要为与被验证性质无关的变量寻找依赖关系，从而导致冗余计算。为解决此问题，我们提出基于Petri网理论的程序依赖网。该模型统一融合了控制流结构与依赖关系，避免了模型转换。在精简方面，我们提出一种PDNet切片方法，可在需要时捕获相关变量的依赖关系。PDNet在线性时态逻辑验证及其按需切片可显著降低计算开销。我们基于PDNet及其按需切片实现了模型检验工具，并验证了所提方法的优越性。