Binary (Boolean?) decision diagrams (BDDs) have emerged as a very important symbolic representation for large sets, especially state spaces of finite-state verification problems. In many cases, BDDs have been able to handle state spaces that would be utterly hopeless if the states were to be stored individually. Research in verification with BDDs is extensive - try searching the web. In recent years, most of our work using BDDs has addressed the question of how to verify high-level descriptions of protocols, described at the same level as with Murphi, using them. In many cases, it turns out to be surprisingly difficult for BDDs to do better than an explicit state verify such as Murphi.
We first implemented a reasonably high-level language with integer arithmetic, records, and arrays, for describing and verifying protocols. A paper about this was published in 1992:
"Higher-Level Specification and Verification With BDDs," Alan J. Hu, David L. Dill, Andreas J. Drexler and C. Han Yang, Workshop on Computer-Aided Verification, Montreal, Quebec, June 29 -- July 2, 1992.We then observed that BDDs did not work as well as expected for some problems, such as directory-based cache coherence protocols (which happened to be our first example). The BDDs became very large. We came up with two techniques to get around some, but not all, of the causes of BDD blowup. Both ideas attempt to eliminate redundant information between variables in the BDD.
The first idea is to note that in a correctly operating protocol, there are dependent variables which are functions of other independent variables. The dependent variables are stored explicitly for efficiency.
"Reducing BDD Size by Exploiting Functional Dependencies," Alan J. Hu and David L. Dill, 30th Design Automation Conference, 1993, pp. 266-271.
The other technique is to break the BDD for the reachable state space into a collection of smaller BDDs that isolate parts of the system or individual properties. Various criteria can be used for how to do this. We have two papers describing variations on this approach.
"Efficient Verification with BDDs Using Implicitly Conjoined Invariants," Alan J. Hu and David L. Dill, Computer Aided Verification, LNCS 697, Springer-Verlag, 1993, pp. 3-14.
New Techniques for Efficient Verification with Implicitly Conjoined BDDs. Alan J. Hu, Gary York, and David L. Dill 31st Design Automation Conference, 1994
All of the above work has been updated and collected into Alan Hu's PhD thesis:
"Efficient Techniques for Formal Verification Using Binary Decision Diagrams," Alan John Hu, Ph.D. Thesis, Stanford University, December 1995.