On-the-fly Unfolding with Optimal Exploration for Linear Temporal Logic Model Checking of Concurrent Software and Systems

Context: Linear temporal logic (LTL) model checking faces a significant challenge known as the state-explosion problem. The on-the-fly method is a solution that constructs and checks the state space simultaneously, avoiding generating all states in advance. But it is not effective for concurrent interleaving. Unfolding based on Petri nets is a succinct structure covering all states that can mitigate this problem caused by concurrency. Many state-of-the-art methods optimally explore a complete unfolding structure using a tree-like structure. However, it is difficult to apply such a tree-like structure directly to the traditional on-the-fly method of LTL. At the same time, constructing a complete unfolding structure in advance and then checking LTL is also wasteful. Thus, the existing optimal exploration methods are not applicable to the on-the-fly unfolding. Objective: To solve these challenges, we propose an LTL model-checking method called on-the-fly unfolding with optimal exploration. This method is based on program dependence net (PDNet) proposed in the previous work. Method: Firstly, we define conflict transitions of PDNet and an exploration tree with a novel notion of delayed transitions, which differs from the existing tree-like structure. The tree improves the on-the-fly unfolding by exploring each partial-order run only once and avoiding enumerating all possible combinations. Then, we propose an on-the-fly unfolding algorithm that simultaneously constructs the exploration tree and generates the unfolding structure while checking LTL. Results: We implement a tool for concurrent programs. It also improves traditional unfolding generations and performs better than SPIN and DiVine on the used benchmarks.