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的性能表现。