Model checking probabilistic systems. (English) Zbl 1392.68227
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 963-999 (2018).
Summary: The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness (see Chapter 2 [Zbl 1392.68263]), and subsequently extended to also handle quantitative features, such as real time (see Chapter 29 [Zbl 1392.68235]), continuous flows (see Chapter 30 [Zbl 1392.68246]), 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.
For the entire collection see [Zbl 1390.68001].
For the entire collection see [Zbl 1390.68001].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
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) · Zbl 0999.68145 |
| [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) · Zbl 0843.68080 |
| [3] | 3. Aldini, A., Bernardo, M., Corradini, F.: A Process Algebraic Approach to Software Architecture Design. Springer, Heidelberg (2010) · Zbl 1255.68004 |
| [4] | 4. de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University, Department of Computer Science (1997) |
| [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) · Zbl 1006.68083 |
| [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) · Zbl 0960.68109 |
| [7] | 7. Ash, R., Doléans-Dade, C.: Probability and Measure Theory. Harcourt/Academic Press, San Diego (2000) · Zbl 0944.60004 |
| [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) |
| [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) · Zbl 1401.68180 |
| [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) |
| [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) · Zbl 1484.68095 |
| [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) · Zbl 1073.93037 |
| [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) |
| [14] | 14. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008) · Zbl 1179.68076 |
| [15] | 15. Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11, 125-155 (1998) · Zbl 1448.68285 |
| [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) |
| [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) · Zbl 1354.68167 |
| [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) · Zbl 1406.68050 |
| [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) |
| [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) |
| [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) · Zbl 0917.60008 |
| [22] | 22. Brázdil, T.: Verification of probabilistic recursive sequential programs. Ph.D. thesis, Masaryk University (2007) |
| [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) |
| [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) |
| [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) · Zbl 1448.68290 |
| [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) · Zbl 1291.68226 |
| [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) · Zbl 1155.68427 |
| [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) · Zbl 1354.68170 |
| [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 |
| [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) |
| [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) · Zbl 1012.68127 |
| [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 |
| [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) · Zbl 1116.68493 |
| [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) · Zbl 1318.91027 |
| [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) · Zbl 1136.90498 |
| [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) · Zbl 1291.68252 |
| [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) |
| [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) |
| [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) · Zbl 1173.68041 |
| [40] | 40. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857-907 (1995) · Zbl 0885.68109 |
| [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) · Zbl 1046.68588 |
| [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) · Zbl 1210.93068 |
| [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) · Zbl 1317.68095 |
| [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) · Zbl 1161.68564 |
| [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) |
| [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 · Zbl 0900.03030 |
| [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) · Zbl 1368.68233 |
| [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) · Zbl 1161.68565 |
| [49] | 49. Etessami, K., Yannakakis, M.: Model checking of recursive probabilistic systems. ACM Trans. Comput. Log. 13(2), 1-40 (2012) · Zbl 1351.68159 |
| [50] | 50. Feller, W.: An Introduction to Probability Theory and Its Applications. Wiley, New York (1950) · Zbl 0039.13201 |
| [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) |
| [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) · Zbl 1315.68177 |
| [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) · Zbl 1315.68177 |
| [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) |
| [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) |
| [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) |
| [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) |
| [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) |
| [59] | 59. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512-535 (1994) · Zbl 0820.68113 |
| [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) |
| [61] | 61. Haverkort, B.: Performance of Computer Communication Systems: A Model-Based Approach. Wiley, Chichester (1998) |
| [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) · Zbl 1133.68043 |
| [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) |
| [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) · Zbl 1312.68152 |
| [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) |
| [66] | 66. Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1), 96-112 (2005) · Zbl 1080.68063 |
| [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) |
| [68] | 68. Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60-87 (1990) · Zbl 0705.68020 |
| [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) |
| [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) |
| [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) · Zbl 1062.68081 |
| [72] | 72. Karloff, H.: Linear Programming. Birkhäuser, Boston (1991) · Zbl 0748.90040 |
| [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) · Zbl 1206.68090 |
| [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) · Zbl 1233.90276 |
| [75] | 75. Kemeny, J., Snell, J.: Finite Markov Chains. Van Nostrand, Princeton (1960) · Zbl 0089.13704 |
| [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) · Zbl 1448.68268 |
| [77] | 77. Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall, London (1995) · Zbl 0866.60004 |
| [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) · Zbl 1188.68194 |
| [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) |
| [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) · Zbl 1262.68125 |
| [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) |
| [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) · Zbl 1284.68406 |
| [83] | 83. Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38-65 (2013) · Zbl 1277.68138 |
| [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) · Zbl 1050.68094 |
| [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) · Zbl 1065.68583 |
| [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) |
| [87] | 87. Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1-28 (1991) · Zbl 0756.68035 |
| [88] | 88. Lassaigne, R., Peyronnet, S.: Approximate verification of probabilistic systems. In: [62], pp. 213-214 (2002) · Zbl 1065.68584 |
| [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) |
| [90] | 90. Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996) · Zbl 0877.68061 |
| [91] | 91. McIver, A., Morgan, C.: Games, probability and the quantitative |
| [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) |
| [93] | 93. Mio, M.: Probabilistic modal · Zbl 1326.68202 |
| [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) · Zbl 1080.68601 |
| [95] | 95. Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Form. Methods Syst. Des. 43(2), 164-190 (2013) · Zbl 1291.68265 |
| [96] | 96. Norris, J.R.: Markov chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (1998) · Zbl 0938.60058 |
| [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) · Zbl 0598.68019 |
| [98] | 98. PRISM web site. |
| [99] | 99. Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994) · Zbl 0829.90134 |
| [100] | 100. Schrijver, A.: Combinatorial Optimization: Polyhedra and Efficiency. Springer, Heidelberg (2003) · Zbl 1041.90001 |
| [101] | 101. Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology (1995) |
| [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) · Zbl 0839.68067 |
| [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) · Zbl 1180.68179 |
| [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) · Zbl 1268.68032 |
| [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) |
| [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) |
| [107] | 107. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1-37 (1994) · Zbl 0827.03009 |
| [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) · Zbl 1126.68490 |
| [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) · Zbl 1010.68513 |
| [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) · Zbl 1141.68443 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
