{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:24:36Z","timestamp":1777519476000,"version":"3.51.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319991535","type":"print"},{"value":"9783319991542","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-99154-2_13","type":"book-chapter","created":{"date-parts":[[2018,8,14]],"date-time":"2018-08-14T14:14:35Z","timestamp":1534256075000},"page":"207-222","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Model Checking for Safe Navigation Among Humans"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Junges","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruohan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mary","family":"Hayhoe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,15]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1613\/jair.318","volume":"4","author":"RI Brafman","year":"1996","unstructured":"Brafman, R.I., Tennenholtz, M.: On partially controlled multi-agent systems. J. Artif. Intell. Res. 4, 477\u2013507 (1996)","journal-title":"J. Artif. Intell. Res."},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1613\/jair.2502","volume":"31","author":"K Dresner","year":"2008","unstructured":"Dresner, K., Stone, P.: A multiagent approach to autonomous intersection management. J. Artif. Intell. Res. 31, 591\u2013656 (2008)","journal-title":"J. Artif. Intell. Res."},{"issue":"2","key":"13_CR3","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1109\/4236.914647","volume":"5","author":"MP Wellman","year":"2001","unstructured":"Wellman, M.P., Wurman, P.R., O\u2019Malley, K., Bangera, R., Reeves, D., Walsh, W.E.: Designing the market game for a trading agent competition. IEEE Internet Comput. 5(2), 43\u201351 (2001)","journal-title":"IEEE Internet Comput."},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1177\/0278364916688949","volume":"36","author":"P Khandelwal","year":"2017","unstructured":"Khandelwal, P., et al.: Bwibots: a platform for bridging the gap between AI and human-robot interaction research. Int. J. Robot. Res. 36, 635\u2013659 (2017)","journal-title":"Int. J. Robot. Res."},{"key":"13_CR5","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)"},{"key":"13_CR6","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"1998","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press, Cambridge (1998)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z.: Model checking for probability and time: from theory to practice. In: LICS, p. 351. IEEE Computer Society (2003)","DOI":"10.1109\/LICS.2003.1210075"},{"key":"13_CR8","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A STORM is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63390-9_31","DOI":"10.1007\/978-3-319-63390-9_31"},{"issue":"5","key":"13_CR10","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 Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"issue":"2","key":"13_CR11","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":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1007\/978-3-662-49674-9_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Kwiatkowska","year":"2016","unstructured":"Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-Games 2.0: a tool for multi-objective strategy synthesis for stochastic games. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 560\u2013566. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49674-9_35"},{"key":"13_CR13","unstructured":"Dean, T.L., Givan, R.: Model minimization in Markov decision processes. In: AAAI\/IAAI, pp. 106\u2013111. AAAI Press\/The MIT Press (1997)"},{"issue":"1","key":"13_CR14","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1167\/17.1.28","volume":"17","author":"MH Tong","year":"2017","unstructured":"Tong, M.H., Zohar, O., Hayhoe, M.M.: Control of gaze while walking: task structure, reward, and uncertainty. J. Vis. 17(1), 28 (2017)","journal-title":"J. Vis."},{"issue":"4","key":"13_CR15","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/s00422-013-0562-6","volume":"107","author":"CA Rothkopf","year":"2013","unstructured":"Rothkopf, C.A., Ballard, D.H.: Modular inverse reinforcement learning for visuomotor behaviour. Biol. Cybern. 107(4), 477\u2013490 (2013)","journal-title":"Biol. Cybern."},{"key":"13_CR16","first-page":"1445","volume":"I","author":"N Sprague","year":"2003","unstructured":"Sprague, N., Ballard, D.: Multiple-goal reinforcement learning with modular sarsa (0). IJCA I, 1445\u20131447 (2003)","journal-title":"IJCA"},{"issue":"1\u20132","key":"13_CR17","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1163\/22134808-00002414","volume":"26","author":"DH Ballard","year":"2013","unstructured":"Ballard, D.H., Kit, D., Rothkopf, C.A., Sullivan, B.: A hierarchical modular architecture for embodied cognition. Multisens. Res. 26(1\u20132), 177\u2013204 (2013)","journal-title":"Multisens. Res."},{"issue":"2","key":"13_CR18","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1016\/j.neuron.2016.12.040","volume":"93","author":"YC Leong","year":"2017","unstructured":"Leong, Y.C., Radulescu, A., Daniel, R., DeWoskin, V., Niv, Y.: Dynamic interaction between reinforcement learning and attention in multidimensional environments. Neuron 93(2), 451\u2013463 (2017)","journal-title":"Neuron"},{"issue":"2","key":"13_CR19","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.robot.2011.10.005","volume":"60","author":"S Konur","year":"2012","unstructured":"Konur, S., Dixon, C., Fisher, M.: Analysing robot swarm behaviour via probabilistic model checking. Robot. Auton. Syst. 60(2), 199\u2013213 (2012)","journal-title":"Robot. Auton. Syst."},{"issue":"6","key":"13_CR20","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1177\/0278364914562980","volume":"34","author":"B Johnson","year":"2015","unstructured":"Johnson, B., Kress-Gazit, H.: Analyzing and revising synthesized controllers for robots with sensing and actuation errors. Int. J. Robot. Res. 34(6), 816\u2013832 (2015)","journal-title":"Int. J. Robot. Res."},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-319-77935-5_16","volume-title":"NASA Formal Methods","author":"R Giaquinta","year":"2018","unstructured":"Giaquinta, R., Hoffmann, R., Ireland, M., Miller, A., Norman, G.: Strategy synthesis for autonomous agents using PRISM. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 220\u2013236. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-77935-5_16"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-642-40196-1_28","volume-title":"Quantitative Evaluation of Systems","author":"T Chen","year":"2013","unstructured":"Chen, T., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: Synthesis for multi-objective stochastic games: an application to autonomous urban driving. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 322\u2013337. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-40196-1_28"},{"issue":"2","key":"13_CR23","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1109\/TASE.2016.2530623","volume":"13","author":"L Feng","year":"2016","unstructured":"Feng, L., Wiltsche, C., Humphrey, L., Topcu, U.: Synthesis of human-in-the-loop control protocols for autonomous systems. IEEE Trans. Autom. Sci. Eng. 13(2), 450\u2013462 (2016)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"13_CR24","unstructured":"Lacerda, B., Parker, D., Hawes, N.: Optimal policy generation for partially satisfiable co-safe LTL specifications. In: IJCAI, pp. 1587\u20131593. AAAI Press (2015)"},{"key":"13_CR25","first-page":"157","volume":"157","author":"ML Littman","year":"1994","unstructured":"Littman, M.L.: Markov games as a framework for multi-agent reinforcement learning. ICML 157, 157\u2013163 (1994)","journal-title":"ICML"},{"issue":"2","key":"13_CR26","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/S0004-3702(02)00121-2","volume":"136","author":"M Bowling","year":"2002","unstructured":"Bowling, M., Veloso, M.: Multiagent learning using a variable learning rate. Artif. Intell. 136(2), 215\u2013250 (2002)","journal-title":"Artif. Intell."},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-642-34005-5_7","volume-title":"Rewriting Logic and Its Applications","author":"R Bruni","year":"2012","unstructured":"Bruni, R., Corradini, A., Gadducci, F., Lluch Lafuente, A., Vandin, A.: Modelling and analyzing adaptive self-assembly strategies with maude. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 118\u2013138. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-34005-5_7"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: LICS, pp. 31\u201345. ACM (2016)","DOI":"10.1145\/2933575.2934574"},{"issue":"1","key":"13_CR29","first-page":"1437","volume":"16","author":"J Garc\u0131a","year":"2015","unstructured":"Garc\u0131a, J., Fern\u00e1ndez, F.: A comprehensive survey on safe reinforcement learning. J. Mach. Learn. Res. 16(1), 1437\u20131480 (2015)","journal-title":"J. Mach. Learn. Res."},{"key":"13_CR30","unstructured":"Sculley, D., Phillips, T., Ebner, D., Chaudhary, V., Young, M.: Machine learning: the high-interest credit card of technical debt (2014)"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Winterer, L., et al.: Motion planning under partial observability using game-based abstraction. In: CDC, pp. 2201\u20132208. IEEE (2017)","DOI":"10.1109\/CDC.2017.8263971"},{"issue":"4","key":"13_CR32","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. Log. Methods Comput. Sci. 4(4), 1\u201321 (2008)","journal-title":"Log. Methods Comput. Sci."},{"issue":"1","key":"13_CR33","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018)","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Wachter, B., Zhang, L., Hermanns, H.: Probabilistic model checking modulo theories. In: QEST, pp. 129\u2013140. IEEE CS (2007)","DOI":"10.1109\/QEST.2007.10"},{"key":"13_CR35","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99154-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,8,14]],"date-time":"2018-08-14T14:22:08Z","timestamp":1534256528000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99154-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319991535","9783319991542"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99154-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}