Symbolic Model Checking in External Memory

TL;DR

This paper enhances an external memory BDD package with relational product support, significantly improving efficiency and enabling larger model checking tasks beyond traditional methods.

Contribution

It introduces support for relational product in external memory BDDs and demonstrates substantial performance improvements over existing tools.

Findings

Up to 47% faster for smaller BDDs

Maintains efficiency on large instances with minimal memory

Outperforms CAL by several orders of magnitude on large tasks

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.