A general approach for defining behavioral preorders over process terms as the maximal precongruences 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 precongruences induced by our basic observables coincide with intuitive and/or widely studied behavioral 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 pre-orders and on the role played in their definition by tests for divergence.
Basic Observables for Processes / M. BOREALE; R. DE NICOLA; R. PUGLIESE. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - STAMPA. - 149(1):(1999), pp. 77-98. [10.1006/inco.1998.2755]
Basic Observables for Processes
BOREALE, MICHELE;PUGLIESE, ROSARIO
1999
Abstract
A general approach for defining behavioral preorders over process terms as the maximal precongruences 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 precongruences induced by our basic observables coincide with intuitive and/or widely studied behavioral 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 pre-orders and on the role played in their definition by tests for divergence.File | Dimensione | Formato | |
---|---|---|---|
99IC-Basic Observables for Processes.pdf
Accesso chiuso
Tipologia:
Versione finale referata (Postprint, Accepted manuscript)
Licenza:
Tutti i diritti riservati
Dimensione
387.23 kB
Formato
Adobe PDF
|
387.23 kB | Adobe PDF | Richiedi una copia |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.