Generating BDDs for symbolic model checking in CCS Export

@article{citeulike:3504912, 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.}, address = {London, UK}, author = {Enders, Reinhard and Filkorn, Thomas and Taubner, Dirk}, citeulike-article-id = {3504912}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1063394}, citeulike-linkout-1 = {http://dx.doi.org/10.1007/BF02242704}, citeulike-linkout-2 = {http://www.springerlink.com/content/7j547280l3867087}, day = {16}, doi = {10.1007/BF02242704}, issn = {0178-2770}, journal = {Distributed Computing}, keywords = {ccs, concurrency, model-checking}, month = {April}, number = {3}, pages = {155--164}, posted-at = {2008-11-12 04:07:13}, priority = {2}, publisher = {Springer-Verlag}, title = {Generating BDDs for symbolic model checking in CCS}, url = {http://dx.doi.org/10.1007/BF02242704}, volume = {6}, year = {1993} }

TY - JOUR ID - citeulike:3504912 L3 - citeulike-article-id:3504912 N2 - 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. IS - 3 JF - Distributed Computing SN - 0178-2770 AD - London, UK EP - 164 TI - Generating BDDs for symbolic model checking in CCS PB - Springer-Verlag VL - 6 SP - 155 KW - ccs KW - concurrency KW - model-checking AU - Enders, Reinhard AU - Filkorn, Thomas AU - Taubner, Dirk PY - 1993/04/16/ UR - http://dx.doi.org/10.1007/BF02242704 ER -