Generating BDDs for symbolic model checking in CCS

Abstract

Finite transition systems can easily be represented by binary decision diagrams (BDDs) through the characteristic function of the transition relation. Burch et al. have shown how model checking of a powerful version of the µ-calculus can be performed on such BDDs. In this paper we show how a BDD can be generated from elementary finite transition systems given as BDDs by applying the CCS operations of parallel composition, restriction, and relabelling. The resulting BDDs only grow linearly in the number of parallel components. This way bisimilarity checking can be performed for processes out of the reach of conventional process algebra tools.