{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T01:10:45Z","timestamp":1773105045287,"version":"3.50.1"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319119359","type":"print"},{"value":"9783319119366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_8","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T19:12:03Z","timestamp":1414177923000},"page":"98-114","source":"Crossref","is-referenced-by-count":125,"title":["Verification of Markov Decision Processes Using Learning Algorithms"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Br\u00e1zdil","sequence":"first","affiliation":[]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Chmel\u00edk","sequence":"additional","affiliation":[]},{"given":"Vojt\u011bch","family":"Forejt","sequence":"additional","affiliation":[]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"given":"Mateusz","family":"Ujma","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Aljazzar, H., Leue, S.: Generation of counterexamples for model checking of Markov decision processes. In: QEST, pp. 197\u2013206 (2009)","DOI":"10.1109\/QEST.2009.10"},{"key":"8_CR2","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)"},{"issue":"1-2","key":"8_CR3","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/0004-3702(94)00011-O","volume":"72","author":"A.G. Barto","year":"1995","unstructured":"Barto, A.G., Bradtke, S.J., Singh, S.P.: Learning to act using real-time dynamic programming. Artificial Intelligence\u00a072(1-2), 81\u2013138 (1995)","journal-title":"Artificial Intelligence"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Bogdoll, J., Ferrer Fioriti, L.M., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE 2011. LNCS, vol.\u00a06722, pp. 59\u201374. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-21461-5_4"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-28540-0_20","volume-title":"Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance","author":"J. Bogdoll","year":"2012","unstructured":"Bogdoll, J., Hartmanns, A., Hermanns, H.: Simulation and statistical model checking for modestly nondeterministic models. In: Schmitt, J.B. (ed.) MMB & DFT 2012. LNCS, vol.\u00a07201, pp. 249\u2013252. Springer, Heidelberg (2012)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-40196-1_12","volume-title":"Quantitative Evaluation of Systems","author":"B. Boyer","year":"2013","unstructured":"Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: A flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol.\u00a08054, pp. 160\u2013164. Springer, Heidelberg (2013)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u0131ik, M., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. CoRR abs\/1402.2967 (2014)","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAAL-SMC: Statistical model checking for priced timed automata. In: QAPL (2012)","DOI":"10.4204\/EPTCS.85.1"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: An O(n 2) algorithm for alternating B\u00fcchi games. In: SODA, pp. 1386\u20131399 (2012)","DOI":"10.1137\/1.9781611973099.109"},{"key":"8_CR10","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: SODA (2011)","DOI":"10.1137\/1.9781611973082.101"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C., Grosser, M., Klein, J.: Reduction techniques for model checking Markov decision processes. In: QEST, pp. 45\u201354 (2008)","DOI":"10.1109\/QEST.2008.45"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/BFb0032043","volume-title":"Automata, Languages and Programming","author":"C. Courcoubetis","year":"1990","unstructured":"Courcoubetis, C., Yannakakis, M.: Markov decision processes and regular events (extended abstract). In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 336\u2013349. Springer, Heidelberg (1990)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-24310-3_7","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A. David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol.\u00a06919, pp. 80\u201396. Springer, Heidelberg (2011)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","volume-title":"Computer Aided Verification","author":"A. David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 349\u2013355. Springer, Heidelberg (2011)"},{"key":"8_CR15","unstructured":"De Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis (1997)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-19811-3_2","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Feng","year":"2011","unstructured":"Feng, L., Kwiatkowska, M., Parker, D.: Automated learning of probabilistic assumptions for compositional reasoning. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol.\u00a06603, pp. 2\u201317. Springer, Heidelberg (2011)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"He, R., Jennings, P., Basu, S., Ghosh, A.P., Wu, H.: A bounded statistical approach for model checking of unbounded until properties. In: ASE, pp. 225\u2013234 (2010)","DOI":"10.1145\/1858996.1859043"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Henriques, D., Martins, J., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for Markov decision processes. In: QEST, pp. 84\u201393 (2012)","DOI":"10.1109\/QEST.2012.19"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-31424-7_26","volume-title":"Computer Aided Verification","author":"C. Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Cross-entropy optimisation of importance sampling parameters for statistical model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 327\u2013342. Springer, Heidelberg (2012)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/978-3-642-28756-5_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking \u2013 PLASMA. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 498\u2013503. Springer, Heidelberg (2012)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/978-3-642-39799-8_38","volume-title":"Computer Aided Verification","author":"C. Jegourel","year":"2013","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 576\u2013591. Springer, Heidelberg (2013)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer (1976)","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Kolobov, A., Mausam, Weld, D.S., Geffner, H.: Heuristic search for generalized stochastic shortest path MDPS. In: ICAPS (2011)","DOI":"10.1609\/icaps.v21i1.13452"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203\u2013204 (2012)","DOI":"10.1109\/QEST.2012.14"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-38613-8_11","volume-title":"Integrated Formal Methods","author":"K.G. Larsen","year":"2013","unstructured":"Larsen, K.G.: Priced timed automata and statistical model checking. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol.\u00a07940, pp. 154\u2013161. Springer, Heidelberg (2013)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large Markov decision processes. In: SAC, pp. 1314\u20131319 (2012)","DOI":"10.1145\/2245276.2231984"},{"key":"8_CR29","unstructured":"Legay, A., Sedwards, S.: Lightweight Monte Carlo algorithm for Markov decision processes. CoRR abs\/1310.3609 (2013)"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"McMahan, H.B., Likhachev, M., Gordon, G.J.: Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees. In: ICML (2005)","DOI":"10.1145\/1102351.1102423"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Puterman, M.: Markov Decision Processes. Wiley (1994)","DOI":"10.1002\/9780470316887"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-04761-9_11","volume-title":"Automated Technology for Verification and Analysis","author":"D. Rabih El","year":"2009","unstructured":"El Rabih, D., Pekergin, N.: Statistical model checking using perfect simulation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 120\u2013134. Springer, Heidelberg (2009)"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 266\u2013280. Springer, Heidelberg (2005)"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 202\u2013215. Springer, Heidelberg (2004)"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Strehl, A.L., Li, L., Wiewiora, E., Langford, J., Littman, M.L.: PAC model-free reinforcement learning. In: ICML, pp. 881\u2013888 (2006)","DOI":"10.1145\/1143844.1143955"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Sutton, R., Barto, A.: Reinforcement Learning: An Introduction. MIT Press (1998)","DOI":"10.1109\/TNN.1998.712192"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"H. Younes","year":"2002","unstructured":"Younes, H., Simmons, R.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 223\u2013235. Springer, Heidelberg (2002)"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/978-3-642-19829-8_10","volume-title":"SBMF 2010","author":"H.L.S. Younes","year":"2011","unstructured":"Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: Davies, J. (ed.) SBMF 2010. LNCS, vol.\u00a06527, pp. 144\u2013160. Springer, Heidelberg (2011)"},{"key":"8_CR39","unstructured":"http:\/\/www.prismmodelchecker.org\/files\/atva14learn\/"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T15:17:04Z","timestamp":1689607024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}