{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,7]],"date-time":"2025-05-07T04:13:48Z","timestamp":1746591228669,"version":"3.40.5"},"publisher-location":"Berlin, Heidelberg","reference-count":59,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662454886"},{"type":"electronic","value":"9783662454893"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-45489-3_2","type":"book-chapter","created":{"date-parts":[[2014,11,3]],"date-time":"2014-11-03T10:42:42Z","timestamp":1415011362000},"page":"26-66","source":"Crossref","is-referenced-by-count":1,"title":["A Tutorial on Interactive Markov Chains"],"prefix":"10.1007","author":[{"given":"Florian","family":"Arnold","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Gebler","sequence":"additional","affiliation":[]},{"given":"Dennis","family":"Guck","sequence":"additional","affiliation":[]},{"given":"Hassan","family":"Hatefi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University (1997)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"de Alfaro, L.: How to specify and verify the long-run average behavior of probabilistic systems. In: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 454\u2013465. IEEE (1998)","DOI":"10.1109\/LICS.1998.705679"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"CONCUR\u201999. Concurrency Theory","author":"L. Alfaro de","year":"1999","unstructured":"de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 66\u201381. Springer, Heidelberg (1999)"},{"key":"2_CR4","unstructured":"Ash, R., Dol\u00e9ans-Dade, C.: Probability & Measure Theory. Academic Press (2000)"},{"issue":"6","key":"2_CR5","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2005.07.022","volume":"345","author":"C. Baier","year":"2005","unstructured":"Baier, C., Hermanns, H., Katoen, J.P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science\u00a0345(1), 2\u201326 (2005)","journal-title":"Theoretical Computer Science"},{"key":"2_CR7","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking, vol. 950. MIT Press (2008)"},{"issue":"3","key":"2_CR8","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1287\/moor.16.3.580","volume":"16","author":"D.P. Bertsekas","year":"1991","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Mathematics of Operations Research\u00a016(3), 580\u2013595 (1991)","journal-title":"Mathematics of Operations Research"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabalistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"issue":"2","key":"2_CR10","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1109\/TSE.2008.102","volume":"35","author":"E. B\u00f6de","year":"2009","unstructured":"B\u00f6de, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Rakow, J., Wimmer, R., Becker, B.: Compositional dependability evaluation for STATEMATE. IEEE Transactions on Software Engineering\u00a035(2), 274\u2013292 (2009)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/TR.2005.859228","volume":"55","author":"H. Boudali","year":"2005","unstructured":"Boudali, H., Dugan, J.B.: A Bayesian network reliability modeling and analysis framework. IEEE Transactions on Reliability\u00a055, 86\u201397 (2005)","journal-title":"IEEE Transactions on Reliability"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: Dynamic fault tree analysis using input\/output interactive Markov chains. In: Proceedings of the 37th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 708\u2013717 (2007)","DOI":"10.1109\/DSN.2007.37"},{"issue":"5","key":"2_CR13","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M. Bozzano","year":"2011","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. The Computer Journal\u00a054(5), 754\u2013775 (2011)","journal-title":"The Computer Journal"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.entcs.2005.12.108","volume":"162","author":"M. Bravetti","year":"2006","unstructured":"Bravetti, M., Hermanns, H., Katoen, J.P.: YMCA: Why Markov chain algebra? Electronic Notes in Theoretical Computer Science (ENTCS)\u00a0162, 107\u2013112 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science (ENTCS)"},{"key":"2_CR15","unstructured":"Br\u00e1zdil, T., Hermanns, H., Krc\u00e1l, J., Kret\u00ednsk\u00fd, J., Reh\u00e1k, V.: Verification of open interactive Markov chains. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pp. 474\u2013485 (2012)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-22110-1_19","volume-title":"Computer Aided Verification","author":"P. Buchholz","year":"2011","unstructured":"Buchholz, P., Hahn, E.M., Hermanns, H., Zhang, L.: Model checking algorithms for CTMDPs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 225\u2013242. Springer, Heidelberg (2011)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: Proceedings of the Twenty-second Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 1318\u20131336. SIAM (2011)","DOI":"10.1137\/1.9781611973082.101"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-16561-0_18","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"N. Coste","year":"2010","unstructured":"Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten Years of Performance Evaluation for Concurrent Systems Using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol.\u00a06416, pp. 128\u2013142. Springer, Heidelberg (2010)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-02658-4_18","volume-title":"Computer Aided Verification","author":"N. Coste","year":"2009","unstructured":"Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 204\u2013218. Springer, Heidelberg (2009)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Crouzen, P., Hermanns, H.: Aggregation ordering for massively compositional models. In: Proceedings of the10th International Conference onApplication of Concurrency to System Design (ACSD), pp. 171\u2013180. IEEE (June 2010)","DOI":"10.1109\/ACSD.2010.28"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-85361-9_25","volume-title":"CONCUR 2008 - Concurrency Theory","author":"P. Crouzen","year":"2008","unstructured":"Crouzen, P., Hermanns, H., Zhang, L.: On the minimisation of acyclic models. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol.\u00a05201, pp. 295\u2013309. Springer, Heidelberg (2008)"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-15375-4_3","volume-title":"CONCUR 2010 - Concurrency Theory","author":"C. Eisentraut","year":"2010","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 21\u201339. Springer, Heidelberg (2010)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 342\u2013351. IEEE (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Esteve, M.A., Katoen, J.P., Nguyen, V.Y., Postma, B., Yushtein, Y.: Formal correctness, safety, dependability, and performance analysis of a satellite. In: Proceedings of the 34th International Conference on Software Engineering (ICSE), pp. 1022\u20131031. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"2_CR25","unstructured":"Giacalone, A., Jou, C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods, pp. 443\u2013458 (1990)"},{"key":"2_CR26","unstructured":"Guck, D.: Quantitative Analysis of Markov Automata. Master\u2019s thesis, RWTH Aachen University (2012)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-642-28891-3_4","volume-title":"NASA Formal Methods","author":"D. Guck","year":"2012","unstructured":"Guck, D., Han, T., Katoen, J.-P., Neuh\u00e4u\u00dfer, M.R.: Quantitative timed analysis of interactive Markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 8\u201323. Springer, Heidelberg (2012)"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-40196-1_5","volume-title":"Quantitative Evaluation of Systems","author":"D. Guck","year":"2013","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J.-P., Timmer, M.: Modelling, reduction and analysis of Markov automata. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol.\u00a08054, pp. 55\u201371. Springer, Heidelberg (2013)"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-78929-1_18","volume-title":"Hybrid Systems: Computation and Control","author":"T. Han","year":"2008","unstructured":"Han, T., Katoen, J.-P., Mereacre, A.: Compositional modeling and minimization of time-inhomogeneous Markov chains. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol.\u00a04981, pp. 244\u2013258. Springer, Heidelberg (2008)"},{"issue":"5","key":"2_CR30","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"issue":"4","key":"2_CR31","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., Trakhtenbrot, M.B.: STATEMATE: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering\u00a016(4), 403\u2013414 (1990)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR32","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. Electronic Communications of the ECEASST 53 (2012)"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Hatefi, H., Hermanns, H.: Improving time bounded reachability computations in interactive markov chains. In: FSEN, pp. 250\u2013266 (2013)","DOI":"10.1007\/978-3-642-40213-5_16"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R., Kuntz, M., Remke, A., Roolvink, S., Stoelinga, M.: Evaluating repair strategies for a water-treatment facility using Arcade. In: Proceedings of the 40th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 419\u2013424 (2010)","DOI":"10.1109\/DSN.2010.5544290"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Hermanns, H.: Interactive Markov Chains. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45804-2"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-642-17071-3_16","volume-title":"Formal Methods for Components and Objects","author":"H. Hermanns","year":"2010","unstructured":"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 2009. LNCS, vol.\u00a06286, pp. 311\u2013338. Springer, Heidelberg (2010)"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Johr, S.: Uniformity by construction in the analysis of nondeterministic stochastic systems. In: Proceedings of the 37th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 718\u2013728 (2007)","DOI":"10.1109\/DSN.2007.96"},{"key":"2_CR38","unstructured":"Hermanns, H., Johr, S.: May we reach it? Or must we? In what time? With what probability? In: MMB, pp. 125\u2013140. VDE Verlag (2008)"},{"key":"2_CR39","unstructured":"Hermanns, H., Katoen, J.P., Meyer-Kayser, J., Siegle, M.: ETMCC: Model checking performability properties of Markov chains. In: Proceedings of the 33rd International Conference on Dependable Systems and Networks (DSN). IEEE Computer Society (2003)"},{"key":"2_CR40","unstructured":"Johr, S.: Model checking compositional Markov systems. Ph.D. thesis, Saarland University (2008)"},{"issue":"1","key":"2_CR41","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P.C. Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation\u00a086(1), 43\u201368 (1990)","journal-title":"Information and Computation"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The Ins and Outs of the probabilistic model checker MRMC. In: Proceedings of the 6th International Conference on the Quantitative Evaluation of Systems (QEST), pp. 167\u2013176. IEEE (2009)","DOI":"10.1109\/QEST.2009.11"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing (preliminary report). In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 344\u2013352. ACM (1989)","DOI":"10.1145\/75277.75307"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94, 1\u201328 (1991)","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"2_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-44804-7_4","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"G.G.I. L\u00f3pez","year":"2001","unstructured":"L\u00f3pez, G.G.I., Hermanns, H., Katoen, J.-P.: Beyond memoryless distributions: Model checking semi-Markov chains. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 57\u201370. Springer, Heidelberg (2001)"},{"key":"2_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-24611-4_3","volume-title":"Validation of Stochastic Systems","author":"N. L\u00f3pez","year":"2004","unstructured":"L\u00f3pez, N., N\u00fa\u00f1ez, M.: An overview of probabilistic process algebras and their equivalences. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 89\u2013123. Springer, Heidelberg (2004)"},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"Markovski, J.: Towards supervisory control of interactive Markov chains: Controllability. In: 11th International Conference on Application of Concurrency to System Design (ACSD), pp. 108\u2013117 (2011)","DOI":"10.1109\/ACSD.2011.18"},{"key":"2_CR49","doi-asserted-by":"crossref","unstructured":"Markovski, J.: Towards supervisory control of interactive Markov chains: Plant minimization. In: 9th IEEE International Conference on Control and Automation (ICCA), pp. 1195\u20131200 (2011)","DOI":"10.1109\/ICCA.2011.6137945"},{"key":"2_CR50","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model checking nondeterministic and randomly timed systems. Ph.D. thesis, RWTH Aachen University (2010)"},{"key":"2_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-540-74407-8_28","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"M.R. Neuh\u00e4u\u00dfer","year":"2007","unstructured":"Neuh\u00e4u\u00dfer, M.R., Katoen, J.-P.: Bisimulation and logical preservation for continuous-time Markov decision processes. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 412\u2013427. Springer, Heidelberg (2007)"},{"key":"2_CR52","unstructured":"Pulungan, R.: Reduction of Acyclic Phase-Type Representations. Ph.D. thesis, Universit\u00e4t des Saarlandes, Saarbruecken, Germany (2009)"},{"key":"2_CR53","unstructured":"Puterman, M.L.: Markov decision processes: discrete stochastic dynamic programming, vol. 414. John Wiley & Sons (2009)"},{"key":"2_CR54","unstructured":"Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons (1998)"},{"key":"2_CR55","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing\u00a02, 250\u2013273 (1995)","journal-title":"Nordic Journal of Computing"},{"key":"2_CR56","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: Proceedings of the 2nd International Conference on the Quantitative Evaluation of Systems (QEST), pp. 251\u2013252. IEEE (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"2_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-32940-1_26","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"M. Timmer","year":"2012","unstructured":"Timmer, M., Katoen, J.-P., van de Pol, J., Stoelinga, M.I.A.: Efficient modelling and generation of markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 364\u2013379. Springer, Heidelberg (2012)"},{"key":"2_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2005","unstructured":"Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 429\u2013433. Springer, Heidelberg (2005)"},{"key":"2_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-12002-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Zhang","year":"2010","unstructured":"Zhang, L., Neuh\u00e4u\u00dfer, M.R.: Model checking interactive markov chains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 53\u201368. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45489-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T05:46:56Z","timestamp":1746510416000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-45489-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662454886","9783662454893"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-45489-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}