J. J? and ?. , ) wt(D 2 P 2 ) The only reduction rule is, Following from Lemma C.16, it holds that wt(J?) = wt(J) wt(P ) = wt(P ?)

A. , S. Andova, and J. C. Baeten, The required result follows from Claim 3 Abstraction in probabilistic process algebra, Tools and Algorithms for the Construction and Analysis of Systems, pp.204-219, 2001.

M. Abadi, Secrecy by typing in security protocols, Journal of the ACM, vol.46, issue.5, pp.749-786, 1999.
DOI : 10.1145/324133.324266

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

L. Aceto, A. Zoltánzoltán´zoltánésik, and . Ingólfsdóttir, Equational Axioms for Probabilistic Bisimilarity (Preliminary Report), BRICS Report Series, vol.9, issue.6, 2002.
DOI : 10.7146/brics.v9i6.21724

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

S. Andova, Process Algebra with Probabilistic Choice, 1999.
DOI : 10.1007/3-540-48778-6_7

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

H. Barendregt, The lambda Calculus: Its Syntax and Semantics, 1984.

C. M. Jos, M. Baeten, and . Bravetti, A ground-complete axiomatization of finite state processes in process algebra, Proceedings of the 16th International Conference on Concurrency Theory, 2005.

C. M. Jos, J. A. Baeten, S. A. Bergstra, and . Smolka, Axiomatizing probabilistic processes: ACP with generative probabilities, Information and Computation, vol.121, issue.2, pp.234-255, 1995.

M. Boreale and R. D. Nicola, Testing Equivalence for Mobile Processes, Information and Computation, vol.120, issue.2, pp.279-303, 1995.
DOI : 10.1006/inco.1995.1114

URL : http://doi.org/10.1006/inco.1995.1114

. Bec80, S. Frank, and . Beckman, Mathematical Foundations of Programming, 1980.

M. Bezem, Mathematical background, Term Rewriting Systems, pp.790-825

N. Borisov, I. Goldberg, and D. Wagner, Intercepting mobile communications, Proceedings of the 7th annual international conference on Mobile computing and networking , MobiCom '01, pp.180-189, 2001.
DOI : 10.1145/381677.381695

C. Baier and H. Hermanns, Weak bisimulation for fully probabilistic processes, Proceedings of the 9th International Conference on Computer Aided Verification, pp.119-130, 1997.
DOI : 10.1007/3-540-63166-6_14

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

J. A. Bergstra and J. W. Klop, Process algebra for synchronous communication, Information and Control, vol.60, issue.1-3, pp.109-137, 1984.
DOI : 10.1016/S0019-9958(84)80025-X

G. Boudol, Asynchrony and the ?-calculus (note), 1992.

G. Boudol, On Strong Normalization in the Intersection Type Discipline, Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications, pp.60-74, 2003.
DOI : 10.1007/3-540-44904-3_5

M. Boreale and D. Sangiorgi, Bisimulation in name-passing calculi without matching, Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226), pp.165-175, 1998.
DOI : 10.1109/LICS.1998.705653

E. Bandini and R. Segala, Axiomatizations for Probabilistic Bisimulation
DOI : 10.1007/3-540-48224-5_31

C. M. Jos, W. P. Baeten, and . Weijland, Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science, 1990.

[. Cardelli and A. D. Gordon, Mobile ambients, Theoretical Computer Science, vol.240, issue.1, pp.177-213, 2000.
DOI : 10.1016/S0304-3975(99)00231-5

]. E. Cod70 and . Codd, A relational model for large shared databanks, Communications of the ACM, vol.13, issue.6, pp.377-387, 1970.

S. Cattani and R. Segala, Decision Algorithms for Probabilistic Bisimulation*, Proceedings of the 13th International Conference on Concurrency Theory, pp.371-385, 2002.
DOI : 10.1007/3-540-45694-5_25

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

Y. Deng, T. Chothia, C. Palamidessi, and J. Pang, Metrics for actionlabelled quantitative transition systems, Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages, 2005.
DOI : 10.1016/j.entcs.2005.10.033

URL : https://hal.archives-ouvertes.fr/hal-00159689

R. De-nicola, G. L. Ferrari, and R. Pugliese, KLAIM: a kernel language for agents interaction and mobility, IEEE Transactions on Software Engineering, vol.24, issue.5, pp.315-330, 1998.
DOI : 10.1109/32.685256

