) 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 ?) ,
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. ,
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=10.1.1.35.8514
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=10.1.1.89.9437
Process Algebra with Probabilistic Choice, 1999. ,
DOI : 10.1007/3-540-48778-6_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.4225
The lambda Calculus: Its Syntax and Semantics, 1984. ,
A ground-complete axiomatization of finite state processes in process algebra, Proceedings of the 16th International Conference on Concurrency Theory, 2005. ,
Axiomatizing probabilistic processes: ACP with generative probabilities, Information and Computation, vol.121, issue.2, pp.234-255, 1995. ,
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
Mathematical Foundations of Programming, 1980. ,
Mathematical background, Term Rewriting Systems, pp.790-825 ,
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
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=10.1.1.141.5616
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
Asynchrony and the ?-calculus (note), 1992. ,
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
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
Axiomatizations for Probabilistic Bisimulation ,
DOI : 10.1007/3-540-48224-5_31
Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science, 1990. ,
Mobile ambients, Theoretical Computer Science, vol.240, issue.1, pp.177-213, 2000. ,
DOI : 10.1016/S0304-3975(99)00231-5
A relational model for large shared databanks, Communications of the ACM, vol.13, issue.6, pp.377-387, 1970. ,
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=10.1.1.4.589
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
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
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
Rewrite Systems, In Handbook of Theoretical Computer Science, chapter, pp.243-320, 1990. ,
DOI : 10.1016/B978-0-444-88074-1.50011-1
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
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
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
Compositional Reasoning for Probabilistic Finite-State Behaviors, 2005. ,
DOI : 10.1007/11601548_17
URL : https://hal.archives-ouvertes.fr/hal-00159683
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
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
Towards an algebraic theory of typed mobile processes, Theoretical Computer Science, 2005. ,
URL : https://hal.archives-ouvertes.fr/hal-00159674
The Join-Calculus: A Calculus for Distributed Mobile Programming, 1998. ,
Variations on mobile processes, Theoretical Computer Science, vol.221, issue.1-2, pp.327-368, 1999. ,
DOI : 10.1016/S0304-3975(99)00037-7
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
Proofs of strong normalization, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980. ,
Algebraic reasoning for probabilistic concurrent systems, Proceedings of IFIP TC2 Working Conference on Programming Concepts and Methods, 1990. ,
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
Communicating Sequential Processes, 1985. ,
Probabilistic asynchronous pi-calculus, INRIA Futurs and LIX, 2004. ,
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
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
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
An object calculus for asynchronous communication ,
DOI : 10.1007/BFb0057019
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
Noninterference through flow analysis, Journal of Functional Programming, vol.15, issue.2, 2005. ,
DOI : 10.1017/S0956796804005477
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
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
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
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
Symbolic bisimulation and proof systems for the ?-calculus, School of Cognitive and Computing Sciences, 1994. ,
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
Serious flaws in bluetooth security lead to disclosure of personal data, 2003. ,
Notes on simply typed lambda calculus, 1998. ,
Probabilities and Priorities in Time CSP, 1991. ,
Bisimulation through probabilistic testing, Information and Computation, vol.94, issue.1, pp.1-28, 1991. ,
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
Locality in the ?-calculus and applications to distributed objects, 2000. ,
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
A calculus of communicating systems, Lecture Notes in Computer Science, vol.92, 1980. ,
DOI : 10.1007/3-540-10235-3
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
Communication and Concurrency, 1989. ,
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
The Polyadic ??-Calculus: a Tutorial, 1991. ,
DOI : 10.1007/978-3-642-58041-3_6
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
Communicating and Mobile Systems: the ?-Calculus, 1999. ,
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
What is a 'good' encoding of guarded choice? Information and Computation, pp.287-319, 2000. ,
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
An introduction to the pi-calculus, Handbook of Process Algebra, pp.479-543, 2001. ,
A Randomized Distributed Encoding of the ??-Calculus with Mixed Choice, 2004. ,
DOI : 10.1007/978-0-387-35608-2_44
A structural approach operational semantics, 1981. ,
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=10.1.1.145.6312
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=10.1.1.35.7169
Typing and subtyping for mobile processes, Mathematical Structures in Computer Science, vol.6, issue.5, pp.409-454, 1996. ,
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
Database Management Systems, 2002. ,
Expressing Mobility in Process Algebras: First-Order and Higher- Order Paradigms, 1993. ,
??-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
A theory of bisimulation for the ??-calculus, Acta Informatica, vol.XVI, issue.2, pp.69-97, 1996. ,
DOI : 10.1007/s002360050036
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. ,
Termination of processes, Mathematical Structures in Computer Science, vol.16, issue.01, 2005. ,
DOI : 10.1017/S0960129505004810
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
Modeling and verification of randomized distributed real-time systems, 1995. ,
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
The problem of ???weak bisimulation up to???, Proceedings of the 3th International Conference on Concurrency Theory, pp.32-46, 1992. ,
DOI : 10.1007/BFb0084781
A complete axiom system for finite-state probabilistic processes, Proof, language, and interaction: essays in honour of Robin Milner, pp.571-595, 2000. ,
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
Alea jacta est: verification of probabilistic, real-time and parametric systems, 2002. ,
The ?-calculus: a Theory of Mobile Processes ,
A Theory of Higher Order Communicating Systems, Information and Computation, vol.116, issue.1, pp.38-57, 1995. ,
DOI : 10.1006/inco.1995.1004
Processes with probabilities, priority and time, Formal Aspects of Computing, vol.458, issue.3, pp.536-564, 1994. ,
DOI : 10.1007/BF01211867
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
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. ,
Strong normalisation in the ??-calculus, Information and Computation, vol.191, issue.2, pp.145-202, 2004. ,
DOI : 10.1016/j.ic.2003.08.004
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