A decision diagram operation for reachability

DOI10.1007/978-3-031-27481-7_29zbMath1529.68153arXiv2212.03684MaRDI QIDQ6132656

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

reachabilitymodel checkingsaturationdecision diagramsBDDsMDDs

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic model checking: \(10^{20}\) states and beyond
• Symbolic model checking with sentential decision diagrams
• A lattice-theoretical fixpoint theorem and its applications
• Graph-Based Algorithms for Boolean Function Manipulation
• Improving the variable ordering of OBDDs is NP-complete
• Gradient-Based Variable Ordering of Decision Diagrams for Systems with Structural Units
• Verification of asynchronous circuits by BDD-based model checking of Petri nets
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Symbolic Reachability for Process Algebras with Recursive Data Types

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