Deng, Yuxin (2005) Axiomatisations and Types for Probabilistic and Mobile Processes. PhD thesis Informatique Temps Réel, Robotique et Automatique, ENSMP - CMA Centre de Mathématiques Appliquées, ENSMP.

Full text available as: - these-deng.pdf ( 1174 Kb )

Licence: Copyright

Alternative Locations: http://www.pps.jussieu.fr/~yuxin/thesis/main.pdf

Abstract

The focus of this thesis are the theoretical foundations for reasoning about algorithms and protocols for modern distributed systems. Two important features of models for these systems are probability and typed mobility: probabilities can be used to quantify unreliable or unpredictable behaviour and types can be used to guarantee secure behaviour in systems with a mobile structure. In this thesis we develop algebraic and type-based techniques for behavioural reasoning on probabilistic and mobile processes. In the first part of the thesis we study the algebraic theory of a process calculus which combines both nondeterministic and probabilistic behaviour in the style of Segala and Lynch's probabilistic automata. We consider various strong and weak behavioural equivalences, and we provide complete axiomatisations for finite-state processes, restricted to guarded recursion in the case of the weak equivalences. In the second part of the thesis we investigate the algebraic theory of the n-calculus under the effect of capability types, which are one of the most useful forms of types in mobile process calculi. Capability types allow one to distinguish between the capability to read from a channel, to write to a channel, and to both read and write. They also give rise to a natural and powerful subtyping relation. We consider two variants of typed bisimilarity, both in their late and in their early version. For both of them, we give complete axiomatisations on the closed finite terms. For one of the two variants, we provide a complete axiomatisation for the open finite terms. In the last part of the thesis we develop a type-based technique for verifying the termination property of some mobile processes. We provide four type systems to guarantee this property. The type systems are obtained by successive refinements of the types of the simply typed n-calculus. The termination proofs take advantage of techniques from term rewriting systems. These type systems can be used for reasoning about the terminating behaviour of some non-trivial examples: the encodings of primitive recursive functions, the protocol for encoding separate choice in terms of parallel composition, a symbol table implemented as a dynamic chain of cells. These results lay out the foundations for further study of more advanced models which may combine probabilities with types. They also highlight the robustness of the algebraic and typebased techniques for behavioural reasoning.

References