[. Dershowitz and C. Hoot, Natural termination, Theoretical Computer Science, vol.142, issue.2, pp.179-207, 1995.
DOI : 10.1016/0304-3975(94)00275-4

URL : http://doi.org/10.1016/0304-3975(94)00275-4

[. Dershowitz and J. Jouannaud, Rewrite Systems, In Handbook of Theoretical Computer Science, chapter, pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden, The metric analogue of weak bisimulation for probabilistic processes, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.413-422, 2002.
DOI : 10.1109/LICS.2002.1029849

J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden, Metrics for labelled Markov processes, DM79] Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings, pp.323-354465, 1979.
DOI : 10.1016/j.tcs.2003.09.013

Y. Deng and C. Palamidessi, Axiomatizations for Probabilistic Finite-State Behaviors, Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures, pp.110-124, 2005.
DOI : 10.1007/978-3-540-31982-5_7

URL : https://hal.archives-ouvertes.fr/hal-00159682

Y. Deng, C. Palamidessi, and J. Pang, Compositional Reasoning for Probabilistic Finite-State Behaviors, 2005.
DOI : 10.1007/11601548_17

URL : https://hal.archives-ouvertes.fr/hal-00159683

Y. Deng and D. Sangiorgi, Ensuring termination by typability, Proceedings of the 3rd IFIP International Conference on Theoretical Computer Science, pp.619-632
DOI : 10.1016/j.ic.2006.03.002

URL : https://hal.archives-ouvertes.fr/hal-00159679

Y. Deng and D. Sangiorgi, Towards an Algebraic Theory of Typed Mobile Processes, Proceedings of the 31st International Colloquium on Automata, Languages and Programming, pp.445-456
DOI : 10.1007/978-3-540-27836-8_39

URL : https://hal.archives-ouvertes.fr/hal-00159674

Y. Deng and D. Sangiorgi, Towards an algebraic theory of typed mobile processes, Theoretical Computer Science, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00159674

C. Fournet, The Join-Calculus: A Calculus for Distributed Mobile Programming, 1998.

Y. Fu, Variations on mobile processes, Theoretical Computer Science, vol.221, issue.1-2, pp.327-368, 1999.
DOI : 10.1016/S0304-3975(99)00037-7

Y. Fu and Z. Yang, Tau laws for pi calculus, Theoretical Computer Science, vol.308, issue.1-3, pp.55-130, 2003.
DOI : 10.1016/S0304-3975(03)00202-0

URL : http://doi.org/10.1016/s0304-3975(03)00202-0

R. O. Gandy, Proofs of strong normalization, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980.

A. Giacalone, C. Jou, and S. A. Smolka, Algebraic reasoning for probabilistic concurrent systems, Proceedings of IFIP TC2 Working Conference on Programming Concepts and Methods, 1990.

H. Hansson and B. Jonsson, A calculus for communicating systems with time and probabilities, [1990] Proceedings 11th Real-Time Systems Symposium, pp.278-287
DOI : 10.1109/REAL.1990.128759

]. C. Hoa85 and . Hoare, Communicating Sequential Processes, 1985.

M. Oltea, C. Herescu, and . Palamidessi, Probabilistic asynchronous pi-calculus, INRIA Futurs and LIX, 2004.

M. Hennessy and J. Riely, Information flow vs. resource access in the asynchronous pi-calculus, ACM Transactions on Programming Languages and Systems, vol.24, issue.5, pp.566-591, 2002.
DOI : 10.1145/570886.570890

M. Hennessy and J. Riely, Resource Access Control in Systems of Mobile Agents, Information and Computation, vol.173, issue.1, pp.82-120, 2002.
DOI : 10.1006/inco.2001.3089

M. Hennessy and J. Rathke, Typed behavioural equivalences for processes in the presence of subtyping, Mathematical Structures in Computer Science, vol.14, issue.5, pp.651-684, 2004.
DOI : 10.1017/S0960129504004281

K. Honda and M. Tokoro, An object calculus for asynchronous communication
DOI : 10.1007/BFb0057019

K. Honda, V. T. Vasconcelos, and N. Yoshida, Secure Information Flow as Typed Process Behaviour, Proceedings of the 9th European Symposium on Programming Languages and Systems, pp.180-199, 2000.
DOI : 10.1007/3-540-46425-5_12

