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

TL;DR

This work tackles state explosion in Linear Temporal Logic (LTL) model checking for concurrent software by introducing on-the-fly unfolding with optimal exploration, grounded in Program Dependence Nets (PDNet). It defines conflict transitions and a novel delayed-transition concept to build an exploration tree that guides on-the-fly unfolding and simultaneous Büchi PDNet synchronization, yielding the Büchi PDNet product $\mathcal{N}_{\neg\psi}$ for counterexample detection. The core contributions include formal definitions of conflict transitions, the exploration tree, and an end-to-end on-the-fly unfolding algorithm with cutoff-based termination, implemented in the PUPER tool. Experimental results show that PUPER outperforms traditional unfolding generations and existing LTL tools (e.g., SPIN, DiVine) on concurrent benchmarks, demonstrating improved scalability and practical impact for verifying LTL properties in concurrent systems. The approach provides a concrete, scalable pathway to correct and efficient LTL verification in real-world multi-threaded environments, with potential for further optimization via more compact unfolding representations.

Abstract

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.

Figures (5)

• Figure 1: Motivating Example. ($a$) An Example Concurrent program $\mathcal{P}$ and LTL formula ($b$) PDNet ($c$) Büchi Automaton ($d$) Model checking ($e$) The Event Structure for the example program ($f$) PDNet Unfolding ($g$) Event Relations ($h$) Exploration Tree ($i$) The Büchi PDNet ($j$) PDNet Synchronization ($k$) Unfolding of PDNet Synchronization.
• Figure 2: Conflict Transitions of PDNet. ($a$) $t_1$ is $assign$ transition and $t_2$ is $assign$ transition. ($b$) $t_1$ is $assign$ transition and $t_2$ is $branch$ transition. ($c$) $t_1$ is $lock$ transition or $wait$ transition for $wa_3$ and $t_2$ is $lock$ transition or $wait$ transition of $wa_3$. ($d$) $t_1$ is $lock$ transition or $wait$ transition for $wa_3$ and $t_2$ is $unlock$ transition or $wait$ transition for $wa_1$. ($e$) $t_1$ is $unlock$ transition or the $wait$ transition for $wa_1$ and $t_2$ is $lock$ transition or $wait$ transition of $wa_3$. ($f$) $t_1$ is $unlock$ transition or the $wait$ transition for $wa_1$ and $t_2$ is $unlock$ transition $wait$ transition of $wa_1$. ($g$) $t_1$ is the $wait$ transition for $wa_2$ and $t_2$ is $signal$ transition. ($h$) $t_1$ is $signal$ transition and $t_2$ is the $wait$ transition for $wa_2$. ($i$) $t_1$ is the $signal$ transition and $t_2$ is $signal$ transition.
• Figure 3: On-the-fly Unfolding with optimal exploration
• Figure 4: Function CUTOFF
• Figure 5: The Exploration Tree.

Theorems & Definitions (27)

• Definition 1: PDNet
• Theorem 1
• Definition 2: Branching Process of PDNet
• Definition 3: Configuration
• Definition 4: Possible Extension of PDNet Unfolding
• Definition 5: Adequate Order
• Definition 6: Cut-off of PDNet Unfolding
• Theorem 2
• Definition 7: Reference Set and Definition Set of PDNet
• Definition 8: Conflict Transitions of PDNet