Michele Boreale, Rocco De Nicola, Rosario Pugliese
Dipartimento di Sistemi e Informatica, Università di Firenze
Abstract
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.