Skip to main content
SpringerLink
Log in

Fully Abstract Characterization of Probabilistic May Testing

  • Conference paper
  • First Online:
Formal Methods for Real-Time and Probabilistic Systems (ARTS 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1601))

Abstract

In this paper, to develop a refinement relation for probabilistic and nondeterministic systems, we study a notion of probabilistic testing, that extends the testing framework of de Nicola and Hennessy for nondeterministic processes to the probabilistic setting. We present a model of probabilistic computation trees, which corresponds to the classic trace model for non-probabilistic systems. Our main contribution is a fully abstract characterization of the may-testing preorder which is essential for the probabilistic setting. The characterization is given based on convex closures of probabilistic computation trees.

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. Samson Abramsky. Observation equivalence as a testing equivalence. Theoretical Computer Science, 53(2,3):225–241, 1987.

    Article  MathSciNet  MATH  Google Scholar 

  2. I. Christoff. Testing equivalences and fully abstract models for probabilistic processes. In Baeten, editor, Proc. CONCUR, Amsterdam, volume 458 of Lecture Notes in Computer Science, pages 126–140. Springer Verlag, 1990.

    Google Scholar 

  3. R. Cleaveland, S. Smolka, and A. Zwarico. Testing preorders for probabilistic processes. In Proc. ICALP’ 92, 1992.

    Google Scholar 

  4. C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. In Proc. 29th Annual Symp. Foundations of Computer Science, pages 338–345, 1988.

    Google Scholar 

  5. R. de Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.

    Article  MathSciNet  MATH  Google Scholar 

  6. A. Giacalone, C. Jou, and S.A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proc. IFIP TC2 Working Conference on Programming Concepts and Methods, Sea of Galilee, April 1990.

    Google Scholar 

  7. H. Hansson and B. Jonsson. A calculus for communicating systems with time and probabilities. In Proc. 11th IEEE Real-Time Systems Symposium, Orlando, Florida, 1990.

    Google Scholar 

  8. H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512–535, 1994.

    Article  MATH  Google Scholar 

  9. S. Hart and M. Sharir. Probabilistic temporal logics for finite and bounded models. In Proc. 16th ACM Symp. on Theory of Computing, pages 1–13, 1984.

    Google Scholar 

  10. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

    Google Scholar 

  11. B. Jonsson, C. Ho-Stuart, and Wang Yi. Testing and refinement for nondeterministic and probabilistic processes. In Langmaack, de Roever, and Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 418–430. Springer Verlag, 1994.

    Chapter  Google Scholar 

  12. B. Jonsson and Wang Yi. Compositional testing preorders for probabilistic processes. In Proc. 10th IEEE Int. Symp. on Logic in Computer Science, pages 431–441, 1995.

    Google Scholar 

  13. D. Kozen. A probabilistic pdl. In Proc. 15th ACM Symp. on Theory of Computing, pages 291–297, 1983.

    Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  15. Gavin Lowe. Probabilities and Priorities in Timed CSP. D.Phil thesis, Oxford, 1993.

    Google Scholar 

  16. Z. Manna and A. Pnueli. The anchored version of the temporal framework. In de Bakker, de Roever, and Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 201–284. Springer Verlag, 1989

    Chapter  Google Scholar 

  17. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  18. M.K. Molloy. Performance analysis using stochastic Petri nets. IEEE Trans. on Computers, C-31(9):913–917, Sept. 1982.

    Article  Google Scholar 

  19. G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark, 1981.

    Google Scholar 

  20. A. Pnueli and L. Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing, 1(1):53–72, 1986.

    Article  MATH  Google Scholar 

  21. S. Purushothaman and P.A. Subrahmanyam. Reasoning about probabilistic behavior in concurrent systems. IEEE Trans. on Software Engineering, SE-13(6):740–745, June 1989.

    Article  Google Scholar 

  22. M.O. Rabin. Probabilistic automata. Information and Control, 6:230–245, 1963.

    Article  MATH  Google Scholar 

  23. R. Segala. A compositional trace-based semantics for probabilistic automata. In Proc. CONCUR’ 95, 6th Int. Conf. on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 234–248. Springer Verlag, 1995.

    Chapter  Google Scholar 

  24. R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. In Jonsson and Parrow, editors, Proc. CONCUR’ 94, 5th Int. Conf. on Concurrency Theory, number 836 in Lecture Notes in Computer Science, pages 481–496. Springer Verlag, 1994.

    Chapter  Google Scholar 

  25. R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250–273, 1995.

    MathSciNet  MATH  Google Scholar 

  26. R. van Glabbeek, S.A. Smolka, B. Steffen, and C. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proc. 5th IEEE Int. Symp. on Logic in Computer Science, pages 130–141, 1990.

    Google Scholar 

  27. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st IEEE Int. Symp. on Logic in Computer Science, pages 332–344, June 1986.

    Google Scholar 

  28. M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. 26th Annual Symp. Foundations of Computer Science, pages 327–338, 1985.

    Google Scholar 

  29. S.-H. Wu, S.A. Smolka, and E.W. Stark. Composition and behaviors of probabilistic I/O-Automata. In Jonsson and Parrow, editors, Proc. CONCUR’ 94, 5th Int. Conf. on Concurrency Theory, number 836 in Lecture Notes in Computer Science, pages 513–528. Springer Verlag, 1994.

    Chapter  Google Scholar 

  30. Wang Yi. Algebraic reasoning for real-time probabilistic processes with uncertain information. In Langmaack, de Roever, and Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 680–693. Springer Verlag, 1994.

    Chapter  Google Scholar 

  31. Wang Yi and K. Larsen. Testing probabilistic and nondeterministic processes. In Protocol Specification, Testing, and Verification XII, 1992.

    Google Scholar 

  32. S. Yuen, R. Cleaveland, Z. Dayar, and S.A. Smolka. Fully abstract characterizations of testing preorders for probabilistic processes. In Jonsson and Parrow, editors, Proc. CONCUR’ 94, 5th Int. Conf. on Concurrency Theory, number 836 in Lecture Notes in Computer Science, pages 497–512. Springer Verlag, 1994

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Systems, Uppsala University, Box 325, S-751 05, Uppsala, Sweden

    Bengt Jonsson & Wang Yi

Authors
  1. Bengt Jonsson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wang Yi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Lehrstuhl für Informatik, University of Erlangen-Nürnberg, Martensstr. 3, D-91058, Erlangen, Germany

    Joost-Pieter Katoen

  2. Formal Methods and Tools Group, University of Twente, P.O. Box 217, 7500 AE, Enschede, The Netherlands

    Joost-Pieter Katoen

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jonsson, B., Yi, W. (1999). Fully Abstract Characterization of Probabilistic May Testing. In: Katoen, JP. (eds) Formal Methods for Real-Time and Probabilistic Systems. ARTS 1999. Lecture Notes in Computer Science, vol 1601. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48778-6_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-48778-6_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66010-1

  • Online ISBN: 978-3-540-48778-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation