Michele Boreale¹, Rocco De Nicola², Rosario Pugliese²,
¹ Dipartimento di Scienze dell'Informazione, Universita' di Roma ``La Sapienza''
² Dipartimento di Sistemi e Informatica, Universita' di Firenze

Abstract
Asynchronous communication mechanisms are usually at the basis of real distributed systems and protocols.For these systems, asynchronous may-based testing seems to be exactly what is needed to capture safety and certain security properties. We study may testing equivalence focusing on the asynchronous versions of CCS and pi-calculus. We start from an operational testing preorder and provide finitary and fully abstract trace-based models for it, together with complete inequational axiomatizations. The results throw light on the differences between synchronous and asynchronous systems and on the weaker testing power of asynchronous observations. We propose a general approach to define behavioural preorders over process terms by considering the pre-congruences induced by three basic observables. These observables provide information about the initial communication capabilities of processes and about their possibility of engaging in an infinite internal chattering. We show that some of the observables-based pre-congruences do correspond to behavioral preorders long studied in the literature. The coincidence proofs shed light on the differences between the must preorder of De Nicola and Hennessy and the fair/should preorder of Cleaveland and Natarajan and of Brinksma, Rensink and Vogler, and on the role played in their definition by tests for internal chattering.