On the Expressiveness of Linearity vs Persistence in the Asychronous Pi-Calculus

Catuscia Palamidessi, INRIA
Vijay Saraswat, IBM TJ Watson Research Center
Frank Valencia, CNRS
Bjorn Victor, Uppsala University
February 10, 2006

Submitted for publication.

Abstract

We present an expressiveness study of linearity and persistence of processes. We choose the π-calculus, one of the main representatives of process calculi, as a framework to conduct our study. We consider four fragments of the π-calculus. Each one singles out a natural source of linearity/persistence also present in other frameworks such as Concurrent Constraint Programming (CCP), Linear CCP, and several calculi for security. The study is presented by providing (or proving the non-existence of) encodings among the fragments, a processes-as-formulae interpretation and a reduction from Minsky machines.

The fragments are: (1) The (polyadic) asynchronous π-calculus Aπ, (2) persistent-input Aπ defined as Aπ with all inputs replicated, (3) persistent-output Aπ defined as Aπ with all outputs replicated, and (4) persistent Aπ defined as Aπ with all inputs and outputs replicated. We provide compositional fully-abstract encodings, homomorphic w.r.t the parallel operator, from (1) into (2) and (3) capturing the behaviour of source processes. In contrast, we show that it is impossible to provide such encodings from (1) into (4). Nevertheless we prove that (4) is Turing-powerful. We further show that barbed congruence is undecidable for the zero-adic version of (2), the monadic version of (3) and the bi-adic version of (4). In contrast, we also show that it is decidable for the zero-adic versions of (3) and (4).

Furthermore, we provide a compositional interpretation of the π processes in (4) as First-Order Logic (FOL) formulae. The interpretation translates restriction and input binders into existential and universal quantifiers respectively. We illustrate how the interpretation simulates name extrusion (mobility) in FOL. We use the interpretation to characterize the standard π-calculus notion of barbed observability (reachability) as FOL entailment. We apply this characterization and classic FOL results by Bernays, Schonfinkel and Godel to identify decidable classes (w.r.t. barbed reachability) of infinite-state processes exhibiting meaningful mobile behaviour.

pdf

Back to Main page