The pi-calculus [61] is one the most influential formalisms for modelling and analyzing the behaviour of concurrent systems. This calculus provides a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. For example, the parallel composition term P | Q, which is built from the terms P and Q, represents the process that results from the parallel execution of the processes P and Q. Similarly, the restriction (v x)P represents a process P with local resource x. The replication !P can be thought of as abbreviating the parallel composition P | P | . . . of an unbounded number of P processes. As for other language-based formalisms (e.g., logic, formal grammars and the pi-calculus) a fundamental part of the research in process calculi involves the study of the expressiveness of fragments or variants of a given process calculus. In this dissertation we shall study the expressiveness of some variants of the pi-calculus focusing on the role of the terms used to represent local and infinite behaviour, namely restriction and replication. The first part of this dissertation is devoted to the expressiveness of the zero-adic variant of the (polyadic) pi-calculus, i.e., CCS with replication (CCS!) [21]. Busi et al [22] show that CCS! is Turing powerful [22]. The result is obtained by encoding Random Access Machines (RAMs) in CCS!. The encoding is said to be non-faithful because it may move from a state which can lead to termination into a divergent one which do not correspond to any configuration of the encoded RAM. I.e., the encoding is not termination preserving. In this dissertation we shall study the existence of faithful encodings into CCS! of models of computability strictly less expressive than Turing Machines. Namely, grammars of Types 1 (Context Sensitive Languages), 2 (Context Free Languages) and 3 (Regular Languages) in the Chomsky Hierarchy. We provide faithful encodings of Type 3 grammars. We show that it is impossible to provide a faithful encoding of Type 2 grammars and that termination-preserving CCS! processes can generate languages which are not Type 2. We finally conjecture that the languages generated by termination-preserving CCS! processes are Type 1 . We also observe that the encoding of RAMs [22] and several encoding of Turing-powerful formalisms in pi-calculus variants may generate an unbounded number of restrictions during the simulation of a given machine. This unboundedness arises from having restrictions under the scope of replication (or recursion) as in e.g., !(v x)P or μX.(v x)(P | X). This suggests that such an interplay between these operators is fundamental for Turing completeness. We shall also study the expressive power of restriction and its interplay with replication. We do this by considering several syntactic variants of CCS! which differ from each other in the use of restriction with respect to replication. We consider three syntactic variations of CCS! which do not allow the generation of unbounded number of restrictions: C2 is the fragment of CCS! not allowing restrictions under the scope of a replication, C3 is the restriction-free fragment of CCS!. The third variant is C4 which extends C2 with Phillips' priority guards [76]. We shall show that the use of an unboundedly many restrictions in CCS! is necessary for obtaining Turing expressiveness in the sense of Busi et al [22]. We do this by showing that there is no encoding of RAMs into C2 which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS! into C2 nor from C2 into C3. Thus up to failures equivalence, we cannot encode a process with an unbounded number of restrictions into one with a bounded number of restrictions, nor one with a bounded number of restrictions into a restriction-free process. As lemmata for the above results we prove that convergence is decidable for C2 and that language equivalence is decidable for C3 but undecidable for C2. As corollary it follows that convergence is decidable for restriction-free CCS. Finally, we show the expressive power of priorities by providing a faithful encoding of RAMs in C4 thus bearing witness to the expressive power of Phillips' priority guards [76]. The second part of this dissertation is devoted to expressiveness of the asynchronous monadic pi-calculus, A [15, 47]. In [70] the authors studied the expressivenessn of persistence in Api [15, 47] wrt weak barbed congruence. The study is incomplete because it ignores divergence. We shall present an expressiveness study of persistence in Api wrt De Nicola and Hennessy's testing scenario which is sensitive to divergence. Following [70],,we consider Api and three sub-languages of it, each capturing one source of persistence: the persistent-input Api-calculus (PIA), the persistent-output Api-calculus (POA) and the persistent Api-calculus (PA). In [70] the authors showed encodings from Api into the semi-persistent calculi (i.e., POA and PIA) correct wrt weak barbed congruence. We show that, under some general conditions related to compositionality of the encoding and preservation of the infinite behaviour, there cannot be an encoding from Api into a (semi)-persistent calculus preserving the must testing semantics. We also prove that convergence and divergence are decidable for POA (and PA). As a consequence there is no encoding preserving and reflecting divergence or convergence from Api into POA (and PA). This study fills a gap on the expressiveness study of persistence in A in [70].
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00430495 |
| Date | 27 November 2009 |
| Creators | Aranda, Jesus |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | English |
| Type | PhD thesis |
Page generated in 0.0024 seconds