Skip to main content

Probabilistic simulations for probabilistic processes

  • Invited Lecture
  • Conference paper
  • First Online:
CONCUR '94: Concurrency Theory

Part of the book series: Lecture Notes in Computer Science ((volume 836))

  • 105 Accesses

Abstract

Several probabilistic simulation relations for probabilistic systems are defined and evaluated according to two criteria: compositionality and preservation of “interesting” properties. Here, the interesting properties of a system are identified with those that are expressible in an untimed version of the Timed Probabilistic concurrent Computation Tree Logic (TPCTL) of Hansson. The definitions are made, and the evaluations carried out, in terms of a general labeled transition system model for concurrent probabilistic computation. The results cover weak simulations, which abstract from internal computation, as well as strong simulations, which do not.

Supported by NSF grant CCR-89-15206, and CCR-92-25124, by DARPA contracts N00014-89-J-1988 and N00014-92-J-4033, and by ONR contract N00014-91-J-1046.

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

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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. J. Aspnes and M.P. Herlihy. Fast randomized consensus using shared memory. Journal of Algorithms, 15(1):441–460, September 1990.

    Article  MathSciNet  Google Scholar 

  2. M. Ben-Or. Another advantage of free choice: completely asynchronous agreement protocols. In Proceedings of the 2 nd PODC, August 1983.

    Google Scholar 

  3. I. Christoff. Testing equivalences for probabilistic processes. Technical Report DoCS 90/22, Ph.D. Thesis, Department of Computer Science, Uppsala University, Sweden, 1990.

    Google Scholar 

  4. M. Fischer and L. Zuck. Reasoning about uncertainty in fault tolerant distributed systems. In Proceedings of the Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 331, pages 142–158, 1988.

    Google Scholar 

  5. R.J. van Glabbeek, S.A. Smolka, B. Steffen, and C.M.N. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proceedings 5 th LICS, pages 130–141. IEEE Computer Society Press, 1990.

    Google Scholar 

  6. R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). In Information Processing 89, pages 613–618. North-Holland, 1989. Full version available as Report CS-R9120, CWI, Amsterdam, 1991.

    Google Scholar 

  7. H. Hansson. Time and Probability in Formal Design of Distributed Systems. PhD thesis, Department of Computer Science, Uppsala University, 1991.

    Google Scholar 

  8. M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.

    Google Scholar 

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

    Google Scholar 

  10. B. Jonsson. Simulations between specifications of distributed systems. In Proceedings CONCUR 91, LNCS 527, pages 346–360, 1991.

    MathSciNet  Google Scholar 

  11. B. Jonsson and K. G. Larsen. Specification and refinement of probabilistic processes. In Proceedings of the 6th LICS, July 1991.

    Google Scholar 

  12. E. Kushilevitz and M. Rabin. Randomized mutual exclusion algorithms revisited. In Proceedings of the 11th PODC, pages 275–284, 1992.

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  14. D. Lehmann and M. Rabin. On the advantage of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In Proceedings of the 8th POPL pages 133–138, January 1981.

    Google Scholar 

  15. N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6th PODC, pages 137–151, Vancouver, Canada, August 1987. A full version is available as MIT Technical Report MIT/LCS/TR-387.

    Google Scholar 

  16. N.A. Lynch and F.W. Vaandrager. Forward and backward simulations for timing-based systems. In Proceedings of the REX Workshop “Real-Time: Theory in Practice”, LNCS 600, pages 397–446, 1991.

    MathSciNet  Google Scholar 

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

    Google Scholar 

  18. A. Pnueli. The temporal semantics of concurrent programs. TCS, 13:45–60, 1982.

    Article  MathSciNet  Google Scholar 

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

    Article  MATH  Google Scholar 

  20. K. Seidel. Probabilistic communicating processes. Technical Report PRG-102, Ph.D. Thesis, Programming Research Group, Oxford University Computing Laboratory, 1992.

    Google Scholar 

  21. M. Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of 26th FOCS, pages 327–338, Portland, OR, 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Bengt Jonsson Joachim Parrow

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag

About this paper

Cite this paper

Segala, R., Lynch, N. (1994). Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds) CONCUR '94: Concurrency Theory. Lecture Notes in Computer Science, vol 836. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015027

Download citation

  • DOI: https://doi.org/10.1007/BFb0015027

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58329-5

  • Online ISBN: 978-3-540-48654-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics