We present a unified approach to evaluate the relative expressive power of process calculi. In particular, we identify a small set of criteria (that have already been somehow presented in the literature) that an encoding should satisfy to be considered a valid means for language comparison. We argue that the combination of such criteria is a valid proposal by noting that: (i) several well-known encodings appeared in the literature satisfy them; (ii) this notion is not trivial, because some known encodings do not satisfy all the criteria we have proposed: (iii) several well-known separation results can be formulated in terms of our criteria: and (iv) some widely believed (but never formally proved) separation results can be proved by using the criteria we propose. Moreover, the criteria defined induce general proof-techniques for separation results that can be easily instantiated to cover known case-studies. (C) 2010 Elsevier Inc. All rights reserved.
Towards a unified approach to encodability and separation results for process calculi / Gorla, Daniele. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - STAMPA. - 208:9(2010), pp. 1031-1053. [10.1016/j.ic.2010.05.002]
Towards a unified approach to encodability and separation results for process calculi
GORLA, DANIELE
2010
Abstract
We present a unified approach to evaluate the relative expressive power of process calculi. In particular, we identify a small set of criteria (that have already been somehow presented in the literature) that an encoding should satisfy to be considered a valid means for language comparison. We argue that the combination of such criteria is a valid proposal by noting that: (i) several well-known encodings appeared in the literature satisfy them; (ii) this notion is not trivial, because some known encodings do not satisfy all the criteria we have proposed: (iii) several well-known separation results can be formulated in terms of our criteria: and (iv) some widely believed (but never formally proved) separation results can be proved by using the criteria we propose. Moreover, the criteria defined induce general proof-techniques for separation results that can be easily instantiated to cover known case-studies. (C) 2010 Elsevier Inc. All rights reserved.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.