A fundamental part of the research in computability, and linguistic formalisms, in particular, has involved the expressiveness of syntactic variants. This includes questions such as whether a given fragment of a logic is as hard for validity as the full language, or whether a given grammar can generate a certain set. Well-known results include the fact that it is not possible to provide a computable transforma-tion, or encoding, of arbitrary formulae into monadic ones that preserves valid-ity and that the set anbn cannot be generated by any regular grammar. Standard taxonomies include the Chomsky Hierarchy of formal languages and the logic classification of prenex normal forms .
Unfortunately, the subject of expressiveness in the π-calculus, and process calculi at large, is not a well-established discipline, or even a stable craft. Several guiding principles and cogent classification criteria have been put forth in several works such as [69, 43, 64, 92, 27, 45, 53, 16, 72, 91]. Hitherto, however, we do not have a general agreement as to what are the properties that a taxonomy of process calculi must consider in the way we have for the linguistic formalisms of computability where the notion of language (generation) can be taken as the canonical measure for expressiveness. This is perhaps due to the great diversity of observations and properties often used to reason about concurrent behaviour (e.g., divergence, convergence, failures, traces, barbs, must testing, bisimilarity, etc). It may be the case that rather than being absolute, a taxonomy of concurrent calculi ought to be parametric on the observations we wish to make of processes.
After all concurrency is a field with a myriad of aspects for which we may require different terms of discussion and analysis.
Nevertheless, expressiveness studies may offer crucial insights about the lim-itations, redundancies and capabilities of a family of process calculi. Most works on the expressiveness of the π-calculus consider questions such as whether a given variant can express certain behaviours, whether a given variant is as expressive as another one w.r.t. certain equivalence, or whether a given fragment is as hard for certain property as the full language.
For example, there are certain context-free sets that cannot be represented in a restriction-free variant of the zero-adic π-calculus . (By n-adic we refer to the maximal arity of the vectors of names that can be transmitted upon synchroniza-tion.) We also know that every polyadic π term can be encoded into a monadic π term preserving bisimilarity (a standard equivalence in concurrency theory)  and that under certain reasonable requirements one cannot encode every monadic
π -calculus term into a zero-adic one . These expressiveness questions are of great interest as a variant may simplify the presentation of the calculus, be tailored to specific applications, or be used to single out important aspects of the calculus.
This dissertation is devoted to the study of the expressiveness of several variants of the π-calculus. The main variants under consideration are the zero-adic π-calculus, also known as CCS! [21, 22], and the asynchronous monadic π-calculus Aπ [15, 47]. We shall mainly focus on behaviours arising from the restriction and replication operators as well as from their interplay. The study will be conducted by imposing natural constraints on these operators and their interaction, and then showing their impact on the expressiveness of the constrained variant.
Our study is inspired in part by work and elements from linguistic formalisms such as logic and formal grammars. This is evidenced by the kind of results that we shall discuss in detail later on in this introduction. Namely, we shall give a classification of zero-adic π-calculi following the Chomsky Hierarchy of formal grammars as well as a classification of zero-adic π-calculus processes that resembles the classification of prenex first-order formulae w.r.t. constraints on quantifiers . We shall also give a classification of semi-linear (semi-persistent)
π -calculus which is inspired by the notion of resource in Girard’s linear logic . Our work builds on the seminal paper by Busi, Gabbrielli and Zavattaro on
π Chapter 3: Computational Expressiveness of CCS!
CCS!  as well as the work by Palamidessi, Saraswat, Victor and Valencia on the asynchronous π-calculus . In fact, this dissertation has been structured in two main parts reflecting the influence of these works. These parts are motivated and discussed next.
Part I: The Expressiveness of CCS!
In  Busi et al demostrated that CCS! is Turing powerful by encoding Random Access Machines (RAMs). The key property of the encoding is that it preserves and reflects convergence (i.e., the existence of halting computations): Given a RAM M , the encoding of M in CCS! converges if and only if M converges.
We wish to outline two observations we made about the encoding given in  that are central to this part: (1) The mechanism used to force ”unfaithful” computational paths of the encoding to be infinite and (2) the mechanism used to generate an unbounded number of restricted names. Let us ellaborate on these two points:
The first observation is
that the CCS! encoding of RAMs uses a divergence mechanism to force the un-faithful computational paths to be infinite. By unfaithful path we mean, infor-mally, paths that do not correspond to those of the encoded machine. The CCS! encoding of a given RAM can, during evolution, move from a state that may ter-minate, i.e. a (weakly) terminating state, into one that cannot terminate, i.e., a (strongly) non-terminating state. Consequently, the encoding does not preserve (weak) termination during evolution. This allows us to ignore the unfaithful be-haviour as follows: Whenever the encoding takes a computational path that makes a wrong guess about a test for zero (i.e., it does not correspond to the test for zero of the encoded RAM) then that path is forced to be infinite. This infinite path is thus regarded as a non-halting computation and therefore ignored. All finite com-putations of the encoding, however, correspond to those halting computations of the encoded RAM. Hence, the encoding preserves and reflects convergence.
One may wonder if we can dispense with the above mechanism and still be able to provide an encoding of RAMs that preserves and reflects convergence.
Busi et al has answered negatively this question in . Another legitimate ques-tion is thus:
Q1: What less expressive computational models can be encoded into CCS! without using this divergence mechanism, i.e. with weak-termination preserving processes ?
We shall partially answer this question in Chapter 3. We study the family of weak-termination preserving processes by considering models of computabil-ity strictly less expressive that RAM’s. In particular we shall study the expres-siveness of CCS! w.r.t. the existence of termination-preserving encodings of gra-mmars of Types 1 (Context Sensitive grammars), 2 (Context Free grammars) and 3 (Regular grammars) in the Chomsky Hierarchy whose expressiveness corresponds to (non-deterministic) Linear-bounded, Pushdown and Finite-State Automata, re-spectively. We shall show that they can encode any Type 3 grammars but not Type 2 grammars. We also conjecture that the set of all finite sequences performed by a weak-termination preserving process corresponds to Type 1 grammars.
Chapter 4: The Expressiveness of Restriction and Replication. The second observation is that the CCS! encoding of RAMs  uses restriction operators un-der the scope of replication as for example in !(νx)P . Indeed, to the best of our knowledge, all the encodings of Turing-powerful formalisms in π-calculus vari-ants such as CCS, the monadic π-calculus, the asynchronous π-calculus involve restrictions under the scope of replication or under the scope recursive expressions as for example in µX.(νx)(P |X).
As mentioned earlier in this introduction, a restriction under replication repre-sents (the potential generation of) unboundedly many local processes in parallel: !(νx)P represents infinitely many restricted declarations of x. This mechanism seems crucial for the encoding of Turing-powerful formalisms mentioned above. We then find it natural to ask:
Q2: Is the occurrence of restriction under the scope of replication necessary for the Turing-completeness of some π-based calculi ?
At this point it is perhaps worth mentioning that a somewhat similar expressiveness situation, from which we partially took inspiration, arises in logic. We can think of a formula ∀y∃xF (y, x) as describing potentially infinitely many ex-istential declarations of x, one for each each possible y. There is a complete study of decidable classes (w.r.t. satisfiability) of formulae involving the occurrence of existential quantifiers under the scope of universal quantification. For exam-ple, Skolem showed that the class of formulae of the form ∀y1…∀yn∃z1…∃zmF, where F is quantifier-free formula, is undecidable while from Godel¨ we know that its subclass ∀y1∀y2∃z1…∃zmF is decidable .
Perhaps a closer analogy arises in temporal logic : The formula ✷∃xF (x), whose intended meaning is ”always there exists x such that F (x)” can be viewed as describing an unbounded number of existential declarations of x over time. This scoping of the ”always” modality over existential quantification is central to the proof that monadic temporal logic is undecidable w.r.t. validity and hence cannot be encoded in propositional temporal logic .
In Chapter 4 we study the expressiveness of restriction and its interplay with replication. We consider two syntactic variations of CCS! that do not allow the use of an unbounded number of restrictions: CCS−!!ν is the fragment of CCS! not allowing restrictions under the scope of a replication. CCS−!ν is the restriction-free fragment of CCS!.
We shall show that having restriction under replication in CCS! is necessary for obtaining Turing expressiveness in the sense of Busi et al  hence providing an answer to question Q2 above. We do this by showing that there is no encoding of RAMs into CCS−!!ν which preserves and reflects convergence.
Furthermore, we shall also prove that up to failures equivalence, an standard equivalence in concurrency theory, there is no encoding from CCS! into CCS−!!ν nor from CCS−!!ν into CCS−!ν . In other words, up to failures equivalence, we can-not encode all processes that may generate an unbounded number of restrictions with processes that can only generate a bounded number, nor all processes that may generate bounded number of restrictions with restriction-free processes.
In the light of the above-mentioned results, one may now wonder whether some other natural process construction can replace the use in CCS! of unbound-edly many restrictions for achieving Turing expressiveness. We shall answer positively this question by considering a third variant CCS−!+!νpr which extends CCS−!!ν with Phillips’ priority guards . This bears witness to the expressive power of this guarding construction.
Part II: The Asynchronous π-calculus
In  the authors presented an expressiveness study of linearity and persistence of processes in the asynchronous version of the π-calculus, henceforth Aπ. Lin-earity (and persistence) is understood in a similar sense of Girard’s linear logic; the ability (incapability) of consuming a resource. The replication operator is cen-tral in  and plays a role similar to the ”bang” operator from linear logic, also denoted as !.
Chapter 5: Linearity and Persistence The study in  is conducted in the asynchronous π-calculus (Aπ), which naturally captures the notion of linearity and persistence also present in other calculi.
Let us for example consider π-calculus system xz¯ | x(y).P | x(y).Q
This system represents a linear message with a datum z, tagged with x, that can be consumed by either (linear) receiver x(y).P or x(y).Q. Persistent messages (and receivers) can simply be specified using the replication operator which, as previ-ously mentioned, creates an unbounded number of copies of a given process. One can then consider the existence of encodings from Aπ into three sub-languages of it, each capturing one source of persistence: the persistent-input calculus (PIAπ), defined as Aπ where inputs are replicated; the persistent-output calculus (POAπ), defined dually, i.e. outputs rather than inputs are replicated; the persistent calculus (PAπ), defined as Aπ but with all inputs and outputs replicated.
The main result in  basically states that we need one source of linearity, i.e. either on inputs (PIAπ) or outputs (POAπ) to encode the behavior of arbitrary Aπ processes via weak barbed congruence.
The notion of linearity (persistency) is present is several concurrency frame-works. Persistence of messages is present , e.g., in Concurrent Constraint Programming (CCP) , Winskel’s SPL  and the Spi Calculus variants in [35, 5]. In all these formalisms messages cannot be consumed. In the π-calculus persistent receivers are used, for instance, to model functions, objects, higher-order commu-nications, or procedure definitions. Furthermore, persistence of both messages and receivers arise in the context of CCP with universally-quantified persistent ask operations  and in the context of calculi for security, persistent receivers can be used to specify protocols where principals are willing to run an unbounded number of times (and persistent messages to model the fact that every message can be remembered by the spy ).
Now, the previously mentioned positive result in  may give insights in the context of the expressiveness of the above frameworks. The main drawback of the work  is, however, that the notion of correctness for the encodings is based on weak barbed bisimulation (congruence), which is not sensitive to divergence. In particular, the encoding provided in  from Aπ into PIAπ is weak barbed congruent preserving but not divergence preserving. Although in some situations divergence may be ignored, in general it is an important issue to consider in the correctness of encodings [26, 44, 43, 27, 24, 69].
As a matter of fact the informal claims of extra expressivity of Linear CCP over CCP in [11, 34] are based on discrimination introduced by divergence that is clearly ignored by the standard notion of weak bisimulation. Furthermore, in  the author suggests as future work to extend SPL, which uses only persistent messages and replication, with recursive definitions to be able to program and model recursive protocols such as those in [4, 73]. Nevertheless, one can give an encoding of recursion in SPL from an easy adaptation of the composition between the Aπ encoding of recursion  (where recursive calls are translated into linear Aπ outputs and recursive definitions into persistent inputs) and the encoding of Aπ into POAπ in . The resulting encoding is correct up to weak bisimilarity. The encoding of Aπ into POAπ, however, introduces divergence and hence the composite encoding does not seem to invalidate the justification for extending SPL with recursive definitions.
The above works suggest that the expressiveness study of persistence of  is relevant but incomplete since divergence is ignored. We therefore ask ourselves:
Q3: Can the above-mentioned linearity be captured in (semi) persistent calculi without introducing divergence ?
In the Chapter 5 we shall study the existence of encodings from Aπ into the persistent sub-languages mentioned above using testing semantics  which takes divergence into account. We shall provide a uniform and general negative answer to question Q3 by stating that, under some reasonable conditions, Aπ can-not be encoded into any of the above (semi) persistent calculi while preserving the must testing semantics. The general conditions involve compositionality on the encoding of constructors such as parallel composition, prefix, and replication. The main result contrasts and completes the ones in . It also supports the informal claims of extra expressivity mentioned above.
We shall also state other more specialized impossibility results for must pre-serving encodings from Aπ into the semi-persistent calculi, focusing on specific properties of each target calculus. This helps clarifying some previous assump-tions on the interplay between syntax and semantics in encodings of process cal-culi. We believe that, since the study is conducted in Aπ with well-established notions of equivalence, our results can be easily adapted to other asynchronous frameworks such as CCP languages and the above-mentioned calculi for security.
Contributions and Organization
In summary this dissertation extends and strengthens the works [22, 70] by sin-gling out key aspects of these works and then filling their gaps in the context of the expressiveness in concurrency theory. Among the other previously mentioned results, we shall show that without the divergence mechanism used in  for encoding Minsky machines, CCS! can capture regular but not context-free be-haviours. We shall also show that the scoping of replication (or recursion) over restriction in the CCS! encoding in  (and in other π-based encodings of Turing-powerful models) is necessary to achieve Turing completeness. We shall show that under some natural conditions, the linearity of the asynchronous π-calculus  cannot be encoded with semi-persistent asychronous π-calculi.
All in all, we shall show how the restriction operator, replication and their interplay play a fundamental and complementary role in the computational expressiveness of some π-based calculi from the literature.
This dissertation is organized as follows: We begin with two introductory chapters followed by the two parts previously discussed in the Introduction. We conclude with some discussion about future work and an index table with the most relevant notions and notations.
The first chapter motivates and discusses our work. In the second chapter we provide some preliminary notions and prove some general properties that will be used in the forthcoming chapters.
Each chapter in Part I and Part II begins with an introduction explaining the motivation, lines of developments and the contributions, and it concludes with a short summary and a discussion about related work.
Chapters 3-4 are included in Part I and were described earlier in the Intro-duction. The third chapter provides the first classification based on the Chomsky Hierarchy. The fourth chapter provides the classification based on the scoping of replication over restriction.
Chapter 5 is included in Part II and was also previously described in the In-troduction. This chapter provides a classification of linearity vs persistence in the asychronous π-calculus.
Table of contents :
2.1 The π-calculus
2.2 The asynchronous π-calculus: Aπ
2.3 The Calculus of Communicating Systems
2.3.1 Finite CCS
2.3.2 Replication: CCS!
2.3.3 Parametric Definitions: CCS and CCSp
2.4 Notions and equivalences
2.4.2 Language and failures equivalences
2.4.3 Testing semantics
2.5 Petri Nets
2.6 Random Access Machines RAMs
3 CCS! in the Chomsky Hierarchy
3.2 The Role of Strong Non-Termination
3.3 CCS! without choice
3.4 Undecidability results for CCS−ω
3.5 CCS! and the Chomsky Hierarchy
3.5.1 Encoding Regular Languages
3.5.2 Impossibility Result: Context Free Languages
3.5.3 Inside Context Sensitive Languages (CSL)
3.6 Summary and Related Work
4 On the Expressive Power of Restriction and Priorities in CCS with replication
4.2 Decidability of Convergence for CCS−!ν
4.2.1 Convergence-invariant properties in fragments of CCS−!ν
4.2.2 The Reduction to Petri Nets
4.3 Decidability of Language Equivalence for CCS−ν
4.4 Impossibility results for failure-preserving encodings
4.5 Encoding from CCS−μν into CCS−ν
4.5.1 The Encoding
4.6 Expressiveness of Priorities
4.6.1 CCS! with priorities
4.6.2 Encoding RAMs with priorities
4.7 Summary and Related Work
5 Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus
5.2 Semi-persistence in Aπ
5.2.1 The (semi-)persistent calculi
5.3 Reasonable Properties of Encodings
5.3.1 Contexts, Compositionality and Homomorphism
5.3.2 Preservation of infinite behaviour
5.4 Previous encodings of Aπ into semi-persistent subcalculi
5.5 Uniform impossibility results for the semi-persistent calculi
5.5.1 Non-existence of encodings homomorphic wrt !
5.5.2 Non-existence of encodings preserving infinite behaviour
5.6 Specialized impossibility result for PAπ
5.7 Decidability results for POAπ
5.7.1 Computing Successors
5.7.2 Decidability of convergence and divergence
5.8 Summary and related work