Skip to main content
SpringerLink
Log in

Computing Behavioral Relations for Probabilistic Concurrent Systems

  • Chapter
Book cover Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems (ROCKS 2012)

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

Abstract

Behavioral equivalences and preorders are fundamental notions to formalize indistinguishability of transition systems and provide means to abstraction and refinement. We survey a collection of models used to represent concurrent probabilistic real systems, the behavioral equivalences and preorders they are equipped with and the corresponding decision algorithms. These algorithms follow the standard refinement approach and they improve their complexity by taking advantage of the efficient algorithms developed in the optimization community to solve optimization and flow problems.

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. Ahuja, R.K., Magnanti, T.J., Orlin, J.B.: Network Flows: Theory, Algorithms, and Applications. Prentice Hall (1993)

    Google Scholar 

  2. Andova, S., Willemse, T.A.C.: Branching bisimulation for probabilistic systems: Characteristics and decidability. TCS 356(3), 325–355 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  3. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model-checking continuous-time Markov chains. ACM Transactions on Computational Logic 1(1), 162–170 (2000)

    Article  MathSciNet  Google Scholar 

  4. Baier, C., Engelen, B., Majster-Cederbaum, M.: Deciding bisimilarity and similarity for probabilistic processes. J. Computer and Systems Science 60(1), 187–231 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  5. Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29(6), 524–541 (2003)

    Article  MATH  Google Scholar 

  6. Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 119–130. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  7. Baier, C., Hermanns, H., Katoen, J.P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. TCS 345(1), 2–26 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  8. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)

    Google Scholar 

  9. Baier, C., Katoen, J.P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. I&C 200(2), 149–214 (2005)

    MathSciNet  MATH  Google Scholar 

  10. Bellman, R.: A Markovian decision process. Indiana University Mathematics Journal 6, 679–684 (1957)

    Article  MathSciNet  MATH  Google Scholar 

  11. Bertsekas, D.P.: Dynamic Programming and Optimal Control. Athena Scientific (2005)

    Google Scholar 

  12. Bertsimas, D., Tsitsiklis, J.N.: Introduction to Linear Optimization. Athena Scientific (1997)

    Google Scholar 

  13. Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  14. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  15. Crafa, S., Ranzato, F.: Probabilistic bisimulation and simulation algorithms by abstract interpretation. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 295–306. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  16. Deng, Y.: Axiomatisations and Types for Probabilistic and Mobile Processes. Ph.D. thesis, École des Mines de Paris (2005)

    Google Scholar 

  17. Deng, Y., Hennessy, M.: On the semantics of Markov automata. I&C 222, 139–168 (2012)

    MathSciNet  MATH  Google Scholar 

  18. Desharnais, J.: Labelled Markov Processes. Ph.D. thesis, McGill University (1999)

    Google Scholar 

  19. Eisentraut, C., Hermanns, H., Katoen, J.-P., Zhang, L.: A semantics for every GSPN. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 90–109. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  20. Eisentraut, C., Hermanns, H., Krämer, J., Turrini, A., Zhang, L.: Deciding bisimilarities on distributions. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 72–88. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  21. Eisentraut, C., Hermanns, H., Schuster, J., Turrini, A., Zhang, L.: The quest for minimal quotients for probabilistic automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 16–31. Springer, Heidelberg (2013)

    Google Scholar 

  22. Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 21–39. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  23. Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351 (2010)

    Google Scholar 

  24. Gallo, G., Grigoriadis, M.D., Tarjan, R.E.: A fast parametric maximum flow algorithm and applications. SIAM J. Comp. 18(1), 30–55 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  25. Goldberg, A.V., Tarjan, R.E.: A new approach to the maximum-flow problem. J. ACM 35(4), 921–940 (1988)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

  27. Hashemi, V., Hermanns, H., Turrini, A.: On the efficiency of deciding probabilistic automata weak bisimulation. ECEASST 66 (2013)

    Google Scholar 

  28. Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  29. Hermanns, H., Turrini, A.: Deciding probabilistic automata weak bisimulation in polynomial time. In: FSTTCS, pp. 435–447 (2012)

    Google Scholar 

  30. Hermanns, H., Turrini, A.: Cost preserving bisimulations for probabilistic automata. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 349–363. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  31. Howard, R.A.: Dynamic Programming and Markov Processes. John Wiley and Sons, Inc. (1960)

    Google Scholar 

  32. Howard, R.A.: Dynamic Probabilistic Systems: Semi-Markov and Decision Processes, vol. II. Dover Publications (2007)

    Google Scholar 

  33. Jansen, D.N., Song, L., Zhang, L.: Revisiting weak simulation for substochastic Markov chains. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 209–224. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  34. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277 (1991)

    Google Scholar 

  35. Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. I&C 86(1), 43–68 (1990)

    MathSciNet  MATH  Google Scholar 

  36. Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  37. Knast, R.: Continuous-time probabilistic automata. Information and Control 15(4), 335–352 (1969)

    Article  MathSciNet  MATH  Google Scholar 

  38. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing (preliminary report). In: POPL, pp. 344–352 (1989)

    Google Scholar 

  39. Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cleiffs (1989)

    Google Scholar 

  40. Milner, R.: Communicating and Mobile Systems: the π-calculus. Cambridge University Press (1999)

    Google Scholar 

  41. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. on Computing 16(6), 973–989 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  42. Peterson, M.: An Introduction to Decision Theory. Cambridge University Press (2009)

    Google Scholar 

  43. Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334–349. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  44. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, vol. (594). John Wiley & Sons, Inc. (2005)

    Google Scholar 

  45. Sack, J., Zhang, L.: A general framework for probabilistic characterizing formulae. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 396–411. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  46. Schuster, J., Siegle, M.: Markov automata: Deciding weak bisimulation by means of “non-naïvely” vanishing states. I&C (to appear, 2014), http://dx.doi.org/10.1016/j.ic.2014.02.001

  47. Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, MIT (1995)

    Google Scholar 

  48. Segala, R.: Probability and nondeterminism in operational models of concurrency. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 64–78. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  49. Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  50. Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nordic J. Computing 2(2), 250–273 (1995)

    MathSciNet  MATH  Google Scholar 

  51. Segala, R., Turrini, A.: Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models. In: QEST, pp. 44–53 (2005)

    Google Scholar 

  52. Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press (1994)

    Google Scholar 

  53. Todd, M.J.: The many facets of linear programming. Mathematical Programming 91(3), 417–436 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  54. Wolovick, N., Johr, S.: A characterization of meaningful schedulers for continuous-time Markov decision processes. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 352–367. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  55. Zhang, L.: Decision Algorithm for Probabilistic Simulations. Ph.D. thesis, Saarland University (2008)

    Google Scholar 

  56. Zhang, L., Hermanns, H.: Deciding simulations on probabilistic automata. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 207–222. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  57. Zhang, L., Hermanns, H., Eisenbrand, F., Jansen, D.N.: Flow faster: Efficient decision algorithms for probabilistic simulations. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 155–169. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, VU University Amsterdam, De Boelelaan 1081a, NL-1081 HV, Amsterdam, The Netherlands

    Daniel Gebler

  2. Max Planck Institute for Informatics, 66123, Saarbrücken, Germany

    Vahid Hashemi

  3. Department of Computer Science, Saarland University, 66123, Saarbrücken, Germany

    Vahid Hashemi

  4. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, 100190, Beijing, China

    Andrea Turrini

Authors
  1. Daniel Gebler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vahid Hashemi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andrea Turrini
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Design and Analysis of Communication Systems, University of Twente, The Netherlands

    Anne Remke

  2. Department of Computer Science, University of Twente, The Netherlands

    Mariëlle Stoelinga

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Gebler, D., Hashemi, V., Turrini, A. (2014). Computing Behavioral Relations for Probabilistic Concurrent Systems. In: Remke, A., Stoelinga, M. (eds) Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. ROCKS 2012. Lecture Notes in Computer Science, vol 8453. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45489-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-45489-3_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-45488-6

  • Online ISBN: 978-3-662-45489-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation