Characterisations of testing preorders for a finite probabilistic π-calculus
Authors: 
Yuxin Deng, Alwen TiuAuthors Info & Claims
Pages 701 - 726
Abstract
We consider two characterisations of the may and must testing preorders for a probabilistic extension of the finite π-calculus: one based on notions of probabilistic weak simulations, and the other on a probabilistic extension of a fragment of Milner–Parrow–Walker modal logic for the π-calculus. We base our notions of simulations on similar concepts used in previous work for probabilistic CSP. However, unlike the case with CSP (or other non-value-passing calculi), there are several possible definitions of simulation for the probabilistic π-calculus, which arise from different ways of scoping the name quantification. We show that in order to capture the testing preorders, one needs to use the “earliest” simulation relation (in analogy to the notion of early (bi)simulation in the non-probabilistic case). The key ideas in both characterisations are the notion of a “characteristic formula” of a probabilistic process, and the notion of a “characteristic test” for a formula. As in an earlier work on testing equivalence for the π-calculus by Boreale and De Nicola, we extend the language of the π-calculus with a mismatch operator, without which the formulation of a characteristic test will not be possible.
References
References
[1]
Acciai L, Boreale M, De Nicola R (2011) Linear-time and may-testing in a probabilistic reactive setting. In: Proceedings of the conference on FMOODS/FORTE. LNCS, vol 6722. Springer, Berlin, pp 29–43
[2]
Boreale M and De Nicola R Testing equivalence for mobile processes Inf Comput 1995 120 2 279-303
[3]
Chatzikokolakis K and Palamidessi C A framework for analyzing probabilistic protocols and its application to the partial secrets exchange Theor Comput Sci 2007 389 3 512-527
[4]
Cheung L, Stoelinga M, and Vaandrager F A testing scenario for probabilistic processes J ACM 2007 54 6 1-45
[5]
De Nicola R and Hennessy M Testing equivalences for processes Theor Comput Sci 1984 34 83-133
[6]
Deng Y, van Glabbeek RJ, Hennessy M, Morgan C, and Zhang C Remarks on testing probabilistic processes ENTCS 2007 172 359-397
[7]
Deng Y, van Glabbeek RJ, Hennessy M, and Morgan C Characterising testing preorders for finite probabilistic processes Logical Methods Comput Sci 2008 4 4 1-33
[8]
Deng Y, van Glabbeek RJ, Hennessy M, Morgan C (2009) Testing finitary probabilistic processes. In: Proceedings of the conference on CONCUR. LNCS, vol 5710. Springer, Berlin, pp 274–288
[9]
Deng Y, van Glabbeek RJ, Morgan C, Zhang C (2007) Scalar outcomes suffice for finitary probabilistic testing. In: Proceedings of the conference on ESOP. LNCS, vol 4421. Springer, Berlin, pp 363–378
[10]
Ferrari GL, Montanari U, Quaglia P (1995) The weak late pi-calculus semantics as observation equivalence. In: Proceeding of the conference on CONCUR. LNCS, vol 962. Springer, Berlin, pp 57–71
[11]
Hennessy M (1982) Power domains and nondeterministic recursive definitions. In: Proceedings of the conference symposium on programming. LNCS, vol 137. Springer, Berlin, pp 178–193
[12]
Hennessy M Algebraic Theory of Processes 1988 Cambridge MIT Press
[13]
Hansson H, Jonsson B (1990) A calculus for communicating systems with time and probabilities. In: Proceedings of the conference on IEEE real time systems symposium, pp 278–287
[14]
Hoare CAR Communicating sequential processes 1985 Englewood Cliffs Prentice-Hall
[15]
Herescu OM, Palamidessi C (2000) Probabilistic asynchronous pi-calculus. In: Proceedings of the conference on FoSSaCS. LNCS, vol 1784, Springer, Berlin, pp 146–160
[16]
Ingólfsdóttir A Late and early semantics coincide for testing Theor Comput Sci 1995 146 1–2 341-349
[17]
Milner R, Parrow J, and Walker D A calculus of mobile processes, II Inf Comput 1992 100 1 41-77
[18]
Milner R, Parrow J, and Walker D Modal logics for mobile processes Theor Comput Sci 1993 114 1 149-171
[19]
Norman G, Palamidessi C, Parker D, and Wu P Model checking probabilistic and stochastic extensions of the pi-calculus IEEE Trans Softw Eng 2009 35 2 209-223
[20]
Parma A, Segala R (2007) Logical characterizations of bisimulations for discrete probabilistic systems. In: Proceedings of the conference on FOSSACS. LNCS, vol 4423. Springer, Berlin, pp 287–301
[21]
Sangiorgi D Bisimulation for higher-order process calculi Inf Comput 1996 131 2 141-178
[22]
Sangiorgi D On the bisimulation proof method Math Struct Comput Sci 1998 8 5 447-479
[23]
Segala R (1996) Testing probabilistic automata. In: Proceedings of the conference on CONCUR. LNCS, vol 1119. Springer, Berlin, pp 299–314
[24]
Segala R, Lynch NA (1994) Probabilistic simulations for probabilistic processes. In: Proceedings of the conference on CONCUR, LNCS, vol 836. Springer, Berlin, pp 481–496
[25]
Sangiorgi D and Walker D π-calculus: a theory of mobile processes 2001 Cambridge Cambridge University Press
[26]
Van Glabbeek RJ, Smolka SA, and Steffen B Reactive, generative and stratified models of probabilistic processes Inf Comput 1995 121 1 59-80
[27]
Van Glabbeek RJ and Weijland WP Branching time and abstraction in bisimulation semantics J ACM 1996 43 3 555-600
[28]
Wang Y, Larsen KG (1992) Testing probabilistic and nondeterministic processes. In: Proceedings of the conference on PSTV. IFIP transactions, vol C-8. North-Holland, Amsterdam, pp 47–61
Recommendations
Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus
In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59-68, 2006] the authors studied the expressiveness of persistence in the asynchronous @p-calculus (...
Bisimilar and Logically Equivalent Programs in PDL
In standard Propositional Dynamic Logic (PDL) literature [D. Harel and D. Kozen and J. Tiuryn. Dynamic Logics. MIT Press, 2000; R. Goldblatt. Logics of Time and Computation. CSLI Lecture Notes 7. Stanford, 1992; P. Blackburn, M. de Rijke, and Y. Venema. ...
Proof search specifications of bisimulation and modal logics for the π-calculus
We specify the operational semantics and bisimulation relations for the finite φ-calculus within a logic that contains the ∇ quantifier for encoding generic judgments and definitions for encoding fixed points. Since we restrict to the finite case, the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© British Computer Society 2012.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 July 2012
Accepted: 24 April 2012
Received: 20 December 2011
Published in FAC Volume 24, Issue 4-6
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 31Total Downloads
- Downloads (Last 12 months)19
- Downloads (Last 6 weeks)4
Reflects downloads up to 10 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in