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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Preserving LTL Properties in Sweep-Line State Space Exploration with Partial-Order Reduction

  • Sami Evangelista,
  • Lars M. Kristensen,
  • Laure Petrucci

摘要

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.