Model Checking Probabilistic Systems

  • Christel Baier
  • Luca de Alfaro
  • Vojtěch Forejt
  • Marta Kwiatkowska
Chapter

Abstract

The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness (see Chap.  2), and subsequently extended to also handle quantitative features, such as real time (see Chap.  29), continuous flows (see Chap.  30), as well as stochastic phenomena, where system evolution is governed by a given probability distribution. Probabilistic model checking aims to establish the correctness of probabilistic system models against quantitative probabilistic specifications, such as those capable of expressing, for example, the probability of an unsafe event occurring, expected time to termination, or expected power consumption in the start-up phase. In this chapter, we present the foundations of probabilistic model checking, focusing on finite-state Markov decision processes as models and quantitative properties expressed in probabilistic temporal logic. Markov decision processes can be thought of as a probabilistic variant of labelled transition systems in the following sense: transitions are labelled with actions, which can be chosen nondeterministically, and successor states for the chosen action are specified by means of discrete probabilistic distributions, thus specifying the probability of transiting to each successor state. To reason about expectations, we additionally annotate Markov decision processes with quantitative costs, which are incurred upon taking the selected action from a given state. Quantitative properties are expressed as formulas of the probabilistic computation tree logic (PCTL) or using linear temporal logic (LTL). We summarise the main model-checking algorithms for both PCTL and LTL, and illustrate their working through examples. The chapter ends with a brief overview of extensions to more expressive models and temporal logics, existing probabilistic model-checking tool support, and main application domains.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abdulla, P., Baier, C., Iyer, P., Jonsson, B.: Reasoning about probabilistic lossy channel systems. In: Palamidessi, C. (ed.) Proc. CONCUR’00. LNCS, vol. 1877, pp. 320–330. Springer, Heidelberg (2000) Google Scholar
  2. 2.
    Ajmone-Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley Series in Parallel Computing. Wiley, New York (1995) MATHGoogle Scholar
  3. 3.
    Aldini, A., Bernardo, M., Corradini, F.: A Process Algebraic Approach to Software Architecture Design. Springer, Heidelberg (2010) MATHGoogle Scholar
  4. 4.
    de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University, Department of Computer Science (1997) Google Scholar
  5. 5.
    de Alfaro, L., Henzinger, T.A., Jhala, R.: Compositional methods for probabilistic systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR. LNCS, vol. 2154, pp. 351–365. Springer, Heidelberg (2001) Google Scholar
  6. 6.
    de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S., Schwartzbach, M.I. (eds.) Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS). LNCS, vol. 1785, pp. 395–410. Springer, Heidelberg (2000) MATHGoogle Scholar
  7. 7.
    Ash, R., Doléans-Dade, C.: Probability and Measure Theory. Harcourt/Academic Press, San Diego (2000) MATHGoogle Scholar
  8. 8.
    Baier, C., Ciesinski, F., Größer, M.: ProbMeLa: a modeling language for communicating probabilistic systems. In: Proc. of the 2nd ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 57–66. IEEE, Piscataway (2004) Google Scholar
  9. 9.
    Baier, C., Clarke, E., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) Proc. International Colloqium on Automata, Languages and Programming (ICALP). LNCS, vol. 1256, pp. 430–440. Springer, Heidelberg (1997) Google Scholar
  10. 10.
    Baier, C., Engelen, B.: Establishing qualitative properties for probabilistic lossy channel systems: an algorithmic approach. In: Katoen, J.-P. (ed.) Intl. AMAST Workshop, ARTS. LNCS, vol. 1601, pp. 34–52. Springer, Heidelberg (1999) Google Scholar
  11. 11.
    Baier, C., Größer, M., Ciesinski, F.: Model checking linear time properties of probabilistic systems. In: Droste, M., Kuich, W., Vogler, H. (eds.) Handbook of Weighted Automata, Monographs in Theoretical Computer Science. An EATCS Series, pp. 519–570. Springer, Heidelberg (2009) Google Scholar
  12. 12.
    Baier, C., Größer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Lévy, J.J., Mayr, E., Mitchell, J. (eds.) Proc. 3rd IFIP Int. Conf. Theoretical Computer Science (TCS’06), pp. 493–5062. Kluwer Academic, Dordrecht (2004) Google Scholar
  13. 13.
    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76–85 (2010) Google Scholar
  14. 14.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008) MATHGoogle Scholar
  15. 15.
    Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11, 125–155 (1998) Google Scholar
  16. 16.
    Barnat, J., Brim, L., Černá, I., Češka, M., Tůmová, J.: ProbDiVinE-MC: multi-core LTL model checker for probabilistic systems. In: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp. 77–78. IEEE, Washington (2008) Google Scholar
  17. 17.
    Bianco, A., De Alfaro, L.: Model checking of probabilistic and non-deterministic systems. In: Thiagarajan, P.S. (ed.) Proceedings of Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995) MATHGoogle Scholar
  18. 18.
    Blahoudek, F., Kretínský, M., Strejcek, J.: Comparison of LTL to deterministic Rabin automata translators. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—Proceedings of the 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. LNCS, vol. 8312, pp. 164–172. Springer, Heidelberg (2013) MATHGoogle Scholar
  19. 19.
    Bogdoll, J., Fioriti, L.M.F., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE. LNCS, vol. 6722, pp. 59–74. Springer, Heidelberg (2011) Google Scholar
  20. 20.
    Bohnenkamp, H., D’Argenio, P., Hermanns, H., Katoen, J.P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812–830 (2006) Google Scholar
  21. 21.
    Bolch, G., Greiner, S., de Meer, H., Trivedi, K.: Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications. Wiley-Interscience, New York (1998) MATHGoogle Scholar
  22. 22.
    Brázdil, T.: Verification of probabilistic recursive sequential programs. Ph.D. thesis, Masaryk University (2007) Google Scholar
  23. 23.
    Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., Kučera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. In: Proceedings of LICS’11, pp. 33–42. IEEE, Piscataway (2011) Google Scholar
  24. 24.
    Brázdil, T., Brožek, V., Forejt, V., Kučera, A.: Stochastic games with branching-time winning objectives. In: 21th IEEE Symp. Logic in Computer Science (LICS 2006), pp. 349–358. IEEE, Piscataway (2006) Google Scholar
  25. 25.
    Brázdil, T., Chatterjee, K., Chmelík, M., Forejt, V., Křetínský, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J. (eds.) Proc. 12th International Symposium on Automated Technology for Verification and Analysis (ATVA’14). LNCS, vol. 8837, pp. 98–114. Springer, Heidelberg (2014) MATHGoogle Scholar
  26. 26.
    Brázdil, T., Esparza, J., Kiefer, S., Kučera, A.: Analyzing probabilistic pushdown automata. Form. Methods Syst. Des. 43(2), 124–163 (2013) MATHGoogle Scholar
  27. 27.
    Brázdil, T., Forejt, V., Kučera, A.: Controller synthesis and verification for Markov decision processes with qualitative branching time objectives. In: Aceto, L., Damgård, I., Goldberg, L., Halldórsson, M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) Proc. 35th Int. Colloq. Automata, Languages and Programming, Part II (ICALP’08). LNCS, vol. 5126, pp. 148–159. Springer, Heidelberg (2008) Google Scholar
  28. 28.
    Brázdil, T., Hermanns, H., Krčál, J., Křetínský, J., Řehák, V.: Verification of open interactive Markov chains. In: D’Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) FSTTCS. LIPIcs, vol. 18, pp. 474–485. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, Dagstuhl (2012) Google Scholar
  29. 29.
    Brim, L., Češka, M., Dražan, S., Šafránek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina and Veith [96], pp. 107–123 Google Scholar
  30. 30.
    Cardelli, L.: Artificial biochemistry. In: Condon, A., Harel, D., Kok, J.N., Salomaa, A., Winfree, E. (eds.) Algorithmic Bioprocesses. Natural Computing Series, pp. 429–462. Springer, Heidelberg (2009) Google Scholar
  31. 31.
    Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) Proc. 14th Int. Conf. Concurrency Theory (CONCUR’02). LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002) Google Scholar
  32. 32.
    Chatterjee, K., Gaiser, A., Křetínský, J.: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina and Veith [13, 21, 61], pp. 559–575 Google Scholar
  33. 33.
    Chatterjee, K., Jurdzinski, M., Henzinger, T.: Simple stochastic parity games. In: Baaz, M., Makowsky, J.A. (eds.) Proceedings of the International Conference for Computer Science Logic (CSL). LNCS, vol. 2803, pp. 100–113. Springer, Heidelberg (2003) Google Scholar
  34. 34.
    Chatterjee, K., Jurdzinski, M., Henzinger, T.: Quantitative stochastic parity games. In: Munro, J.I. (ed.) Proceedings of the Annual Symposium on Discrete Algorithms (SODA), pp. 121–130. SIAM, Philadelphia (2004) Google Scholar
  35. 35.
    Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: Durand, B., Thomas, W. (eds.) STACS. LNCS, vol. 3884, pp. 325–336. Springer, Heidelberg (2006) Google Scholar
  36. 36.
    Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Form. Methods Syst. Des. 43(1), 61–92 (2013) MATHGoogle Scholar
  37. 37.
    Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE’13), pp. 85–92. IEEE, Piscataway (2013) Google Scholar
  38. 38.
    Ciesinski, F., Baier, C.: LiQuor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. QEST 2007, pp. 131–132. IEEE, Piscataway (2007) Google Scholar
  39. 39.
    Ciocchetta, F., Hillston, J.: Bio-PEPA: a framework for the modelling and analysis of biological systems. Theor. Comput. Sci. 410(33–34), 3065–3084 (2009) MathSciNetMATHGoogle Scholar
  40. 40.
    Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995) MathSciNetMATHGoogle Scholar
  41. 41.
    Daniele, M., Giunchiglia, F., Vardi, M.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D. (eds.) Proc. International Conference on Computer Aided Verification (CAV). LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999) Google Scholar
  42. 42.
    Delahaye, B., Caillaud, B., Legay, A.: Probabilistic contracts: a compositional reasoning methodology for the design of stochastic systems. In: Proc. 10th Int. Conf. Application of Concurrency to System Design (ACSD’10), pp. 223–232. IEEE, Piscataway (2010) Google Scholar
  43. 43.
    Delahaye, B., Katoen, J.P., Larsen, K., Legay, A., Pedersen, M., Sher, F., Wasowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D.A. (eds.) 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol. 6538, pp. 324–339. Springer, Heidelberg (2011) MATHGoogle Scholar
  44. 44.
    Donaldson, A., Miller, A.: Symmetry reduction for probabilistic model checking using generic representatives. In: Graf, S., Zhang, W. (eds.) Proc. 4th Int. Symp. Automated Technology for Verification and Analysis (ATVA’06). LNCS, vol. 4218, pp. 9–23. Springer, Heidelberg (2006) Google Scholar
  45. 45.
    Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of Bluetooth device discovery. Int. J. Softw. Tools Technol. Transf. 8(6), 621–632 (2006) Google Scholar
  46. 46.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, pp. 996–1072. Elsevier, Amsterdam (1990). Chap. 14 Google Scholar
  47. 47.
    Esparza, J., Křetínský, J.: From LTL to deterministic automata: a Safraless compositional approach. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification—Proceedings of the 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18–22, 2014. LNCS, vol. 8559, pp. 192–208. Springer, Heidelberg (2014) Google Scholar
  48. 48.
    Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4) (2008) Google Scholar
  49. 49.
    Etessami, K., Yannakakis, M.: Model checking of recursive probabilistic systems. ACM Trans. Comput. Log. 13(2), 1–40 (2012) MathSciNetMATHGoogle Scholar
  50. 50.
    Feller, W.: An Introduction to Probability Theory and Its Applications. Wiley, New York (1950) MATHGoogle Scholar
  51. 51.
    Feng, L., Kwiatkowska, M., Parker, D.: Compositional verification of probabilistic systems using learning. In: Proc. 7th Int. Conf. Quantitative Evaluation of Systems (QEST’10), pp. 133–142. IEEE, Piscataway (2010) Google Scholar
  52. 52.
    Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) Formal Methods for Eternal Networked Software Systems (SFM’11). LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011) Google Scholar
  53. 53.
    Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P., Leino, K. (eds.) Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’11). LNCS, vol. 6605, pp. 112–127. Springer, Heidelberg (2011) MATHGoogle Scholar
  54. 54.
    Fujita, M., McGeer, P.C., Yang, J.C.Y.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form. Methods Syst. Des. 10(2/3), 149–169 (1997) Google Scholar
  55. 55.
    van Glabbeek, R., Smolka, S.A., Steffen, B., Tofts, C.M.N.: Reactive, generative, and stratified models of probabilistic processes. In: Proc. 5th Annual Symposium on Logic in Computer Science (LICS), pp. 130–141. IEEE, Piscataway (1990) Google Scholar
  56. 56.
    Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. LNCS, vol. 2500. Springer, Heidelberg (2002) Google Scholar
  57. 57.
    Hahn, E., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) 22nd International Conference on Computer Aided Verification (CAV). LNCS, vol. 6174, pp. 660–664. Springer, Heidelberg (2010) Google Scholar
  58. 58.
    Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: abstraction refinement for infinite probabilistic models. In: Esparza, J., Majumdar, R. (eds.) Proc. TACAS 2010. LNCS, vol. 6015, pp. 353–357. Springer, Heidelberg (2010) Google Scholar
  59. 59.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994) MATHGoogle Scholar
  60. 60.
    Hartonas-Garmhausen, V., Campos, S., Clarke, E.: ProbVerus: probabilistic symbolic model checking. In: Katoen, J. (ed.) 5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems (ARTS). LNCS, vol. 1601, pp. 96–110. Springer, Heidelberg (1999) Google Scholar
  61. 61.
    Haverkort, B.: Performance of Computer Communication Systems: A Model-Based Approach. Wiley, Chichester (1998) Google Scholar
  62. 62.
    Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theor. Comput. Sci. 319(3), 239–257 (2008) MathSciNetMATHGoogle Scholar
  63. 63.
    Henzinger, T.A., Mateescu, M.: Propagation models for computing biochemical reaction networks. In: Fages, F. (ed.) Proc. CMSB’11, pp. 1–3. ACM, New York (2011) Google Scholar
  64. 64.
    Hermanns, H., Katoen, J.P.: The how and why of interactive Markov chains. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO’09. LNCS, vol. 6286, pp. 311–337. Springer, Heidelberg (2010) Google Scholar
  65. 65.
    Hermanns, H., Segala, R. (eds.): Proc. 2nd Joint Int. Workshop Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV). LNCS, vol. 2399. Springer, Heidelberg (2002) MATHGoogle Scholar
  66. 66.
    Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1), 96–112 (2005) MathSciNetMATHGoogle Scholar
  67. 67.
    Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proc. 12th Annual IEEE Symposium on Logic in Computer Science (LICS’97), pp. 111–122. IEEE, Piscataway (1997) Google Scholar
  68. 68.
    Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60–87 (1990) MathSciNetMATHGoogle Scholar
  69. 69.
    Iyer, P., Narasimha, M.: Probabilistic lossy channel systems. In: Bidoit, M., Dauchet, M. (eds.) TAPSOFT ’97: Theory and Practice of Software Development. LNCS, vol. 1214, pp. 667–681. Springer, Heidelberg (1997) Google Scholar
  70. 70.
    Jeannet, B., d’Argenio, P.R., Larsen, K.G.: Rapture: A tool for verifying Markov Decision Processes. In: Tools Day’02, Technical Report. Masaryk University, Brno (2002) Google Scholar
  71. 71.
    Jonsson, B., Larsen, K., Yi, W.: Probabilistic extensions of process algebras. In: Bergstra, J.A., Pomse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 685–710. Elsevier, Amsterdam (2001) MATHGoogle Scholar
  72. 72.
    Karloff, H.: Linear Programming. Birkhäuser, Boston (1991) MATHGoogle Scholar
  73. 73.
    Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N., Müller-Olm, M. (eds.) Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’09). LNCS, vol. 5403, pp. 182–197. Springer, Heidelberg (2009) Google Scholar
  74. 74.
    Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Form. Methods Syst. Des. 36(3), 246–280 (2010) MATHGoogle Scholar
  75. 75.
    Kemeny, J., Snell, J.: Finite Markov Chains. Van Nostrand, Princeton (1960) MATHGoogle Scholar
  76. 76.
    Komárková, Z., Křetínský, J.: Rabinizer 3: Safraless translation of LTL to small deterministic automata. In: Cassez, F., Raskin, J. (eds.) Automated Technology for Verification and Analysis—Proceedings of the 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3–7, 2014. LNCS, vol. 8837, pp. 235–241. Springer, Heidelberg (2014) MATHGoogle Scholar
  77. 77.
    Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall, London (1995) MATHGoogle Scholar
  78. 78.
    Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) Proc. of the 18th International Conference on Computer Aided Verification (CAV). LNCS, vol. 4144, pp. 234–248. Springer, Heidelberg (2006) Google Scholar
  79. 79.
    Kwiatkowska, M., Norman, G., Parker, D.: Using probabilistic model checking in systems biology. ACM SIGMETRICS Perform. Eval. Rev. 35(4), 14–21 (2008) Google Scholar
  80. 80.
    Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) Proc. 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS’09). LNCS, vol. 5813, pp. 212–227. Springer, Heidelberg (2009) Google Scholar
  81. 81.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV’11). LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011) Google Scholar
  82. 82.
    Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, R.M.J. (ed.) 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 6015, pp. 23–37 (2010) Google Scholar
  83. 83.
    Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38–65 (2013) MathSciNetMATHGoogle Scholar
  84. 84.
    Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282, 101–150 (2002) MathSciNetMATHGoogle Scholar
  85. 85.
    Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) Proc. 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM/PROBMIV’02). LNCS, vol. 2399, pp. 169–187. Springer, Heidelberg (2002) Google Scholar
  86. 86.
    Kwiatkowska, M., Parker, D., Qu, H.: Incremental quantitative verification for Markov decision processes. In: Proc. IEEE/IFIP International Conference on Dependable Systems and Networks (DSN-PDS’11), pp. 359–370. IEEE, Piscataway (2011) Google Scholar
  87. 87.
    Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991) MathSciNetMATHGoogle Scholar
  88. 88.
    Lassaigne, R., Peyronnet, S.: Approximate verification of probabilistic systems. In: [62], pp. 213–214 (2002) Google Scholar
  89. 89.
    Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large Markov decision processes. In: Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC ’12, pp. 1314–1319. ACM, New York (2012) Google Scholar
  90. 90.
    Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996) MATHGoogle Scholar
  91. 91.
    McIver, A., Morgan, C.: Games, probability and the quantitative \(\mu\)-calculus qM\(\mu\). In: Baaz, M., Voronkov, A. (eds.) Proc. LPAR 2002. LNCS, vol. 2514, pp. 292–310. Springer, Heidelberg (2002) Google Scholar
  92. 92.
    Mikeev, L., Sandmann, W., Wolf, V.: Numerical approximation of rare event probabilities in biochemically reacting systems. In: Gupta, A., Henzinger, T.A. (eds.) Proc. CMSB 2013. LNCS, vol. 8130, pp. 5–18. Springer, Heidelberg (2013) Google Scholar
  93. 93.
    Mio, M.: Probabilistic modal \(\mu\)-calculus with independent product. Log. Methods Comput. Sci. 8(4), 1–36 (2012) MathSciNetMATHGoogle Scholar
  94. 94.
    Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., Gupta, R.: Using probabilistic model checking for dynamic power management. In: Leuschel, M., Gruner, S., Presti, S.L. (eds.) Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS’03), Technical Report DSSE-TR-2003-2, University of Southampton, pp. 202–215 (2003) Google Scholar
  95. 95.
    Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Form. Methods Syst. Des. 43(2), 164–190 (2013) MATHGoogle Scholar
  96. 96.
    Norris, J.R.: Markov chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (1998) MATHGoogle Scholar
  97. 97.
    Pnueli, A., Zuck, L.: Probabilistic verification by tableaux. In: Proc. Annual Symposium on Logic in Computer Science (LICS), pp. 322–331. IEEE, Piscataway (1986) Google Scholar
  98. 98.
    PRISM web site. www.prismmodelchecker.org. Accessed 20 August 2013
  99. 99.
    Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994) MATHGoogle Scholar
  100. 100.
    Schrijver, A.: Combinatorial Optimization: Polyhedra and Efficiency. Springer, Heidelberg (2003) MATHGoogle Scholar
  101. 101.
    Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology (1995) Google Scholar
  102. 102.
    Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) Proc. CONCUR ’94. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994) Google Scholar
  103. 103.
    Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3920, pp. 394–410. Springer, Heidelberg (2006) Google Scholar
  104. 104.
    Sharygina, N., Veith, H. (eds.): Computer Aided Verification—Proceedings of the 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. LNCS, vol. 8044. Springer, Heidelberg (2013) MATHGoogle Scholar
  105. 105.
    Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. 26th IEEE Symposium on Foundations of Computer Science (FOCS), pp. 327–338. IEEE, Piscataway (1985) Google Scholar
  106. 106.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symposium on Logic in Computer Science (LICS’86), pp. 332–345. IEEE, Piscataway (1986) Google Scholar
  107. 107.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994) MathSciNetMATHGoogle Scholar
  108. 108.
    Younes, H., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transf. 8(3), 216–228 (2006) MATHGoogle Scholar
  109. 109.
    Younes, H., Simmons, R.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) Proc. 14th International Conference on Computer Aided Verification (CAV). LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002) Google Scholar
  110. 110.
    Zhang, L., Hermanns, H.: Deciding simulations on probabilistic automata. In: Namjoshi, K., Yoneda, T., Higashino, T., Okamura, Y. (eds.) Proc. 5th Int. Symp. Automated Technology for Verification and Analysis (ATVA’07). LNCS, vol. 4762, pp. 207–222. Springer, Heidelberg (2007) Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Christel Baier
    • 1
  • Luca de Alfaro
    • 2
  • Vojtěch Forejt
    • 3
  • Marta Kwiatkowska
    • 3
  1. 1.Technische Universität DresdenDresdenGermany
  2. 2.University of California, Santa CruzSanta CruzUSA
  3. 3.University of OxfordOxfordUK

Personalised recommendations