Trace and Testing Equivalence on Asynchronous Processes

 Michele Boreale, Rocco De Nicola, Rosario Pugliese
Dipartimento di Sistemi e Informatica, Università di Firenze

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 for it finitary and fully abstract trace-based characterizations, 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.