Preserving LTL Properties in Sweep-Line State Space Exploration with Partial-Order Reduction
摘要
Model checking often requires the combined use of multiple reduction techniques to mitigate the state explosion problem. The contribution of this paper is a generalised sweep-line algorithm that enforces the conditions necessary for partial-order reduction in the form of stubborn sets to preserve LTL \(_{-X}\) properties. The core idea in our algorithm is to compute strongly connected components and detect cycles within each state space layer explored by the sweep-line method, while leveraging persistent states as anchor states for enforcing cross-layer partial-order reduction conditions. We have implemented our new algorithm and conducted an experimental evaluation on set of benchmarks from the Petri Nets Model Checking Contest. The results show our LTL \(_{-X}\) preserving combination of sweep-line exploration with partial-order reduction even in a conservative implementation may substantially reduce peak memory usage. Furthermore, the overhead is mostly similar to plain partial-order preserving LTL \(_{-X}\) reduction.