K. Honda and N. Yoshida, Noninterference through flow analysis, Journal of Functional Programming, vol.15, issue.2, 2005.
DOI : 10.1017/S0956796804005477

C. B. Jones, A pi-calculus semantics for an object-based design notation, Proceedings of the 4th International Conference on Concurrency Theory, pp.158-172, 1993.
DOI : 10.1007/3-540-57208-2_12

N. Kobayashi, A partially deadlock-free typed process calculus, ACM Transactions on Programming Languages and Systems, vol.20, issue.2, pp.436-482, 1998.
DOI : 10.1145/276393.278524

N. Kobayashi, Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness, Proceedings of the 1st IFIP International Conference on Theoretical Computer Science, pp.365-389, 2000.
DOI : 10.1007/3-540-44929-9_27

N. Kobayashi, B. C. Pierce, and D. N. Turner, Linearity and the pi-calculus, ACM Transactions on Programming Languages and Systems, vol.21, issue.5, pp.914-947, 1999.
DOI : 10.1145/330249.330251

H. Lin, Symbolic bisimulation and proof systems for the ?-calculus, School of Cognitive and Computing Sciences, 1994.

H. Lin, Complete inference systems for weak bisimulation equivalences in the ??-calculus, Information and Computation, vol.180, issue.1, pp.1-29, 2003.
DOI : 10.1016/S0890-5401(02)00014-7

A. Laurie and B. Laurie, Serious flaws in bluetooth security lead to disclosure of personal data, 2003.

