{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T09:47:12Z","timestamp":1769507232867,"version":"3.49.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031753794","type":"print"},{"value":"9783031753800","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T00:00:00Z","timestamp":1730246400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T00:00:00Z","timestamp":1730246400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75380-0_22","type":"book-chapter","created":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T08:29:02Z","timestamp":1730190542000},"page":"385-404","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["CommonUppRoad: A Framework of\u00a0Formal Modelling, Verifying, Learning, and\u00a0Visualisation of\u00a0Autonomous Vehicles"],"prefix":"10.1007","author":[{"given":"Rong","family":"Gu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kaige","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas Holck","family":"H\u00f8eg-Petersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,30]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a032 (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Althoff, M., Koschi, M., Manzinger, S.: CommonRoad: composable benchmarks for motion planning on roads. In: 2017 IEEE Intelligent Vehicles Symposium (IV), pp. 719\u2013726. IEEE (2017)","DOI":"10.1109\/IVS.2017.7995802"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1016\/j.ic.2018.02.021","volume":"261","author":"R Alur","year":"2018","unstructured":"Alur, R., Moarref, S., Topcu, U.: Compositional and symbolic synthesis of reactive controllers for multi-agent systems. Inf. Comput. 261, 616\u2013633 (2018)","journal-title":"Inf. Comput."},{"key":"22_CR4","unstructured":"BBC: Uber\u2019s self-driving operator charged over fatal crash. https:\/\/www.bbc.com\/news\/technology-54175359 (2020)"},{"key":"22_CR5","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: timed games for everyone. In: Nordic Workshop on Programming Theory (NWPT 2006) (2006)"},{"key":"22_CR6","doi-asserted-by":"publisher","unstructured":"Bender, P., Ziegler, J., Stiller, C.: Lanelets: efficient map representation for autonomous driving. In: 2014 IEEE Intelligent Vehicles Symposium Proceedings, pp. 420\u2013425 (2014). https:\/\/doi.org\/10.1109\/IVS.2014.6856487","DOI":"10.1109\/IVS.2014.6856487"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354\u2013359. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_31"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0055357","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 298\u2013302. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055357"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-662-46681-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2015","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.:  Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206\u2013211. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"Gu, R., et al.: Synthesis and verification of mission plans for multiple autonomous agents under complex road conditions. ACM Trans. Softw. Eng. Methodol. (2024). https:\/\/doi.org\/10.1145\/3672445","DOI":"10.1145\/3672445"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Gu, R., Enoiu, E., Seceleanu, C.: TAMAA: UPPAAL-based mission planning for autonomous agents. In: Proceedings of the 35th Annual ACM Symposium on Applied Computing, pp. 1624\u20131633 (2020)","DOI":"10.1145\/3341105.3374001"},{"issue":"3","key":"22_CR13","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s10009-022-00657-z","volume":"24","author":"R Gu","year":"2022","unstructured":"Gu, R., Jensen, P.G., Poulsen, D.B., Seceleanu, C., Enoiu, E., Lundqvist, K.: Verifiable strategy synthesis for multiple autonomous agents: a scalable approach. Int. J. Softw. Tools Technol. Transfer 24(3), 395\u2013414 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"22_CR14","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102894","volume":"224","author":"R Gu","year":"2022","unstructured":"Gu, R., Jensen, P.G., Seceleanu, C., Enoiu, E., Lundqvist, K.: Correctness-guaranteed strategy synthesis and compression for multi-agent autonomous systems. Sci. Comput. Program. 224, 102894 (2022)","journal-title":"Sci. Comput. Program."},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Hekmatnejad, M., et al.: Encoding and monitoring responsibility sensitive safety rules for automated vehicles in signal temporal logic. In: Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 1\u201311 (2019)","DOI":"10.1145\/3359986.3361203"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Krajewski, R., Bock, J., Kloeker, L., Eckstein, L.: The highD dataset: a drone dataset of naturalistic vehicle trajectories on German highways for validation of highly automated driving systems. In: 2018 21st International Conference on Intelligent Transportation Systems (ITSC), pp. 2118\u20132125 (2018). https:\/\/doi.org\/10.1109\/ITSC.2018.8569552","DOI":"10.1109\/ITSC.2018.8569552"},{"key":"22_CR17","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Lenz, D., Kessler, T., Knoll, A.: Stochastic model predictive controller with chance constraints for comfortable and safe driving behavior of autonomous vehicles. In: 2015 IEEE Intelligent Vehicles Symposium (IV), pp. 292\u2013297 (2015). https:\/\/doi.org\/10.1109\/IVS.2015.7225701","DOI":"10.1109\/IVS.2015.7225701"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Lercher, F., Althoff, M.: Specification-compliant reachability analysis for autonomous vehicles using on-the-fly model checking (2024)","DOI":"10.1109\/IV55156.2024.10588549"},{"key":"22_CR20","doi-asserted-by":"publisher","first-page":"4180","DOI":"10.1109\/TIV.2023.3289580","volume":"8","author":"I Liu","year":"2023","unstructured":"Liu, I., Althoff, M.: Specification-compliant driving corridors for motion planning of automated vehicles. IEEE Trans. Intell. Veh. 8, 4180\u20134197 (2023)","journal-title":"IEEE Trans. Intell. Veh."},{"key":"22_CR21","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2022.110692","volume":"152","author":"N Mehdipour","year":"2023","unstructured":"Mehdipour, N., Althoff, M., Tebbens, R.D., Belta, C.: Formal methods to comply with rules of the road in autonomous driving: state of the art and grand challenges. Automatica 152, 110692 (2023)","journal-title":"Automatica"},{"key":"22_CR22","unstructured":"Muhammad, N., Rong, G., Cristina, S., Kim, G.L., Brian, N., Michele, A.: Energy-optimized motion planning for autonomous vehicles using UPPAAL STRATEGO. In: The 18th International Symposium on Theoretical Aspects of Software Engineering. Springer (2024)"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Pek, C., Rusinov, V., Manzinger, S., \u00dcste, M.C., Althoff, M.: Commonroad drivability checker: simplifying the development and validation of motion planning algorithms. In: 2020 IEEE Intelligent Vehicles Symposium (IV), pp. 1013\u20131020. IEEE (2020)","DOI":"10.1109\/IV47402.2020.9304544"},{"key":"22_CR24","unstructured":"Post, T.W.: 17 fatalities, 736 crashes: the shocking toll of tesla\u2019s autopilot (2023). https:\/\/www.washingtonpost.com\/technology\/2023\/06\/10\/tesla-autopilot-crashes-elon-musk\/"},{"key":"22_CR25","unstructured":"Raffin, A., Hill, A., Gleave, A., Kanervisto, A., Ernestus, M., Dormann, N.: Stable-baselines3: reliable reinforcement learning implementations. J. Mach. Learn. Res. 22(268), 1\u20138 (2021). http:\/\/jmlr.org\/papers\/v22\/20-1364.html"},{"key":"22_CR26","unstructured":"SAE: Taxonomy and definitions for terms related to driving automation systems for on-road motor vehicles (2021)"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, J.M.G., Nyberg, T., Pek, C., Tumova, J., T\u00f6rngren, M.: Foresee the unseen: sequential reasoning about hidden obstacles for safe driving. In: 2022 IEEE Intelligent Vehicles Symposium (IV), pp. 255\u2013264. IEEE (2022)","DOI":"10.1109\/IV51971.2022.9827171"},{"key":"22_CR28","unstructured":"Schilling, C., Lukina, A., Demirovi\u0107, E., Larsen, K.: Safety verification of decision-tree policies in continuous time. In: Advances in Neural Information Processing Systems, vol. 36 (2024)"},{"issue":"1","key":"22_CR29","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1162\/089892999563184","volume":"11","author":"RS Sutton","year":"1999","unstructured":"Sutton, R.S., Barto, A.G., et al.: Reinforcement learning. J. Cogn. Neurosci. 11(1), 126\u2013134 (1999)","journal-title":"J. Cogn. Neurosci."},{"key":"22_CR30","doi-asserted-by":"publisher","unstructured":"Towers, M., et al.: Gymnasium (2023). https:\/\/doi.org\/10.5281\/zenodo.8127026, https:\/\/zenodo.org\/record\/8127025","DOI":"10.5281\/zenodo.8127026"},{"key":"22_CR31","doi-asserted-by":"publisher","unstructured":"Wang, X., Krasowski, H., Althoff, M.: CommonRoad-RL: a configurable reinforcement learning environment for motion planning of autonomous vehicles. In: IEEE International Conference on Intelligent Transportation Systems (ITSC) (2021). https:\/\/doi.org\/10.1109\/ITSC48978.2021.9564898","DOI":"10.1109\/ITSC48978.2021.9564898"},{"key":"22_CR32","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/BF00992698","volume":"8","author":"CJ Watkins","year":"1992","unstructured":"Watkins, C.J., Dayan, P.: Q-learning. Mach. Learn. 8, 279\u2013292 (1992)","journal-title":"Mach. Learn."},{"key":"22_CR33","doi-asserted-by":"crossref","unstructured":"Yang, Q., Sim\u00e3o, T.D., Jansen, N., Tindemans, S.H., Spaan, M.T.: Reinforcement learning by guided safe exploration. arXiv preprint arXiv:2307.14316 (2023)","DOI":"10.3233\/FAIA230598"},{"issue":"3","key":"22_CR34","first-page":"991","volume":"49","author":"J Tao","year":"2022","unstructured":"Tao, J., et al.: Finding critical scenarios for automated driving systems: a systematic mapping study. IEEE Trans. Software Eng. 49(3), 991\u20131026 (2022)","journal-title":"IEEE Trans. Software Eng."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75380-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T08:52:50Z","timestamp":1730191970000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75380-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,30]]},"ISBN":["9783031753794","9783031753800"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75380-0_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,30]]},"assertion":[{"value":"30 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}