{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:12:08Z","timestamp":1768907528387,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496732","type":"print"},{"value":"9783662496749","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_8","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"130-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":55,"title":["Safety-Constrained Reinforcement Learning for MDPs"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Junges","sequence":"first","affiliation":[]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Dehnert","sequence":"additional","affiliation":[]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"8_CR1","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)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Proceedings of QEST, pp. 131\u2013132 (2006)","DOI":"10.1109\/QEST.2006.25"},{"issue":"2","key":"8_CR3","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"JP Katoen","year":"2011","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. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"issue":"4\u20135","key":"8_CR4","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-005-0216-7","volume":"8","author":"GD Penna","year":"2006","unstructured":"Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite horizon analysis of Markov chains with the Murphi verifier. Softw. Tools Technol. Transf. 8(4\u20135), 397\u2013409 (2006)","journal-title":"Softw. Tools Technol. Transf."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of QEST, pp. 203\u2013204. IEEE CS (2012)","DOI":"10.1109\/QEST.2012.14"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 317\u2013332. Springer, Heidelberg (2012)"},{"issue":"4","key":"8_CR7","first-page":"1","volume":"4","author":"K Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Logical Methods Comput. Sci. 4(4), 1\u201321 (2008)","journal-title":"Logical Methods Comput. Sci."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S.: Trade-off analysis meets probabilistic model checking. In: Proceedings of CSL-LICS, pp. 1:1\u20131:10. ACM (2014)","DOI":"10.1145\/2603088.2603089"},{"key":"8_CR9","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":"8_CR10","doi-asserted-by":"crossref","unstructured":"Littman, M.L.: Markov games as a framework for multi-agent reinforcement learning. In: Proceedings of ICML, pp. 157\u2013163. Morgan Kaufmann (1994)","DOI":"10.1016\/B978-1-55860-335-6.50027-1"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-642-54862-8_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Dr\u00e4ger","year":"2014","unstructured":"Dr\u00e4ger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 531\u2013546. Springer, Heidelberg (2014)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Wen, M., Ehlers, R., Topcu, U.: Correct-by-synthesis reinforcement learning with temporal logic constraints. CoRR (2015)","DOI":"10.1109\/IROS.2015.7354078"},{"key":"8_CR13","unstructured":"Moldovan, T.M., Abbeel, P.: Safe exploration in Markov decision processes. In: Proceedings of ICML. icml.cc\/Omnipress (2012)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Fu, J., Topcu, U.: Probably approximately correct MDP learning and control with temporal logic constraints. In: Proceedings of RSS (2014)","DOI":"10.15607\/RSS.2014.X.039"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Akametalu, A., Fisac, J., Gillula, J., Kaynama, S., Zeilinger, M., Tomlin, C.: Reachability-based safe learning with Gaussian processes. In: Proceedings of CDC, pp. 1424\u20131431 (2014)","DOI":"10.1109\/CDC.2014.7039601"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-13823-7_31","volume-title":"Modelling and Simulation for Autonomous Systems","author":"M Pecka","year":"2014","unstructured":"Pecka, M., Svoboda, T.: Safe exploration techniques for reinforcement learning \u2013 an overview. In: Hodicky, J. (ed.) MESAS 2014. LNCS, vol. 8906, pp. 357\u2013375. Springer, Heidelberg (2014)"},{"key":"8_CR17","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24611-4_1","volume-title":"Validation of Stochastic Systems","author":"A Sokolova","year":"2004","unstructured":"Sokolova, A., de Vink, E.P.: Probabilistic automata: system types, parallel composition and comparison. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 1\u201343. Springer, Heidelberg (2004)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Phan, A.: $$\\nu $$ Z - maximal satisfaction with Z3. In: Proceedings of SCSS. EPiC Series, vol. 30, pp. 1\u20139. EasyChair (2014)","DOI":"10.29007\/jmxj"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.tcs.2014.06.020","volume":"549","author":"R Wimmer","year":"2014","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: Minimal counterexamples for linear-time probabilistic verification. Theor. Comput. Sci. 549, 61\u2013100 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR21","first-page":"213","volume":"3","author":"RI Brafman","year":"2002","unstructured":"Brafman, R.I., Tennenholtz, M.: R-MAX - a general polynomial time algorithm for near-optimal reinforcement learning. J. Mach. Learn. Res. 3, 213\u2013231 (2002)","journal-title":"J. Mach. Learn. Res."},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"St\u00fcckler, J., Schwarz, M., Schadler, M., Topalidou-Kyniazopoulou, A., Behnke, S.: Nimbro explorer: semiautonomous exploration and mobile manipulation in rough terrain. J. Field Robot. (2015, to appear)","DOI":"10.1002\/rob.21592"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T08:26:56Z","timestamp":1748852816000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}