Skip to main content
SpringerLink
Log in

On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems

  • Conference paper
Quantitative Evaluation of Systems (QEST 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8657))

Included in the following conference series:

Abstract

Testing equivalences have been deeply investigated on fully nondeterministic processes, as well as on processes featuring probabilities and internal nondeterminism. This is not the case with reactive probabilistic processes, for which it is only known that the discriminating power of probabilistic bisimilarity is achieved when admitting a copying capability within tests. In this paper, we introduce for reactive probabilistic processes three testing equivalences without copying, which are respectively based on reactive probabilistic tests, fully nondeterministic tests, and nondeterministic and probabilistic tests. We show that the three testing equivalences are strictly finer than probabilistic failure-trace equivalence, and that the one based on nondeterministic and probabilistic tests is strictly finer than the other two, which are incomparable with each other. Moreover, we provide a number of facts that lead us to conjecture that (i) may testing and must testing coincide on reactive probabilistic processes and (ii) nondeterministic and probabilistic tests reach the same discriminating power as probabilistic bisimilarity.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky, S.: Observational equivalence as a testing equivalence. Theoretical Computer Science 53, 225–241 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  2. Baier, C., Kwiatkowska, M.: Domain equations for probabilistic processes. Mathematical Structures in Computer Science 10, 665–717 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. Logical Methods in Computer Science 10(1:16), 1–42 (2014)

    Google Scholar 

  4. Bernardo, M., De Nicola, R., Loreti, M.: Relating strong behavioral equivalences for processes with nondeterminism and probabilities. Theoretical Computer Science (2014)

    Google Scholar 

  5. Bernardo, M., Sangiorgi, D., Vignudelli, V.: On the discriminating power of passivation and higher-order interaction. In: Proc. of CSL/LICS. ACM Press (2014)

    Google Scholar 

  6. Bloom, B., Meyer, A.R.: A remark on bisimulation between probabilistic processes. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 26–40. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  7. van Breugel, F., Mislove, M., Ouaknine, J., Worrell, J.: Domain theory, testing and simulation for labelled Markov processes. Theoretical Computer Science 333, 171–197 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  8. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31, 560–599 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  9. De Nicola, R.: Extensional equivalences for transition systems. Acta Informatica 24, 211–237 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  10. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  11. Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.: Characterising testing preorders for finite probabilistic processes. Logical Methods in Computer Science 4(4:4), 1–33 (2008)

    Google Scholar 

  12. Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C., Zhang, C.: Remarks on testing probabilistic processes. In: Computation, Meaning, and Logic: Articles Dedicated to Gordon Plotkin. ENTCS, vol. 172, pp. 359–397. Elsevier (2007)

    Google Scholar 

  13. Deng, Y., van Glabbeek, R.J., Morgan, C., Zhang, C.: Scalar outcomes suffice for finitary probabilistic testing. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 363–378. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Information and Computation 179, 163–193 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  15. van Glabbeek, R.J.: The linear time – branching time spectrum I. In: Handbook of Process Algebra, pp. 3–99. Elsevier (2001)

    Google Scholar 

  16. van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Information and Computation 121, 59–80 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  17. Huynh, D.T., Tian, L.: On some equivalence relations for probabilistic processes. Fundamenta Informaticae 17, 211–234 (1992)

    MATH  MathSciNet  Google Scholar 

  18. Jonsson, B., Ho-Stuart, C., Yi, W.: Testing and refinement for nondeterministic and probabilistic processes. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 418–430. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  19. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proc. of LICS, pp. 266–277. IEEE-CS Press (1991)

    Google Scholar 

  20. Jonsson, B., Yi, W.: Compositional testing preorders for probabilistic processes. In: Proc. of LICS, pp. 431–441. IEEE-CS Press (1995)

    Google Scholar 

  21. Jou, C.-C., Smolka, S.A.: Equivalences, congruences, and complete axiomatizations for probabilistic processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 367–383. Springer, Heidelberg (1990)

    Google Scholar 

  22. Keller, R.M.: Formal verification of parallel programs. Communications of the ACM 19, 371–384 (1976)

    Article  MATH  Google Scholar 

  23. Kwiatkowska, M., Norman, G.: A testing equivalence for reactive probabilistic processes. In: Proc. of EXPRESS. ENTCS, vol. 16(2), pp. 114–132. Elsevier (1998)

    Google Scholar 

  24. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94, 1–28 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  25. Lynch, N.A., Segala, R., Vaandrager, F.: Compositionality for probabilistic automata. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 208–221. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  26. Milner, R.: Communication and Concurrency. Prentice Hall (1989)

    Google Scholar 

  27. Phillips, I.: Refusal testing. Theoretical Computer Science 50, 241–284 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  28. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons (1994)

    Google Scholar 

  29. Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD Thesis (1995)

    Google Scholar 

  30. Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234–248. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  31. Segala, R.: Testing probabilistic automata. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 299–314. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  32. Yi, W., Larsen, K.G.: Testing probabilistic and nondeterministic processes. In: Proc. of PSTV, pp. 47–61. North-Holland (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Università di Urbino, Italy

    Marco Bernardo

  2. Università di Bologna, Italy

    Davide Sangiorgi & Valeria Vignudelli

  3. INRIA, France

    Davide Sangiorgi & Valeria Vignudelli

Authors
  1. Marco Bernardo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Davide Sangiorgi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Valeria Vignudelli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK

    Gethin Norman

  2. University of Illinois, 61801-2918, Urbana, IL, USA

    William Sanders

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Bernardo, M., Sangiorgi, D., Vignudelli, V. (2014). On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems. In: Norman, G., Sanders, W. (eds) Quantitative Evaluation of Systems. QEST 2014. Lecture Notes in Computer Science, vol 8657. Springer, Cham. https://doi.org/10.1007/978-3-319-10696-0_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10696-0_23

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10695-3

  • Online ISBN: 978-3-319-10696-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation