Serialized BDDs from the Model Checking Competition

This is a collection of real-life BDDs created from a reachability analysis of 1-safe Petri nets from the Model Checking Competition. These can be used to benchmark the performance of one (or more) BDD packages.

Contents

Each .zip archive multiple .zip archives for the models from that particular year. Each archive for one such model includes the following serialized BDDs:

relation.bdd: A single joined relation of all transitions in the Petri net.

states_.bdd: The first set of states with a BDD of magnitude 2ⁿ that was constructed while computing all reachable states in the Petri net.

Usage

These BDDs can be used in two of the benchmarks from the BDD Benchmarking Suite:

Apply: Load two (or more) BDDs and combine them with either an or or an and operation. This is a reimplementation of the benchmark by Pastva and Henzinger (Zenodo).

RelProd: Load the relation (relation.bdd) and (states_.bdd) and combine them with a forward or backwards application of the relational product.

Reproduction

See README.md for all the details.