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

共 50 条

[1] GENERATING BDDS FOR SYMBOLIC MODEL CHECKING IN CCS
ENDERS, R
FILKORN, T
TAUBNER, D
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 575 : 203 - 213
[2] Symbolic Model Checking without BDDs
Biere, A
Cimatti, A
Clarke, E
Zhu, YS
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1999, 1579 : 193 - 207
[3] BDDs vs. zero-suppressed BDDs: for CTL symbolic model checking of Petri nets
Yoneda, T
Hatori, H
Takahara, A
Minato, S
[J]. FORMAL METHODS IN COMPUTER-AIDED DESIGN, 1996, 1166 : 435 - 449
[4] Abstract BDDs: A technique for using abstraction in model checking
Clarke, E
Jha, S
Lu, Y
Wang, D
[J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 : 172 - 186
[5] Symbolic model checking
McMillan, KL
[J]. VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 117 - 137
[6] A comparison of BDDs, BMC, and sequential SAT for model checking
Parthasarathy, G
Iyer, MK
Cheng, KT
Wang, LC
[J]. EIGHTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2003, : 157 - 162
[7] Checking satisfiability of a conjunction of BDDs
Damiano, R
Kukula, J
[J]. 40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 818 - 823
[8] Can BDDs compete with SAT solvers on bounded model checking?
Cabodi, G
Camurati, P
Quer, S
[J]. 39TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2002, 2002, : 117 - 122
[9] Interpolants and symbolic model checking
McMillan, K. L.
[J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2007, 4349 : 89 - 90
[10] On partitioning and symbolic model checking
Iyer, S
Sahoo, D
Emerson, EA
Jain, J
[J]. FM 2005: FORMAL METHODS, PROCEEDINGS, 2005, 3582 : 497 - 511

← 1 2 3 4 5 →