A decision diagram operation for reachability

DOI10.1007/978-3-031-27481-7_29MaRDI QIDQ6132656zbMATH OpenFDO

Authors Sebastiaan Brand, Thomas Bäck, Alfons W. Laarman

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2212.03684

zbMATH Keywords

model checkingreachabilitysaturationdecision diagramsBDDsMDDs

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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 cores. Finally, in a comparison with the state-of-the-art model checking tool ITS-tools we find that REACH outperforms ITS-tools on 29% of models, suggesting that REACH can be useful as a complementary method in an ensemble tool.

Recommendations

• Improving Saturation Efficiency with Implicit Relations
• Hierarchical Set Decision Diagrams and Automatic Saturation
• Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams
• Building efficient model checkers using hierarchical set decision diagrams and automatic saturation
• scientific article; zbMATH DE number 1629965

Cites work

• scientific article; zbMATH DE number 1701768 (Why is no real title available?)
• scientific article; zbMATH DE number 1701774 (Why is no real title available?)
• scientific article; zbMATH DE number 1956594 (Why is no real title available?)
• scientific article; zbMATH DE number 1863167 (Why is no real title available?)
• scientific article; zbMATH DE number 1423226 (Why is no real title available?)
• A lattice-theoretical fixpoint theorem and its applications
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Gradient-based variable ordering of decision diagrams for systems with structural units
• Graph-Based Algorithms for Boolean Function Manipulation
• Improving the variable ordering of OBDDs is NP-complete
• Symbolic Reachability for Process Algebras with Recursive Data Types
• Symbolic model checking with sentential decision diagrams
• Symbolic model checking: \(10^{20}\) states and beyond
• The art of computer programming. Volume 4A. Combinatorial algorithms. Part 1.
• Verification of asynchronous circuits by BDD-based model checking of Petri nets

Cited in

(1)

• Improving Saturation Efficiency with Implicit Relations

This page was built for publication: A decision diagram operation for reachability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6132656)