Basic Observables for Processes

We propose a general approach for defining behavioural preorders over process terms as the maximal pre–congruences induced by basic observables. We will consider three of these, that provide information about the initial communication capabilities of processes and about the possibility that processes get engaged in divergent computations. 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 rˆole played in their definition by tests for divergence.

• Type: Conference
• Year: 1997
• Where: ICALP
• Authors: Michele Boreale, Rocco De Nicola, Rosario Pugliese
• Keywords: Basic Observables, Behavioural Preorders, ICALP 1997, Initial Communication Capabilities, Programming Languages