[AB01] Suzana Andova and J. C. M. Baeten. Abstraction in probabilistic process algebra. In Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 204-219. Springer, 2001.
[Aba99] Martin Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749-786, 1999.
[AéI02] Luca Aceto, Zolt´an ésik, and Anna Ingolfsdottir. Equational axioms for probabilistic bisimilarity (preliminary report). Technical Report RS-02-6, BRICS, 2002.
[And99] Suzana Andova. Process algebra with probabilistic choice. Technical Report CSR 99-12, Eindhoven University of Technology, 1999.
[Bar84] Henk Barendregt. The lambda Calculus: Its Syntax and Semantics. North-Holland, 1984.
[BB05] Jos C. M. Baeten and Mario Bravetti. A ground-complete axiomatization of finite state processes in process algebra. In Proceedings of the 16th International Conference on Concurrency Theory, Lecture Notes in Computer Science. Springer, 2005. To appear.
[BBS95] Jos C. M. Baeten, Jan A. Bergstra, and Scott A. Smolka. Axiomatizing probabilistic processes: ACP with generative probabilities. Information and Computation, 121(2):234-255, 1995.
[BD95] Michele Boreale and Rocco De Nicola. Testing equivalences for mobile processes. Information and Computation, 120:279-303, 1995.
[Bec80] Frank S. Beckman. Mathematical Foundations of Programming. Addison-Wesley, 1980.
[Bez03] Marc Bezem. Mathematical background. In Term Rewriting Systems, pages 790-825. Cambridge University Press, 2003.
[BGW01] Nikita Borisov, Ian Goldberg, and David Wagner. Intercepting mobile communications :The insecurity of 802.11. In Proceedings of the 7th Annual International Conference on Mobile Computing and Networking, pages 180-189. ACM Press, 2001.
[BH97] Christel Baier and Holger Hermanns. Weak bisimulation for fully probabilistic processes. In Proceedings of the 9th International Conference on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 119-130. Springer, 1997.
[BK84] Jan A. Bergstra and Jan Willem Klop. Process algebra for synchronous communication. Information and Computation, 60:109-137, 1984.
[Bou92] Gérard Boudol. Asynchrony and the n-calculus (note). Technical Report RR-1702, INRIA Sophia-Antipolis, 1992.
[Bou03] Gérard Boudol. On strong normalization in the intersection type discipline. In Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications, volume 2701 of Lecture Notes in Computer Science, pages 60-74. Springer, 2003.
[BS98] Michele Boreale and Davide Sangiorgi. Bisimulation in name-passing calculi without matching. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pages 165-175. IEEE, Computer Society Press, 1998.
[BS01] Emanuele Bandini and Roberto Segala. Axiomatizations for probabilistic bisimulation. In Proceedings of the 28th International Colloquium on Automata, Languages and Programming, volume 2076 of Lecture Notes in Computer Science, pages 370-381. Springer, 2001.
[BW90] Jos C. M. Baeten and W. P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.
[CG00] Luca Cardelli and Andrew D. Gordon. Mobile ambients. Theoretical Computer Science, 240(1):177-213, 2000.
[Cod70] E.F. Codd. A relational model for large shared databanks. Communications of the ACM, 13(6):377-387, 1970.
[CS02] Stefano Cattani and Roberto Segala. Decision algorithms for probabilistic bisimulation. In Proceedings of the 13th International Conference on Concurrency Theory, volume 2421 of Lecture Notes in Computer Science, pages 371-385. Springer, 2002.
[DCPP05] Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang. Metrics for actionlabelled quantitative transition systems. In Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages, Electronic Notes in Theoretical Computer Science, 2005. To appear.
[DFP98] Rocco De Nicola, Gian Luigi Ferrari, and Rosario Pugliese. Kaim: a kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering, 24(5):315-330, 1998.
[DH95] Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, 142(2):179-207, 1995.
[DJ90] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, chapter 6, pages 243-320. North-Holland, 1990.
[DJGP02] Josee Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 413-422. IEEE Computer Society, 2002.
[DJGP04] Josee Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. Metrics for labelled markov processes. Theoretical Computer Science, 318(3):323-354, 2004.
[DM79] Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465-476, 1979.
[DP05] Yuxin Deng and Catuscia Palamidessi. Axiomatizations for probabilistic finite-state behaviors. In Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures, volume 3441 of Lecture Notes in Computer Science, pages 110-124. Springer, 2005.
[DPP05] Yuxin Deng, Catuscia Palamidessi, and Jun Pang. Compositional reasoning for probabilistic finite-state behaviors, 2005. Submitted. A draft version is available at http://www.pps.jussieu.fr/nyuxin/publications/par.ps.
[DS04a] Yuxin Deng and Davide Sangiorgi. Ensuring termination by typability. In Proceedings of the 3rd IFIP International Conference on Theoretical Computer Science, pages 619-632. Kluwer, 2004.
[DS04b] Yuxin Deng and Davide Sangiorgi. Towards an algebraic theory of typed mobile processes. In Proceedings of the 31st International Colloquium on Automata, Languages and Programming, volume 3142 of Lecture Notes in Computer Science, pages 445-456. Springer, 2004.
[DS05] Yuxin Deng and Davide Sangiorgi. Towards an algebraic theory of typed mobile processes. Theoretical Computer Science, 2005. To appear.
[Fou98] Cédric Fournet. The Join-Calculus: A Calculus for Distributed Mobile Programming. PhD thesis, Ecole Polytechnique, Paris, France, 1998.
[Fu99] Yuxi Fu. Variations on mobile processes. Theoretical Computer Science, 221(1-2):327-368, 1999.
[FY03] Yuxi Fu and Zhenrong Yang. Tau laws for pi calculus. Theoretical Computer Science, 308:55-130, 2003.
[Gan80] Robin O. Gandy. Proofs of strong normalization. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
[GJS90] Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proceedings of IFIP TC2 Working Conference on Programming Concepts and Methods, 1990.
[HJ90] Hans Hansson and Bengt Jonsson. A calculus for communicating systems with time and probabilities. In Proceedings of IEEE Real-Time Systems Symposium, pages 278-287. IEEE Computer Society Press, 1990.
[Hoa85] C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
[HP04] Oltea M. Herescu and Catuscia Palamidessi. Probabilistic asynchronous pi-calculus. Technical report, INRIA Futurs and LIX, 2004.
[HR02a] Matthew Hennessy and James Riely. Information flow vs. resource access in the asynchronous pi-calculus. ACM Transactions on Programming Languages and Systems, 24(5):566-591, 2002.
[HR02b] Matthew Hennessy and James Riely. Resource access control in systems of mobile agents. Information and Computation, 173(1):82-120, 2002.
[HR04] Matthew Hennessy and Julian Rathke. Typed behavioural equivalences for processes in the presence of subtyping. Mathematical Structures in Computer Science, 14:651-684, 2004.
[HT91] Kohei Honda and Mario Tokoro. An object calculus for asynchronous communication. In Proceedings of the 5th European Conference on Object-Oriented Programming, volume 512 of Lecture Notes in Computer Science, pages 133-147. Springer, 1991.
[HVY00] Kohei Honda, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. Secure information flow as typed process behaviour. In Proceedings of the 9th European Symposium on Programming Languages and Systems, volume 1782 of Lecture Notes in Computer Science, pages 180-199. Springer, 2000.
[HY05] Kohei Honda and Nobuko Yoshida. Noninterference through flow analysis. Journal Functional Programming, 2005. To appear.
[Jon93] Cliff B. Jones. A n-calculus semantics for an object-based design notation. In Proceedings of the 4th International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 158-172. Springer, 1993.
[Kob98] Naoki Kobayashi. A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems, 20(2):436-482, 1998.
[Kob00] Naoki Kobayashi. Type systems for concurrent processes: From deadlock-freedom to livelock-freedom, time-boundedness. In Proceedings of the 1st IFIP International Conference on Theoretical Computer Science, volume 1872 of Lecture Notes in Computer Science, pages 365-389. Springer, 2000.
[KPT99] Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the picalculus. ACM Transactions on Programming Languages and Systems, 21(5):914-947, 1999.
[Lin94] Huimin Lin. Symbolic bisimulation and proof systems for the n-calculus. Technical Report 7/94, School of Cognitive and Computing Sciences, University of Sussex, 1994.
[Lin03] Huimin Lin. Complete inference systems for weak bisimulation equivalences in the n-calculus. Information and Computation, 180(1):1-29, 2003.
[LL03] A. Laurie and B. Laurie. Serious flaws in bluetooth security lead to disclosure of personal data, 2003. http://bluestumbler.org.
[Loa98] Ralph Loader. Notes on simply typed lambda calculus. Technical Report 381, LFCS, University of Edinburgh, 1998.
[Low91] Gavin Lowe. Probabilities and Priorities in Time CSP. PhD thesis, Oxford, 1991.
[LS91] Kim G. Larsen and Aren Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991.
[LS00] Francesca Levi and Davide Sangiorgi. Controlling interference in ambients. In Proceedings of the 27th ACM symposium on Principles of Programming Languages, pages 352-364. ACM Press, 2000.
[Mer00] Massimo Merro. Locality in the n-calculus and applications to distributed objects. PhD thesis, Ecole des Mines de Paris, France, 2000.
[Mil78] Robin Milner. Synthesis of communicating behaviour. In Proceedings of the 7th Symposium on Mathematical Foundations of Computer Science, volume 64 of Lecture Notes in Computer Science, pages 71-83. Springer, 1978.
[Mil80] Robin Milner. A calculus of communicating systems. volume 92 of Lecture Notes in Computer Science. Springer, 1980.
[Mil84] Robin Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Science, 28:439-466, 1984.
[Mil89a] Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
[Mil89b] Robin Milner. A complete axiomatisation for observational congruence of finite-state behaviours. Information and Computation, 81:227-247, 1989.
[Mil91] Robin Milner. The polyadic n-calculus: A tutorial. Technical Report ECS-LFCS-91-180, Department of Computer Science, University of Edingburgh, 1991.
[Mil92] Robin Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2):119-141, 1992.
[Mil99] Robin Milner. Communicating and Mobile Systems: the n-Calculus. Cambridge University Press, 1999.
[MPW92] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, part I/II. Information and Computation, 100:1-77, 1992.
[Nes00] Uwe Nestmann. What is a ‘good' encoding of guarded choice? Information and Computation, 156:287-319, 2000.
[Pal03] Catuscia Palamidessi. Comparing the expressive power of the synchronous and the asynchronous pi-calculus. Mathematical Structures in Computer Science, 13(5):685-719, 2003.
[Par01] Joachim Parrow. An introduction to the pi-calculus. In Handbook of Process Algebra, pages 479-543. Elsevier, 2001.
[PH04] Catuscia Palamidessi and Oltea M. Herescu. A randomized encoding of the n-calculus with mixed choice. Technical report, INRIA Futurs and LIX, 2004.
[Plo81] Gordon Plotkin. A structural approach operational semantics. Technical Report DAIMIFN-19, Computer Science Department, Aarhus University, 1981.
[PLS00] Anna Philippou, Insup Lee, and Oleg Sokolsky. Weak bisimulation for probabilistic systems. In Proceedings of the 11th International Conference on Concurrency Theory, volume 1877 of Lecture Notes in Computer Science, pages 334-349. Springer, 2000.
[PS95] Joachim Parrow and Davide Sangiorgi. Algebraic theories for name-passing calculi. In-formation and Computation, 120(2):174-197, 1995.
[PS96] Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409-454, 1996.
[PV98] Joachim Parrow and Bj¨orn Victor. The fusion calculus: Expressiveness and symmetry in mobile processes. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pages 176-185. IEEE, Computer Society Press, 1998.
[RG02] Raghu Ramakrishnan and Johannes Gehrke. Database Management Systems. McGraw-Hill, 2002.
[San93] Davide Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis CST-99-93, Department of Computer Science, University of Edingburgh, 1993.
[San96a] Davide Sangiorgi. n-calculus, internal mobility and agent-passing calculi. Theoretical Computer Science, 167:235-274, 1996.
[San96b] Davide Sangiorgi. A theory of bisimulation for the n-calculus. Acta Informatica, 33:69-97, 1996.
[San99] Davide Sangiorgi. The typed n-calculus at work: A proof of jones's parallelisation transformation on concurrent objects. Theory and Practice of Object-Oriented Systems, 5(1):25-33, 1999.
[San05] Davide Sangiorgi. Termination of processes. Mathematical Structures in Computer Science, 2005. To appear.
[SdV04] Ana Sokolova and Erik P. de Vink. Probabilistic automata: system types, parallel composition and comparison. In Validation of Stochastic Systems: A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science, pages 1-43. Springer, 2004.
[Seg95] Roberto Segala. Modeling and verification of randomized distributed real-time systems. Technical Report MIT/LCS/TR-676, PhD thesis, MIT, Dept. of EECS, 1995.
[SL94] Roberto Segala and Nancy A. Lynch. Probabilistic simulations for probabilistic processes. In Proceedings of the 5th International Conference on Concurrency Theory, volume 836 of Lecture Notes in Computer Science, pages 481-496. Springer, 1994.
[SM92] Davide Sangiorgi and Robin Milner. The problem of "weak bisimulation up-to". In Proceedings of the 3th International Conference on Concurrency Theory, volume 630 of Lecture Notes in Computer Science, pages 32-46. Springer, 1992.
[SS00] Eugene W. Stark and Scott A. Smolka. A complete axiom system for finite-state probabilistic processes. In Proof, language, and interaction: essays in honour of Robin Milner, pages 571-595. MIT Press, 2000.
[Sta79] Richard Statman. The typed n-calculus is not elementary recursive. Theoretical Computer Science, 9(1):73-81, 1979.
[Sto02] Mari¨elle Stoelinga. Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, University of Nijmegen, 2002.
[SW01] Davide Sangiorgi and David Walker. The n-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001.
[Tho95] Bent Thomsen. A theory of higher order communicating systems. Information and Computation, 116(1):38-57, 1995.
[Tof94] Chris Tofts. Processes with probabilities, priority and time. Formal Aspects of Computing, 6(5):536-564, 1994.
[vBW01] Franck van Breugel and James Worrell. An algorithm for quantitative verification of probabilistic transition systems. In Proceedings of the 12th International Conference on Concurrency Theory, volume 2154 of Lecture Notes in Computer Science, pages 336-350. Springer, 2001.
[vBW04] Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 2004. In press.
[vdP01] Jaco van de Pol. A prover for the mucrl toolset with applications - version 0.1. Technical Report SEN-R0106, CWI, Amsterdam, 2001.
[vGSS95] Rob J. van Glabbeek, Scott A. Smolka, and Bernhard Steffen. Reactive, generative, and stratified models of probabilistic processes. Information and Computation, 121(1):59-80,
1995.[VH93] Vasco Thudichum Vasconcelos and Kohei Honda. Principal typing schemes in a polyadic n-calculus. In Proceedings of the 4th International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 524-538. Springer, 1993.
[Wal95] David Walker. Objects in the n-calculus. Information and Computation, 116(2):253-271, 1995.
[YBH04] Nobuko Yoshida, Martin Berger, and Kohei Honda. Strong normalisation in the picalculus. Information and Computation, 191(2):145-202, 2004.
[YL92] Wang Yi and Kim Larsen. Testing probabilistic and nondeterministic processes. In Proceedings of the 12th IFIP International Symposium on Protocol Specification, Testing and Verification, pages 47-61. North Holland, 1992.
[Zan03] Hans Zantema. Termination. In Term Rewriting Systems, pages 181-259. Cambridge University Press, 2003.

Table of content

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 n-calculus
2.2.1 From CCS to the n-calculus
2.2.2 The Untyped n-calculus
2.2.3 Sorts and Sorting
2.2.4 A Simple Example
2.2.5 The Simply Typed n-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 n-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 n-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 Work
A Proofs from Chapter 3
A.1 Proof of Lemma 3 - 14
A.2 Proof of Proposition 3 - 34
A.3 Proof of Lemma 3 - 36
A.4 Proof of Lemma 3 - 45
B Proofs from Chapter 4
B.1 Some More Derived Rules
B.2 Proof of Theorem 4 - 36
C Proofs from Chapter 5
C.1 Proofs from Section 5 - 2
C.2 Proofs from Section 5 - 3
C.3 Extending T 0 with Polyadicity and Conditional
C.4 Proofs from Section 5 - 4
C.5 Proofs from Section 5 - 5
C.6 Levels in the Join-calculus
Bibliography

Statistiques de consultation

Repository Staff Only: edit this item