Michele Boreale1, Rocco De Nicola2, Rosario
Pugliese2,
1 Dipartimento di Scienze dell'Informazione, Universita' di Roma ``La Sapienza''
2 Dipartimento di Sistemi e Informatica, Universita' di Firenze
Abstract
A general approach for defining behavioural preorders over process terms
as the maximal pre-congruences induced by basic observables is examined.
Three different observables, that provide information about the initial
communication capabilities of processes and about the possibility that
processes get engaged in divergent computations, will be considered.
We show that the pre-congruences induced by our basic observables
coincide with intuitive and/or widely studied behavioural preorders.
In particular, we retrieve in our setting the must preorder of
De Nicola and Hennessy and the fair/should preorder introduced by
Cleaveland and Natarajan and by Brinksma, Rensink and Vogler.
A new form of testing preorder, which we call safe-must, also emerges.
The alternative characterizations we offer shed light on the differences
between these preorders, and on the role played in their definition by
tests for divergence.