{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:23:52Z","timestamp":1768001032654,"version":"3.49.0"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030255398","type":"print"},{"value":"9783030255404","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25540-4_29","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T11:02:35Z","timestamp":1562929355000},"page":"497-519","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":38,"title":["PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games"],"prefix":"10.1007","author":[{"given":"Pranav","family":"Ashok","sequence":"first","affiliation":[]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]},{"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Ashok, P., K\u0159et\u00ednsk\u00fd, J.: Maximilian Weininger. PAC statistical model checking for markov decision processes and stochastic games. Technical Report arXiv.org\/abs\/1905.04403 (2019)","DOI":"10.1007\/978-3-030-25540-4_29"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-13464-7_4","volume-title":"Formal Techniques for Distributed Systems","author":"A Basu","year":"2010","unstructured":"Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE 2010. LNCS, vol. 6117, pp. 32\u201346. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13464-7_4"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., et al.: Verification of markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"29_CR4","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., DArgenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160\u2013164. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_12"},{"key":"29_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.85.1","volume":"85","author":"Peter Bulychev","year":"2012","unstructured":"Bulychev, P.E., et al.: UPPAAL-SMC: statistical model checking for priced timed automata. In: QAPL (2012)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-21461-5_4","volume-title":"Formal Techniques for Distributed Systems","author":"J Bogdoll","year":"2011","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. 6722, pp. 59\u201374. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21461-5_4"},{"key":"29_CR7","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. 7201, pp. 249\u2013252. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28540-0_20"},{"key":"29_CR8","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008). ISBN 978-0-262-02649-9"},{"key":"29_CR9","unstructured":"Brafman, R.I., Tennenholtz, M.: A near-optimal poly-time algorithm for learning a class of stochastic games. In: IJCAI, pp. 734\u2013739 (1999)"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-36742-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: a model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 185\u2013191. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_13"},{"issue":"1","key":"29_CR11","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Meth. Syst. Des. 43(1), 61\u201392 (2013)","journal-title":"Formal Meth. Syst. Des."},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-69850-0_7","volume-title":"25 Years of Model Checking","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee, K., Henzinger, T.A.: Value iteration. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 107\u2013138. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0_7"},{"issue":"2","key":"29_CR13","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","volume":"78","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee, K., Henzinger, T.A.: A survey of stochastic $$\\omega $$ -regular games. J. Comput. Syst. Sci. 78(2), 394\u2013413 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-642-34059-8_16","volume-title":"Large-Scale Complex IT Systems. Development, Operation and Management","author":"R Calinescu","year":"2012","unstructured":"Calinescu, R., Kikuchi, S., Johnson, K.: Compositional reverification of probabilistic safety properties for large-scale complex IT systems. In: Calinescu, R., Garlan, D. (eds.) Monterey Workshop 2012. LNCS, vol. 7539, pp. 303\u2013329. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34059-8_16"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-22359-4_14","volume-title":"Computational Logic in Multi-Agent Systems","author":"T Chen","year":"2011","unstructured":"Chen, T., Kwiatkowska, M., Parker, D., Simaitis, A.: Verifying team formation protocols with probabilistic model checking. In: Leite, J., Torroni, P., \u00c5gotnes, T., Boella, G., van der Torre, L. (eds.) CLIMA 2011. LNCS (LNAI), vol. 6814, pp. 190\u2013207. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22359-4_14"},{"issue":"2","key":"29_CR16","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203\u2013224 (1992)","journal-title":"Inf. Comput."},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: ATVA, pp. 1\u201312 (2011)","DOI":"10.1007\/978-3-642-24372-1_1"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"David, A., et al.: Statistical model checking for stochastic hybrid systems. In: HSB, pp. 122\u2013136 (2012)","DOI":"10.4204\/EPTCS.92.9"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-38088-4_24","volume-title":"NASA Formal Methods","author":"A David","year":"2013","unstructured":"David, A., Du, D., Guldstrand Larsen, K., Legay, A., Miku\u010dionis, M.: Optimizing control strategy using statistical model checking. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 352\u2013367. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_24"},{"key":"29_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-662-49674-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Daca","year":"2016","unstructured":"Daca, P., Henzinger, T.A., K\u0159et\u00ednsk\u00fd, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 112\u2013129. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_7"},{"key":"29_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-03421-4_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"PR D\u2019Argenio","year":"2018","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 336\u2013353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_22"},{"key":"29_CR22","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., et al.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80\u201396. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24310-3_7"},{"key":"29_CR23","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. 6806, pp. 349\u2013355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_27"},{"issue":"4","key":"29_CR24","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s10009-015-0383-0","volume":"17","author":"P D\u2019Argenio","year":"2015","unstructured":"D\u2019Argenio, P., Legay, A., Sedwards, S., Traonouez, L.-M.: Smart sampling for lightweight verification of markov decision processes. STTT 17(4), 469\u2013484 (2015)","journal-title":"STTT"},{"key":"29_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-33365-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"C Ellen","year":"2012","unstructured":"Ellen, C., Gerwinn, S., Fr\u00e4nzle, M.: Confidence bounds for statistical model checking of probabilistic hybrid systems. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 123\u2013138. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33365-1_10"},{"key":"29_CR26","doi-asserted-by":"crossref","unstructured":"Fu, J., Topcu, U.: Probably approximately correct MDP learning and control with temporal logic constraints. In: Robotics: Science and Systems (2014)","DOI":"10.15607\/RSS.2014.X.039"},{"key":"29_CR27","unstructured":"Hasanbeig, M., Abate, A., Kroening, D.: Logically-correct reinforcement learning. CoRR, 1801.08099 (2018)"},{"key":"29_CR28","unstructured":"Hasanbeig, M., Abate, A., Kroening, D.: Certified reinforcement learning with logic guidance. CoRR, abs\/1902.00778 (2019)"},{"key":"29_CR29","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":"29_CR30","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Arnd Hartmanns","year":"2019","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: TACAS 2019 (2019, to appear)"},{"key":"29_CR31","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. 2937, pp. 73\u201384. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_8"},{"key":"29_CR32","doi-asserted-by":"crossref","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. (2017)","DOI":"10.1016\/j.tcs.2016.12.003"},{"key":"29_CR33","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":"29_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-030-17462-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2019","unstructured":"Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Omega-regular objectives in model-free reinforcement learning. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 395\u2013412. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_27"},{"key":"29_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-03845-7_15","volume-title":"Computational Methods in Systems Biology","author":"SK Jha","year":"2009","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218\u2013234. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03845-7_15"},{"key":"29_CR36","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. 7214, pp. 498\u2013503. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_37"},{"key":"29_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1007\/978-3-319-96145-3_36","volume-title":"Computer Aided Verification","author":"E Kelmendi","year":"2018","unstructured":"Kelmendi, E., Kr\u00e4mer, J., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: stopping criterion and learning algorithm. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 623\u2013642. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_36"},{"key":"29_CR38","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T.: Of cores: a partial-exploration framework for Markov decision processes. Submitted 2019"},{"key":"29_CR39","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. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"29_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-33365-1_2","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"KG Larsen","year":"2012","unstructured":"Larsen, K.G.: Statistical model checking, refinement checking, optimization,. for stochastic hybrid systems. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 7\u201310. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33365-1_2"},{"key":"29_CR41","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 Guldstrand Larsen","year":"2013","unstructured":"Guldstrand Larsen, K.: Priced timed automata and statistical model checking. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 154\u2013161. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38613-8_11"},{"key":"29_CR42","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/B978-1-55860-335-6.50027-1","volume-title":"Machine Learning Proceedings 1994","author":"Michael L. Littman","year":"1994","unstructured":"Littman, M.L.: Markov games as a framework for multi-agent reinforcement learning. In: ICML, pp. 157\u2013163 (1994)"},{"issue":"3","key":"29_CR43","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1287\/moor.6.3.379","volume":"6","author":"S Lakshmivarahan","year":"1981","unstructured":"Lakshmivarahan, S., Narendra, K.S.: Learning algorithms for two-person zero-sum stochastic games with incomplete information. Math. Oper. Res. 6(3), 379\u2013386 (1981)","journal-title":"Math. Oper. Res."},{"issue":"1\u20133","key":"29_CR44","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/j.apal.2007.11.006","volume":"152","author":"R Lassaigne","year":"2008","unstructured":"Lassaigne, R., Peyronnet, S.: Probabilistic verification and approximation. Ann. Pure Appl. Logic 152(1\u20133), 122\u2013131 (2008)","journal-title":"Ann. Pure Appl. Logic"},{"key":"29_CR45","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":"29_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-319-15201-1_23","volume-title":"Software Engineering and Formal Methods","author":"A Legay","year":"2015","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Scalable verification of markov decision processes. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 350\u2013362. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23"},{"issue":"2","key":"29_CR47","doi-asserted-by":"publisher","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"DA Martin","year":"1975","unstructured":"Martin, D.A.: Borel determinacy. Ann. Math. 102(2), 363\u2013371 (1975)","journal-title":"Ann. Math."},{"key":"29_CR48","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: In ICML 2005, pp. 569\u2013576 (2005)","DOI":"10.1145\/1102351.1102423"},{"key":"29_CR49","volume-title":"Markov Chains","author":"JR Norris","year":"1998","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press, Cambridge (1998)"},{"key":"29_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-40708-6_10","volume-title":"Computational Methods in Systems Biology","author":"SK Palaniappan","year":"2013","unstructured":"Palaniappan, S.K., Gyori, B.M., Liu, B., Hsu, D., Thiagarajan, P.S.: Statistical model checking based calibration and analysis of bio-pathway models. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 120\u2013134. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40708-6_10"},{"key":"29_CR51","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"2014","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (2014)"},{"issue":"6","key":"29_CR52","first-page":"437","volume":"35","author":"TES Raghavan","year":"1991","unstructured":"Raghavan, T.E.S., Filar, J.A.: Algorithms for stochastic games \u2013 a survey. Z. Oper. Res. 35(6), 437\u2013472 (1991)","journal-title":"Z. Oper. Res."},{"key":"29_CR53","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. 5799, pp. 120\u2013134. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_11"},{"key":"29_CR54","volume-title":"Reinforcement Learning: An Introduction","author":"R Sutton","year":"1998","unstructured":"Sutton, R., Barto, A.: Reinforcement Learning: An Introduction. MIT Press, Cambridge (1998)"},{"key":"29_CR55","doi-asserted-by":"crossref","unstructured":"Sadigh, D., Kim, E.S., Coogan, S., Sastry, S.S.S., Sanjit, A.: A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In: CDC, pp. 1091\u20131096 (2014)","DOI":"10.21236\/ADA623517"},{"key":"29_CR56","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"},{"issue":"1","key":"29_CR57","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/2168260.2168264","volume":"7","author":"F Saffre","year":"2012","unstructured":"Saffre, F., Simaitis, A.: Host selection through collective decision. ACM Trans. Auton. Adapt. Syst. 7(1), 4:1\u20134:16 (2012)","journal-title":"ACM Trans. Auton. Adapt. Syst."},{"key":"29_CR58","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. 3114, pp. 202\u2013215. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_16"},{"key":"29_CR59","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. 3576, pp. 266\u2013280. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_26"},{"key":"29_CR60","unstructured":"Wen, M., Topcu, U.: Probably approximately correct learning in stochastic games with temporal logic specifications. In: IJCAI, pp. 3630\u20133636 (2016)"},{"key":"29_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-642-19829-8_10","volume-title":"Formal Methods: Foundations and Applications","author":"HLS Younes","year":"2011","unstructured":"Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 144\u2013160. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19829-8_10"},{"issue":"3","key":"29_CR62","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"HLS Younes","year":"2006","unstructured":"Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT 8(3), 216\u2013228 (2006)","journal-title":"STTT"},{"key":"29_CR63","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":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_17"},{"key":"29_CR64","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink\/stateflow verification. In: HSCC, pp. 243\u2013252 (2010)","DOI":"10.21236\/ADA531406"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25540-4_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,3]],"date-time":"2019-12-03T17:29:07Z","timestamp":1575394147000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25540-4_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255398","9783030255404"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25540-4_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"258","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}