Project topics and materials
Get Complete Project Material File(s) Now! »
Expressiveness
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 [14].
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 [28]. (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) [83] and that under certain reasonable requirements one cannot encode every monadic
π -calculus term into a zero-adic one [69]. 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 [14]. 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 [39]. Our work builds on the seminal paper by Busi, Gabbrielli and Zavattaro on
π Chapter 3: Computational Expressiveness of CCS!
4 CHAPTER 1. INTRODUCTION
CCS! [22] as well as the work by Palamidessi, Saraswat, Victor and Valencia on the asynchronous π-calculus [70]. In fact, this dissertation has been structured in two main parts reflecting the influence of these works. These parts are motivated and discussed next.
The Expressiveness of CCS!
In [22] 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 [22] 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 [21]. 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 [22] 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 [14].
Perhaps a closer analogy arises in temporal logic [56]: 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 [68].
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 [22] 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 [76]. This bears witness to the expressive power of this guarding construction.
The Asynchronous π-calculus
In [70] 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 [70] and plays a role similar to the ”bang” operator from linear logic, also denoted as !.
Chapter 5: Linearity and Persistence The study in [70] 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 [70] 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) [84], Winskel’s SPL [31] 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 [67] 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 [12]).
Now, the previously mentioned positive result in [70] may give insights in the context of the expressiveness of the above frameworks. The main drawback of the work [70] 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 [70] 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 [30] 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 [83] (where recursive calls are translated into linear
Aπ outputs and recursive definitions into persistent inputs) and the encoding of Aπ into POAπ in [70]. 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.
Table of contents :
1 Introduction
2 Preliminaries
2.1 The π-calculus
2.1.1 Syntax
2.1.2 Semantics
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.1 Bisimilarity
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
3.1 Introduction
3.1.1 Contributions
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.1 Introduction
4.1.1 Contributions
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.1 Introduction
5.1.1 Contributions
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
6 Conclusions
