## The size of BDDs and other data structures in temporal logics
modelchecking

**Andrea Ferrara, Paolo Liberatore, and Marco Schaerf**
*IEEE Transactions on Computers*

Temporal Logic Model Checking is a verification method in which
we describe a system, the model, and then we verify whether
important properties, expressed in a temporal logic formula, hold
in the system. Many Model Checking tools employ BDDs or some
other data structure to represent sets of states. It has been
empirically observed that the BDDs used in these algorithms may
grow exponentially as the model and formula increase in size. We
formally prove that no kind of data structure of polynomial size
can represent the set of valid initial states for all models and
all formulae. This result holds for all data structures where a
state can be checked in polynomial time. Therefore, it holds not
only for all types of BDDs regardless of variable ordering, but
also for more powerful data structures, such as RBCs, MTBDDs,
ADDs and SDDs. Thus, the size explosion of BDDs is not a limit
of these specific data representation structures, but is
unavoidable: every formalism used in the same way would lead to
an exponential size blow up.

@article{libe-scha-16,
title = {The size of BDDs and other data structures in temporal
logics modelchecking},
year = {2016},
author = {Ferrara, Andrea and Liberatore, Paolo and Schaerf,
Marco},
journal = {IEEE Transactions on Computers},
pages = {3148--3156},
volume = {65},
}

doi: 10.1109/TC.2015.2512872