Submitted for publication.
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.
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.