A Decision Diagram Operation for Reachability
Sebastiaan Brand, Thomas B\"ack, Alfons Laarman

TL;DR
This paper introduces the REACH decision diagram operation for fixpoint computation in model checking, offering a simpler alternative to saturation that often performs better, especially on low-locality transition relations, with effective parallelization.
Contribution
The paper presents the REACH operation for decision diagrams, providing algorithms and parallel implementations that outperform saturation on many benchmarks and can complement existing tools.
Findings
REACH often outperforms saturation on various benchmarks.
Parallel REACH scales well up to 16 cores, less so at 64 cores.
REACH outperforms ITS-tools on 29% of tested models.
Abstract
Saturation is considered the state-of-the-art method for computing fixpoints with decision diagrams. We present a relatively simple decision diagram operation called REACH that also computes fixpoints. In contrast to saturation, it does not require a partitioning of the transition relation. We give sequential algorithms implementing the new operation for both binary and multi-valued decision diagrams, and moreover provide parallel counterparts. We implement these algorithms and experimentally compare their performance against saturation on 692 model checking benchmarks in different languages. The results show that the REACH operation often outperforms saturation, especially on transition relations with low locality. In a comparison between parallelized versions of REACH and saturation we find that REACH obtains comparable speedups up to 16 cores, although falls behind saturation at 64…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Engineering Research · Software Reliability and Analysis Research
