GENERATING BDDS FOR SYMBOLIC MODEL CHECKING IN CCS

被引：18

作者：

ENDERS, R ^{[1
]}

FILKORN, T ^{[1
]}

TAUBNER, D ^{[1
]}

机构：

[1] SD&M GMBH, W-8000 MUNICH 83, GERMANY

来源：

DISTRIBUTED COMPUTING | 1993年 / 6卷 / 03期

关键词：

BINARY DECISION DIAGRAM (BDD); PROCESS ALGEBRA; CCS; TRANSITION SYSTEM; (SYMBOLIC) MODEL CHECKING; BISIMILARITY;

D O I：

10.1007/BF02242704

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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 mu-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.

引用

页码：155 / 164

页数：10

共 13 条

[1] BRYANT RE, 1986, IEEE T COMPUT, V35, P677, DOI 10.1109/TC.1986.1676819
[2] BURCH JR, 1990, 5TH P IEEE S LOG COM, P428
[3] CLEAVELAND R, 1990, LECT NOTES COMPUT SC, V407, P24
[4] DESIMONE R, 1989, INRIA111 RAPP TECHN
[5] Emerson E. A., 1986, Proceedings of the Symposium on Logic in Computer Science (Cat. No.86CH2321-8), P267
[6] ESTENFELD K, 1991, VIS 91 DARMSTADT INF, V271, P208
[7] FILKORN T, 1988, THESIS TU MUNCHEN
[8] FISCHER S, 1992, P CAV92 WORKSHOP COM
[9] GROOTE JF, 1990, LECT NOTES COMPUT SC, V443
[10] Milner R., 1989, Communication and concurrency

← 1 2 →