Trace and testing equivalence on asynchronous processes

被引:39
作者
Boreale, M [1 ]
De Nicola, R [1 ]
Pugliese, R [1 ]
机构
[1] Univ Florence, Dipartimento Sci & Informat, I-50134 Florence, Italy
关键词
asynchronous communications; process algebras; semantics;
D O I
10.1006/inco.2001.3080
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We study trace and may-testing equivalences in the asynchronous versions of CCS and pi-calculus. We start from the operational definition of the may-testing preorder and provide finitary and fully abstract trace-based characterizations for it, along with a complete in-equational proof system. We also touch upon two variants of this theory by first considering a more demanding equivalence notion (must-testing) and then a richer version of asynchronous CCS. The results throw light on the difference between synchronous and asynchronous communication and on the weaker testing power of asynchronous observations. (C) 2002 Elsevier Science (USA).
引用
收藏
页码:139 / 164
页数:26
相关论文
共 36 条
[21]  
HANSEN M, 1995, P TIBL S LANG LOG CO
[22]  
Hennessy M., 1988, An algebraic theory of processes
[23]  
HONDA K, 1992, LECT NOTES COMPUT SC, V612, P21
[24]  
HONDA K, 1991, LECT NOTES COMPUT SC, V512, P133
[25]  
JIFENG H, 1990, P IFIP WORK C PROGR, P446
[26]  
Jonsson B., 1985, P 4 ACM S PRINC DIST, P49
[27]   THE TEMPORAL LOGIC OF ACTIONS [J].
LAMPORT, L .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (03) :872-923
[28]   A PROOF OF THE KAHN PRINCIPLE FOR INPUT OUTPUT AUTOMATA [J].
LYNCH, NA ;
STARK, EW .
INFORMATION AND COMPUTATION, 1989, 82 (01) :81-92
[29]  
Milner R., 1989, Communication and concurrency
[30]  
MILNER R, 1992, INFORM COMPUT, V100, P1, DOI [10.1016/0890-5401(92)90008-4, 10.1016/0890-5401(92)90009-5]