AN EFFICIENT FULLY SYMBOLIC BISIMULATION ALGORITHM FOR NON-DETERMINISTIC SYSTEMS

被引：4

作者：

Mumme, Malcolm ^{[1
]}

Ciardo, Gianfranco ^{[1
]}

机构：

[1] Univ Calif Riverside, Dept Comp Sci & Engn, Riverside, CA 92521 USA

来源：

INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE | 2013年 / 24卷 / 02期

基金：

美国国家科学基金会;

关键词：

Bisimulation; symbolic methods; algorithms; decision diagrams; saturation; locality; verification; GENERATION;

D O I：

10.1142/S012905411340011X

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The definition of bisimulation suggests a partition-refinement step, which we show to be suitable for a saturation-based implementation. We compare our fully symbolic saturation-based implementation with the fastest extant bisimulation algorithms over a set of benchmarks, and conclude that it appears to be the fastest algorithm capable of computing the largest bisimulation over very large quotient spaces.

引用

页码：263 / 282

页数：20

共 17 条

[1]

Aczel P., 1988, Non-well-founded sets

[2]

Bouali A., 1992, LECT NOTES COMPUTER, V663, P96, DOI DOI 10.1007/3-540-56496-9_9

[3]

Chung MY, 2006, LECT NOTES COMPUT SC, V4218, P51

[4]

Ciardo G, 2002, LECT NOTES COMPUT SC, V2517, P256

[5]

Ciardo G., SMART STOCHASTIC MOD

[6] AN O(N LOG N) UNIDIRECTIONAL DISTRIBUTED ALGORITHM FOR EXTREMA FINDING IN A CIRCLE [J].

DOLEV, D ;

KLAWE, M ;

RODEH, M .

JOURNAL OF ALGORITHMS, 1982, 3 (03) :245-260

[7] An efficient algorithm for computing bisimulation equivalence [J].

Dovier, A ;

Piazza, C ;

Policriti, A .

THEORETICAL COMPUTER SCIENCE, 2004, 311 (1-3) :221-256

[8]

Graf S., 1996, Formal Aspects of Computing, V8, P607, DOI 10.1007/BF01211911

[9]

Milner R., 1989, Communication and concurrency

[10]

MUMME M, 2011, P 5 INT WORKSH REACH, V6945, P218

← 1 2 →