Advertisement

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.

Keywords

Model Check Markov Decision Process Label Transition System Discrete Time Markov Chain Step Condition 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Ahuja, R.K., Magnanti, T.J., Orlin, J.B.: Network Flows: Theory, Algorithms, and Applications. Prentice Hall (1993)Google Scholar
  2. 2.
    Andova, S., Willemse, T.A.C.: Branching bisimulation for probabilistic systems: Characteristics and decidability. TCS 356(3), 325–355 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 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)MathSciNetCrossRefGoogle Scholar
  4. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 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)CrossRefzbMATHGoogle Scholar
  6. 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)CrossRefGoogle Scholar
  7. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)Google Scholar
  9. 9.
    Baier, C., Katoen, J.P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. I&C 200(2), 149–214 (2005)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Bellman, R.: A Markovian decision process. Indiana University Mathematics Journal 6, 679–684 (1957)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Bertsekas, D.P.: Dynamic Programming and Optimal Control. Athena Scientific (2005)Google Scholar
  12. 12.
    Bertsimas, D., Tsitsiklis, J.N.: Introduction to Linear Optimization. Athena Scientific (1997)Google Scholar
  13. 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)CrossRefGoogle Scholar
  14. 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)CrossRefGoogle Scholar
  15. 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)CrossRefGoogle Scholar
  16. 16.
    Deng, Y.: Axiomatisations and Types for Probabilistic and Mobile Processes. Ph.D. thesis, École des Mines de Paris (2005)Google Scholar
  17. 17.
    Deng, Y., Hennessy, M.: On the semantics of Markov automata. I&C 222, 139–168 (2012)MathSciNetzbMATHGoogle Scholar
  18. 18.
    Desharnais, J.: Labelled Markov Processes. Ph.D. thesis, McGill University (1999)Google Scholar
  19. 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)CrossRefGoogle Scholar
  20. 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)CrossRefGoogle Scholar
  21. 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. 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)CrossRefGoogle Scholar
  23. 23.
    Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351 (2010)Google Scholar
  24. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Goldberg, A.V., Tarjan, R.E.: A new approach to the maximum-flow problem. J. ACM 35(4), 921–940 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)CrossRefzbMATHGoogle Scholar
  27. 27.
    Hashemi, V., Hermanns, H., Turrini, A.: On the efficiency of deciding probabilistic automata weak bisimulation. ECEASST 66 (2013)Google Scholar
  28. 28.
    Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  29. 29.
    Hermanns, H., Turrini, A.: Deciding probabilistic automata weak bisimulation in polynomial time. In: FSTTCS, pp. 435–447 (2012)Google Scholar
  30. 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)CrossRefGoogle Scholar
  31. 31.
    Howard, R.A.: Dynamic Programming and Markov Processes. John Wiley and Sons, Inc. (1960)Google Scholar
  32. 32.
    Howard, R.A.: Dynamic Probabilistic Systems: Semi-Markov and Decision Processes, vol. II. Dover Publications (2007)Google Scholar
  33. 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)CrossRefGoogle Scholar
  34. 34.
    Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277 (1991)Google Scholar
  35. 35.
    Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. I&C 86(1), 43–68 (1990)MathSciNetzbMATHGoogle Scholar
  36. 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)CrossRefGoogle Scholar
  37. 37.
    Knast, R.: Continuous-time probabilistic automata. Information and Control 15(4), 335–352 (1969)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing (preliminary report). In: POPL, pp. 344–352 (1989)Google Scholar
  39. 39.
    Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cleiffs (1989)Google Scholar
  40. 40.
    Milner, R.: Communicating and Mobile Systems: the π-calculus. Cambridge University Press (1999)Google Scholar
  41. 41.
    Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. on Computing 16(6), 973–989 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  42. 42.
    Peterson, M.: An Introduction to Decision Theory. Cambridge University Press (2009)Google Scholar
  43. 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)CrossRefGoogle Scholar
  44. 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. 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)CrossRefGoogle Scholar
  46. 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. 47.
    Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, MIT (1995)Google Scholar
  48. 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)CrossRefGoogle Scholar
  49. 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)CrossRefGoogle Scholar
  50. 50.
    Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nordic J. Computing 2(2), 250–273 (1995)MathSciNetzbMATHGoogle Scholar
  51. 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. 52.
    Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press (1994)Google Scholar
  53. 53.
    Todd, M.J.: The many facets of linear programming. Mathematical Programming 91(3), 417–436 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  54. 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)CrossRefGoogle Scholar
  55. 55.
    Zhang, L.: Decision Algorithm for Probabilistic Simulations. Ph.D. thesis, Saarland University (2008)Google Scholar
  56. 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)CrossRefGoogle Scholar
  57. 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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Daniel Gebler
    • 1
  • Vahid Hashemi
    • 2
    • 3
  • Andrea Turrini
    • 4
  1. 1.Department of Computer ScienceVU University AmsterdamAmsterdamThe Netherlands
  2. 2.Max Planck Institute for InformaticsSaarbrückenGermany
  3. 3.Department of Computer ScienceSaarland UniversitySaarbrückenGermany
  4. 4.State Key Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingChina

Personalised recommendations