Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
summary
Paper implements automata-driven stubborn sets and a heuristically guided search inside TAPAAL 3.9, reusing progression formulas from the Büchi automaton to both prune interleavings and prioritize successors. The reduction enforces four preservation rules (com, r, key, safe) so LTL counterexamples are preserved; the safe rule blocks actions that would “make progression formulas more true.” Evaluation on the Model Checking Contest 2021 dataset (~1,200 Petri nets × 32 formulas ≈ 38,000 instances) shows a 6.5 percentage-point lead over IGS (94.3% vs 87.8%, ≈2,500 extra queries) and a 1.1 point gain attributable to the partial-order reduction alone.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:35The Problem
- 1:43Outline
- 3:17Guided Search
- 6:35Partial Order Reduction
- 7:48LTL Preserving Techniques
- 9:21StopSet Method
- 13:22Safe Actions
- 14:27Safe Actions Example
- 20:45Conclusion
- 21:20Questions
- 22:14Impact
- 23:18Question
- 27:51Extra Question
related talks
22mOptimal Stateless Model Checking under the Release-Acquire Semantics
20mTruly Stateless, Optimal Dynamic Partial Order Reduction
16mPomsets with Preconditions: A Simple Model of Relaxed Memory
21mA Navigation Logic for Recursive Programs with Dynamic Thread Creation
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
28mCAAT: Consistency as a Theory
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
19mScenario-based Proofs for Concurrent Objects