Testing and refinement for nondeterministic and probabilistic processes

  • Bengt Jonsson
  • Chris Ho-Stuart
  • Wang Yi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 863)


Transition systems are a basic semantic model for formal description, specification, and analysis of concurrent and distributed systems. In order to describe and analyze aspects of reliability, such as the likelihood of trace and failure, this model has been extended in various ways to handle probabilistic behavior. To use these models for specification and stepwise development of systems, it is important to develop appropriate refinement preorders. In the paper, we develop refinement preorders based on a framework of testing for a model that represents both nondeterministic and probabilistic choices as independent concepts [YL92]. Our main contribution is a notion of reward testing, and a denotational characterization of a testing preorder, which corresponds to a natural probabilistic extension of the trace model [Hoa85].


Probabilistic Choice Maximal Chain Label Transition System Probabilistic Process Trace Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Chr90]
    I. Christoff. Testing Equivalences for Probabilistic Processes. PhD thesis, Dept. of Computer Systems, Uppsala University, Sweden, Uppsala, Sweden, 1990. Available as report DoCS 90/22.Google Scholar
  2. [CSZ92]
    R. Cleaveland, S. Smolka, and A. Zwarico. Testing preorders for probabilistic processes. In Proc. ICALP '92, 1992.Google Scholar
  3. [CY88]
    C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. In Proc. 29 th Annual Symp. Foundations of Computer Science, pages 338–345, 1988.Google Scholar
  4. [dNH84]
    R. de Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.Google Scholar
  5. [GJS90]
    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
  6. [HJ89]
    H. Hansson and B. Jonsson. A framework for reasoning about time and reliability. In Proc. 10 th IEEE Real — Time Systems Symposium, S:a Monica, Ca., 1989.Google Scholar
  7. [HJ90]
    H. Hansson and B. Jonsson. A calculus for communicating systems with time and probabilities. In Proc. 11 th IEEE Real — Time Systems Symposium, Orlando, Florida, 1990.Google Scholar
  8. [Hoa85]
    C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  9. [HS84]
    S. Hart and M. Sharir. Probabilistic temporal logics for finite and bounded models. In Proc. 16 th ACM Symp. on Theory of Computing, pages 1–13, 1984.Google Scholar
  10. [JL91]
    B. Jonsson and K. Larsen. Specification and refinement of probabilistic processes. In Proc. 6 th IEEE Int. Symp. on Logic in Computer Science, Amsterdam, Holland, July 1991.Google Scholar
  11. [Koz83]
    D. Kozen. A probabilistic pdl. In Proc. 15 th A CM Symp. on Theory of Computing, pages 291–297, 1983.Google Scholar
  12. [Low93]
    Gavin Lowe. Probabilities and Priorities in Timed CSP. D. Phil thesis, Oxford, 1993.Google Scholar
  13. [LS91]
    K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Control, 94(1):1–28, 1991.Google Scholar
  14. [Mil89]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  15. [Mol82]
    M.K. Molloy. Performance analysis using stochastic petri nets. IEEE Trans. on Computers, C-31(9):913–917, Sept. 1982.Google Scholar
  16. [MP89]
    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.Google Scholar
  17. [Plo81]
    G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark, 1981.Google Scholar
  18. [PS89]
    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.Google Scholar
  19. [PZ86]
    A. Pnueli and L. Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing, 1(1):53–72, 1986.Google Scholar
  20. [Rab63]
    M.O. Rabin. Probabilistic automata. Information and Control, 6:230–245, 1963.Google Scholar
  21. [Var85]
    M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. 26 th Annual Symp. Foundations of Computer Science, pages 327–338, 1985.Google Scholar
  22. [vGSST90]
    R. van Glabbeek, S.A. Smolka, B. Steffen, and C. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proc. 5 th IEEE Int. Symp. on Logic in Computer Science, pages 130–141, 1990.Google Scholar
  23. [VW86]
    M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1 st IEEE Int. Symp. on Logic in Computer Science, pages 332–344, June 1986.Google Scholar
  24. [YL92]
    Wang Yi and K. Larsen. Testing probabilistic and nondeterministic processes. In Protocol Specification, Testing, and Verification XII, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Bengt Jonsson
    • 1
  • Chris Ho-Stuart
    • 2
  • Wang Yi
    • 1
  1. 1.Dept. of Computer SystemsUppsala UniversityUppsalaSweden
  2. 2.School of Computing ScienceQueensland University of TechnologyBrisbaneAustralia

Personalised recommendations