Project topics and materials
Get Complete Project Material File(s) Now! »
Termination of Mobile Processes by Typability
A term terminates if all its reduction sequences are of finite length. As far as programming languages are concerned, termination means that computation in programs will eventually stop. In computer science termination has been extensively investigated in term rewriting systems [DM79, DH95] and -calculi [Gan80, Bou03] (where strong normalization is a synonym more commonly used). Termination has also been discussed in process calculi, notably the -calculus. Indeed, termination is interesting in concurrency. For instance, if we interrogate a process, we may want to know that an answer is eventually produced (termination alone does not guarantee this, but termination would be the main ingredient in a proof). Similarly, when we load an applet we would like to know that the applet will not run for ever on our machine, possibly absorbing all the computing resources (a “denial of service” attack). In general, if the lifetime of a process can be infinite, we may want to know that the process does not remain alive simply because of nonterminating internal activity, and that, therefore, the process will eventually accept interactions with the environment.
Languages of terminating processes are proposed in [YBH04] and [San05]. In both cases, the proofs of termination make use of logical relations, a well-known technique from functional languages. The languages of terminating processes so obtained are however rather “functional”, in that the structures allowed are similar to those derived when encoding functions as processes. In particular, the languages are very restrictive on nested inputs (that is, the possibility of having free inputs underneath other inputs), and recursive inputs (that is, replications !a(x).P in which the body P can recursively call the guard a of the replication). Such patterns are entirely forbidden in [YBH04]; nested inputs are allowed in [San05] but in a very restricted form. For example, the process a(x).!b.¯x.0 | ¯ac.0.
Outline of the Thesis
The material presented in Chapter 2 is meant to prepare the technical development in the rest of the thesis. We introduce some basic notions about process calculi, with CCS and the -calculus as our templates. We then focus on channel types; we review sorts, simple channel types and subtyping progressively.
In Chapter 3 we introduce a probabilistic process calculus which includes both nondeterministic and probabilistic choice, as well as recursion. We give its semantics in terms of Segala and Lynch’s probabilistic automata. We introduce two strong equivalences and two weak equivalences. We show some properties of the equivalences, using a probabilistic version of “bisimulation up to” proof techniques. For the strong equivalences we give complete axiomatisations for all expressions, while for the weak equivalences we achieve this result only for guarded expressions. We conjecture that in the general case of unguarded recursion the “natural” weak equivalences are undecidable. In the completeness proofs, our proof schemas are inspired by [Mil84, Mil89b, SS00], but the details are more involved due to the presence of both probabilistic and nondeterministic dimensions. Indeed, it turns out that, to give a complete axiomatisation of observational equivalence, the simple probabilistic extension of Milner’s three -laws [Mil89a] would not be sufficient, thus we need a new rule. At last, for recursion-free expressions we provide axiomatisations of all the four equivalences, whose completeness proofs are very simple.
In Chapter 4 we study the algebraic theory of a finite -calculus with capability types. Firstly we consider a sublanguage without parallelism. This small language already shows the major obstacles for axiomatisations. Following [HR04] we give the operational semantics of the language in terms of a typed labelled transition system, from which we define typed (late) bisimulation. Secondly we set up a complete proof system for closed terms. Then we present a complete axiom system for open terms. The schema of the completeness proof is similar to that for the untyped -calculus [PS95]. The details, however, are quite different, due to the rich subtyping relation of the type system. Thirdly we recall the typed bisimilarity proposed in [HR04], and provide a proof system
for closed terms, together with an indirect axiomatisation for all terms. Fourthly we show that the difference between late and early bisimilarity can be captured by one axiom. Lastly we admit parallel composition. Its effect on the axiomatisations is to add an expansion law to eliminate all occurrences of the operator.
From CCS to the -calculus
A significant limitation of CCS, as argued in [Mil99], is that it is not able to naturally specify communicating systems with dynamically changing connectivity. For example, let us consider the system composed of three components P,Q and R as displayed in Figure 2.1(1). Initially P and R are connected by the link a, while P and Q are connected by b. In the configuration of Figure 2.1(2), P and Q have evolved into P0 and Q0 respectively and the link to R has moved from P to Q. Since CCS gives us no way of creating new links among existing components, we are not able to specify the system in (1) as a CCS expression that can evolve into (2). However, this kind of evolution occurs often in many real systems. For instance, we may imagine R as a critical section that are accessed by P and Q successively. A natural way of dealing with link mobility like this is to give actions more structures so that links can be passed around in communicating systems. This is the method adopted by the -calculus.
Table of contents :
Abstract
Acknowledgements
Main Notations
R´esum´e en fran¸cais
1 Introduction
1.1 Background
1.2 Objectives
1.3 Axiomatisations for Probabilistic Processes
1.4 Axiomatisations for Typed Mobile Processes
1.5 Termination of Mobile Processes by Typability
1.6 Outline of the Thesis
2 Preliminaries
2.1 A Calculus of Communicating Systems
2.2 The -calculus
2.2.1 From CCS to the -calculus
2.2.2 The Untyped -calculus
2.2.3 Sorts and Sorting
2.2.4 A Simple Example
2.2.5 The Simply Typed -calculus
2.2.6 Subtyping
3 Axiomatisations for Probabilistic Processes
3.1 Probabilistic Distributions
3.2 A Probabilistic Process Calculus
3.3 Behavioural Equivalences
3.3.1 Equivalence of Distributions
3.3.2 Behavioural Equivalences
3.3.3 Probabilistic “Bisimulation up to” Techniques
3.3.4 Some Properties of Strong Bisimilarity
3.3.5 Some Properties of Observational Equivalence
3.4 Axiomatisations for All Expressions
3.4.1 Axiomatizing Strong Bisimilarity
3.4.2 Axiomatizing Strong Probabilistic Bisimilarity
3.5 Axiomatisations for Guarded Expressions
3.5.1 Axiomatizing Divergency-Sensitive Equivalence
3.5.2 Axiomatizing Observational Equivalence
3.6 Axiomatisations for Finite Expressions
3.7 Summary
4 Axiomatisations for Typed Mobile Processes
4.1 A Fragment of The Typed -calculus
4.1.1 Standard Operational Semantics
4.1.2 Typed Labelled Transition System
4.1.3 Typed Bisimilarity
4.2 Proof System for the Closed Terms
4.3 Axioms for Typed Bisimilarity
4.3.1 The Axiom System
4.3.2 Soundness and Completeness
4.4 Other Equivalences
4.4.1 Hennessy and Rathke’s Typed Bisimilarity
4.4.2 Early Bisimilarity
4.5 Adding Parallelism
4.6 Summary
5 Termination of Mobile Processes by Typability
5.1 Preliminary Notations
5.2 The Core System: the Simply Typed -calculus with Levels
5.3 Allowing Limited Forms of Recursive Inputs
5.3.1 The Type System
5.3.2 Example: Primitive Recursive Functions
5.4 Asynchronous Names
5.4.1 Proving Termination with Asynchronous Names
5.4.2 Example: the Protocol of Encoding Separate Choice
5.5 Partial Orders
5.5.1 The Type System
5.5.2 Example: Symbol Table
5.6 Summary
6 Conclusions and Future Word
A Proofs from Chapter 3
A.1 Proof of Lemma 3
A.2 Proof of Proposition 3
A.3 Proof of Lemma 3.
A.4 Proof of Lemma
B Proofs from Chapter 4
B.1 Some More Derived Rules
B.2 Proof of Theorem 4.
C Proofs from Chapter 5
C.1 Proofs from Section 5
C.2 Proofs from Section 5.
C.3 Extending T 0 with Polyadicity and Conditional
C.4 Proofs from Section 5.
C.5 Proofs from Section 5.
C.6 Levels in the Join-calculus
Bibliography
