# 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