Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Symbolic Model Checking in External Memory

Steffan Christ Sølvsten, Jaco van de Pol

TL;DR

This work addresses the RAM-memory bottleneck in symbolic model checking with BDDs by advancing Adiar’s external-memory capabilities. It introduces monotone variable substitution and a refined relational product, and further integrates variable substitution and conjunction with existential quantification into a single AndExists pipeline within a time-forward processing framework, leveraging I/O-efficient sweeps. The results show notable improvements for small to medium BDDs (up to 47% speedups) and robust performance for larger instances where existential quantification dominates, with Adiar remaining largely memory-independent and outperforming CAL on large problems. The practical impact is a scalable approach to model checking tasks (e.g., Petri nets and Boolean networks) that exceed traditional RAM limits, enabling reachability, deadlock analysis, and SCC decomposition at larger scales.

Abstract

We extend the external memory BDD package Adiar with support for monotone variable substitution. Doing so, it now supports the relational product operation at the heart of symbolic model checking. We also identify additional avenues for merging variable substitution fully and the conjunction operation partially inside the relational product's existential quantification step. For smaller BDDs, these additional ideas improve the running of Adiar for model checking tasks up to 47%. For larger instances, the computation time is mostly unaffected as it is dominated by the existential quantification. Adiar's relational product is about one order of magnitude slower than conventional depth-first BDD implementations. Yet, its I/O-efficiency allows its running time to be virtually independent of the amount of internal memory. This allows it to compute on BDDs with much less internal memory and potentially to solve model checking tasks beyond the reach of conventional implementations. Compared to the only other external memory BDD package, CAL, Adiar is several orders of magnitude faster when computing on larger instances.

Symbolic Model Checking in External Memory

TL;DR

This work addresses the RAM-memory bottleneck in symbolic model checking with BDDs by advancing Adiar’s external-memory capabilities. It introduces monotone variable substitution and a refined relational product, and further integrates variable substitution and conjunction with existential quantification into a single AndExists pipeline within a time-forward processing framework, leveraging I/O-efficient sweeps. The results show notable improvements for small to medium BDDs (up to 47% speedups) and robust performance for larger instances where existential quantification dominates, with Adiar remaining largely memory-independent and outperforming CAL on large problems. The practical impact is a scalable approach to model checking tasks (e.g., Petri nets and Boolean networks) that exceed traditional RAM limits, enabling reachability, deadlock analysis, and SCC decomposition at larger scales.

Abstract

We extend the external memory BDD package Adiar with support for monotone variable substitution. Doing so, it now supports the relational product operation at the heart of symbolic model checking. We also identify additional avenues for merging variable substitution fully and the conjunction operation partially inside the relational product's existential quantification step. For smaller BDDs, these additional ideas improve the running of Adiar for model checking tasks up to 47%. For larger instances, the computation time is mostly unaffected as it is dominated by the existential quantification. Adiar's relational product is about one order of magnitude slower than conventional depth-first BDD implementations. Yet, its I/O-efficiency allows its running time to be virtually independent of the amount of internal memory. This allows it to compute on BDDs with much less internal memory and potentially to solve model checking tasks beyond the reach of conventional implementations. Compared to the only other external memory BDD package, CAL, Adiar is several orders of magnitude faster when computing on larger instances.
Paper Structure (10 sections, 3 theorems, 2 equations, 2 figures)

This paper contains 10 sections, 3 theorems, 2 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Preliminaries
  4. I/O Model
  5. Binary Decision Diagrams
  6. Relational Product
  7. I/O-efficient BDD Manipulation
  8. I/O-efficient Relational Product
  9. I/O-efficient Variable Substitution
  10. An I/O-efficient AndExists

Key Result

proposition thmcounterproposition

A monotone variable substitution can be applied to a BDD of $N$ nodes in $\mathcal{O} ( N )$ time and using $2 \cdot \tfrac{N}{B}$ I/Os.

Figures (2)

  • Figure 1: The transition system in \ref{['fig:bdd_example:ts']} can be represented as the BDD for its relation relation \ref{['fig:bdd_example:rel']} and the BDD for its initial state in \ref{['fig:bdd_example:init']} via a unary encoding and an interleaved variable ordering. One (More) relational product of these two BDDs creates the one in \ref{['fig:bdd_example:next']} (\ref{['fig:bdd_example:closure']}). For readability, we suppress the $\bot$ terminal. The $\top$ terminal is drawn as a box while BDD nodes are drawn as circles surrounding their decision variable. The then, resp. else, child is drawn solid, resp. dashed.
  • Figure 2: The Apply--Reduce pipelines in Adiar.

Theorems & Definitions (4)

  • proposition thmcounterproposition
  • proof
  • proposition thmcounterproposition
  • proposition thmcounterproposition