CCS EXPRESSIONS, FINITE STATE PROCESSES, AND 3 PROBLEMS OF EQUIVALENCE

被引:248
作者
KANELLAKIS, PC [1 ]
SMOLKA, SA [1 ]
机构
[1] SUNY STONY BROOK,DEPT COMP SCI,STONY BROOK,NY 11794
基金
美国国家科学基金会;
关键词
D O I
10.1016/0890-5401(90)90025-D
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We examine the computational complexity of testing finite state processes for equivalence in Milner's Calculus of Communicating Systems (CCS). The equivalence problems in CCS are presented as refinements of the familiar problem of testing whether two nondeterministic finite automata (NFA) are equivalent, i.e., accept the same language. Three notions of equivalence proposed for CCS are investigated, namely, observational equivalence, strong observational equivalence, and failure equivalence. We show that observational equivalence can be tested in polynomial time. As defined in CCS, observational equivalence is the limit of a sequence of successively finer equivalence relations, ≈k, where ≈1 is nondeterministic finite automaton equivalence. We prove that, for each fixed k, deciding ≈k is PSPACE-complete. We show that strong observational equivalence can be decided in polynomial time by reducing it to generalized partitioning, a new combinatorial problem of independent interest. Finally, we demonstrate that testing for failure equivalence is PSPACE-complete, even for a very restricted type of process. © 1990.
引用
收藏
页码:43 / 68
页数:26
相关论文
共 24 条
[1]  
Aho A. V., 1974, DESIGN ANAL COMPUTER
[2]   BISIMULATION OF AUTOMATA [J].
BENSON, DB ;
BENSHACHAR, O .
INFORMATION AND COMPUTATION, 1988, 79 (01) :60-83
[3]  
BERGSTRA JA, 1987, CSR8725 CWI COMP SCI
[4]  
BERGSTRA JA, 1986, CWI MONOGRAPHS, V1, P89
[5]   A THEORY OF COMMUNICATING SEQUENTIAL PROCESSES [J].
BROOKES, SD ;
HOARE, CAR ;
ROSCOE, AW .
JOURNAL OF THE ACM, 1984, 31 (03) :560-599
[6]  
BROOKES SD, 1983, LECT NOTES COMPUT SC, V154, P83
[7]  
BROOKES SD, 1983, LECT NOTES COMPUT SC, V154, P97
[8]  
CHANDRA AK, 1982, COMMUNICATION
[9]   TESTING EQUIVALENCES FOR PROCESSES [J].
DENICOLA, R ;
HENNESSY, MCB .
THEORETICAL COMPUTER SCIENCE, 1984, 34 (1-2) :83-133
[10]   ALGEBRAIC LAWS FOR NONDETERMINISM AND CONCURRENCY [J].
HENNESSY, M ;
MILNER, R .
JOURNAL OF THE ACM, 1985, 32 (01) :137-161