[. Loader, Notes on simply typed lambda calculus, 1998.

G. Lowe, Probabilities and Priorities in Time CSP, 1991.

G. Kim, A. Larsen, and . Skou, Bisimulation through probabilistic testing, Information and Computation, vol.94, issue.1, pp.1-28, 1991.

F. Levi and D. Sangiorgi, Controlling interference in ambients, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.352-364
DOI : 10.1145/325694.325741

M. Merro, Locality in the ?-calculus and applications to distributed objects, 2000.

[. Milner, Synthesis of communicating behaviour, Proceedings of the 7th Symposium on Mathematical Foundations of Computer Science, pp.71-83, 1978.
DOI : 10.1007/3-540-08921-7_57

[. Milner, A calculus of communicating systems, Lecture Notes in Computer Science, vol.92, 1980.
DOI : 10.1007/3-540-10235-3

R. Milner, A complete inference system for a class of regular behaviours, Journal of Computer and System Sciences, vol.28, issue.3, pp.439-466, 1984.
DOI : 10.1016/0022-0000(84)90023-0

[. Milner, Communication and Concurrency, 1989.

R. Milner, A complete axiomatisation for observational congruence of finite-state behaviours, Information and Computation, vol.81, issue.2, pp.227-247, 1989.
DOI : 10.1016/0890-5401(89)90070-9

[. Milner, The Polyadic ??-Calculus: a Tutorial, 1991.
DOI : 10.1007/978-3-642-58041-3_6

[. Milner, Functions as processes, Mathematical Structures in Computer Science, vol.4, issue.02, pp.119-141, 1992.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00075405

[. Milner, Communicating and Mobile Systems: the ?-Calculus, 1999.

[. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, I, Information and Computation, vol.100, issue.1, pp.1-77, 1992.
DOI : 10.1016/0890-5401(92)90008-4

U. Nestmann, What is a 'good' encoding of guarded choice? Information and Computation, pp.287-319, 2000.

[. Palamidessi, Comparing the expressive power of the synchronous and asynchronous $pi$ -calculi, Mathematical Structures in Computer Science, vol.13, issue.5, pp.685-719, 2003.
DOI : 10.1017/S0960129503004043

URL : https://hal.archives-ouvertes.fr/inria-00201104

J. Parrow, An introduction to the pi-calculus, Handbook of Process Algebra, pp.479-543, 2001.

[. Palamidessi and O. M. Herescu, A Randomized Distributed Encoding of the ??-Calculus with Mixed Choice, 2004.
DOI : 10.1007/978-0-387-35608-2_44

G. Plotkin, A structural approach operational semantics, 1981.

A. Philippou, I. Lee, and O. Sokolsky, Weak Bisimulation for Probabilistic Systems, Proceedings of the 11th International Conference on Concurrency Theory, pp.334-349, 2000.
DOI : 10.1007/3-540-44618-4_25

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

J. Parrow and D. Sangiorgi, Algebraic theories for name-passing calculi. Information and Computation, pp.174-197, 1995.
DOI : 10.1007/3-540-58043-3_27

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

C. Benjamin, D. Pierce, and . Sangiorgi, Typing and subtyping for mobile processes, Mathematical Structures in Computer Science, vol.6, issue.5, pp.409-454, 1996.

J. Parrow and B. Victor, The fusion calculus: expressiveness and symmetry in mobile processes, Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226), pp.176-185, 1998.
DOI : 10.1109/LICS.1998.705654

[. Ramakrishnan and J. Gehrke, Database Management Systems, 2002.

D. Sangiorgi, Expressing Mobility in Process Algebras: First-Order and Higher- Order Paradigms, 1993.

D. Sangiorgi, ??-Calculus, internal mobility, and agent-passing calculi, Theoretical Computer Science, vol.167, issue.1-2, pp.235-274, 1996.
DOI : 10.1016/0304-3975(96)00075-8

URL : http://doi.org/10.1016/0304-3975(96)00075-8

D. Sangiorgi, A theory of bisimulation for the ??-calculus, Acta Informatica, vol.XVI, issue.2, pp.69-97, 1996.
DOI : 10.1007/s002360050036

D. Sangiorgi, The typed ?-calculus at work: A proof of jones's parallelisation transformation on concurrent objects. Theory and Practice of Object-Oriented Systems, pp.25-33, 1999.

D. Sangiorgi, Termination of processes, Mathematical Structures in Computer Science, vol.16, issue.01, 2005.
DOI : 10.1017/S0960129505004810

A. Sokolova and E. P. De-vink, Probabilistic Automata: System Types, Parallel Composition and Comparison, Validation of Stochastic Systems: A Guide to Current Research, pp.1-43, 2004.
DOI : 10.1007/978-3-540-24611-4_1

R. Segala, Modeling and verification of randomized distributed real-time systems, 1995.

R. Segala and N. A. Lynch, Probabilistic Simulations for Probabilistic Processes, Proceedings of the 5th International Conference on Concurrency Theory, pp.481-496, 1994.
DOI : 10.1007/978-3-540-48654-1_35

D. Sangiorgi and R. Milner, The problem of ???weak bisimulation up to???, Proceedings of the 3th International Conference on Concurrency Theory, pp.32-46, 1992.
DOI : 10.1007/BFb0084781

E. W. Stark and S. A. Smolka, A complete axiom system for finite-state probabilistic processes, Proof, language, and interaction: essays in honour of Robin Milner, pp.571-595, 2000.

R. Statman, The typed ??-calculus is not elementary recursive, Theoretical Computer Science, vol.9, issue.1, pp.73-81, 1979.
DOI : 10.1016/0304-3975(79)90007-0

M. Stoelinga, Alea jacta est: verification of probabilistic, real-time and parametric systems, 2002.

D. Sangiorgi and D. Walker, The ?-calculus: a Theory of Mobile Processes

[. Thomsen, A Theory of Higher Order Communicating Systems, Information and Computation, vol.116, issue.1, pp.38-57, 1995.
DOI : 10.1006/inco.1995.1004

C. Tofts, Processes with probabilities, priority and time, Formal Aspects of Computing, vol.458, issue.3, pp.536-564, 1994.
DOI : 10.1007/BF01211867

R. J. Van-glabbeek, S. A. Smolka, and B. Steffen, Reactive, generative, and stratified models of probabilistic processes, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.59-80, 1995.
DOI : 10.1109/LICS.1990.113740

V. Thudichum, V. , and K. Honda, Principal typing schemes in a polyadic ?-calculus, Proceedings of the 4th International Conference on Concurrency Theory Objects in the ?-calculus. Information and Computation, pp.524-538253, 1993.

N. Yoshida, M. Berger, and K. Honda, Strong normalisation in the ??-calculus, Information and Computation, vol.191, issue.2, pp.145-202, 2004.
DOI : 10.1016/j.ic.2003.08.004

W. Yi and K. Larsen, Testing Probabilistic and Nondeterministic Processes, Proceedings of the 12th IFIP International Symposium on Protocol Specification, Testing and Verification, pp.47-61, 1992.
DOI : 10.1016/B978-0-444-89874-6.50010-6