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 条
[1]   A calculus for cryptographic protocols: The spi calculus [J].
Abadi, M ;
Gordon, AD .
INFORMATION AND COMPUTATION, 1999, 148 (01) :1-70
[2]  
Agha G., 1997, J FUNCTIONAL PROGRAM, V7, P1, DOI DOI 10.1017/S095679689700261X
[3]   On bisimulations for the asynchronous π-calculus [J].
Amadio, RM ;
Castellani, I ;
Sangiorgi, D .
THEORETICAL COMPUTER SCIENCE, 1998, 195 (02) :291-324
[4]  
[Anonymous], THESIS U TWENTE
[5]   PROCESS ALGEBRA FOR SYNCHRONOUS COMMUNICATION [J].
BERGSTRA, JA ;
KLOP, JW .
INFORMATION AND CONTROL, 1984, 60 (1-3) :109-137
[6]   TESTING EQUIVALENCE FOR MOBILE PROCESSES [J].
BOREALE, M ;
DENICOLA, R .
INFORMATION AND COMPUTATION, 1995, 120 (02) :279-303
[7]  
Boreale M, 1998, LECT NOTES COMPUT SC, V1378, P95, DOI 10.1007/BFb0053544
[8]  
Boreale M, 1999, LECT NOTES COMPUT SC, V1578, P165
[9]  
BOREALE M, 1998, P PROCOMET 97
[10]  
BOUDOL G, 1992, 1702 INRIA