Unfolding can tackle the path-explosion problem caused by concurrency. Traditional unfolding generation faces an NP-complete problem when adding events to the unfolding structure, which also exists in the case of verifying linear temporal logic (LTL). The reason is that it is necessary to enumerate possible concurrent event combinations after adding an event. Many state-of-the-art methods optimally explore unfolding-based structure (called event structure) by a tree-like structure, which should be constructed on the event structure with complete conflict and causal relations. However, a synchronization of a Petri net and the Buchi representation of LTL as a folded net can not represent complete conflict and causal relations. Thus, it is difficult to apply such a tree-like structure directly on the folded net. To resolve this difficulty, we propose a new method, called partial-order checking with unfolding, to verify LTL based on PDNet (program dependence net). We define an exploration tree with a new notion of delayed transitions, which is different from the existing tree-like structure. It improves the unfolding generation by avoiding all possible event combinations. Then, we propose an algorithm to simultaneously construct the exploration tree while generating the unfolding structure, as well as checking LTL. We implement a tool PUPER for concurrent programs with POSIX threads. It improves traditional unfolding generations via our exploration tree-based algorithms and shows better performance than SPIN and DiVine on the used benchmarks.

翻译：摘要：展开技术能够解决并发导致的路径爆炸问题。传统展开生成在向展开结构添加事件时面临NP完备问题，这在验证线性时序逻辑（LTL）时同样存在。其原因在于添加事件后需要枚举所有可能的并发事件组合。许多前沿方法通过树状结构优化探索基于展开的结构（称为事件结构），该结构需要构建在具有完整冲突关系和因果关联的事件结构之上。然而，Petri网与LTL的Büchi表达作为折叠网进行同步时，无法表征完整的冲突关系和因果关联。因此，这类树状结构难以直接应用于折叠网。为解决这一难题，我们提出了一种名为"基于展开的偏序检查"的新方法，基于PDNet（程序依赖网）验证LTL。我们定义了具有延迟转移新概念的探索树，该探索树不同于现有树状结构，通过避免所有可能的事件组合来改进展开生成。随后，我们提出一种算法，在生成展开结构的同时同步构建探索树并完成LTL验证。我们为采用POSIX线程的并发程序实现了工具PUPER。该工具通过基于探索树的算法改进了传统展开生成，并在所用基准测试中展现出优于SPIN和DiVine的性能。