{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T16:07:55Z","timestamp":1779034075466,"version":"3.51.4"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We introduce a hybrid spatiotemporal logic for automotive safety applications (HSTL), focused on highway driving. Spatiotemporal logic features specifications about vehicles throughout space and time, while hybrid logic enables precise references to individual vehicles and their historical positions. We define the semantics of HSTL and provide a baseline model-checking algorithm for it. We propose two optimized model-checking algorithms, which reduce the search space based on the reachable states and possible transitions from one state to another. All three model-checking algorithms are evaluated on a series of common driving scenarios such as safe following, safe crossings, overtaking, and platooning. An exponential performance improvement is observed for the optimized algorithms.<\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_18","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:51:19Z","timestamp":1779033079000},"page":"337-356","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Hybrid Spatiotemporal Logic for\u00a0Automotive Applications: Modeling and\u00a0Model-Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6966-1136","authenticated-orcid":false,"given":"Radu-Florin","family":"Tulcan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5201-9895","authenticated-orcid":false,"given":"Rose","family":"Bohrer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9814-7323","authenticated-orcid":false,"given":"Yo\u00e0v","family":"Montacute","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4907-9453","authenticated-orcid":false,"given":"Kevin","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2151-9560","authenticated-orcid":false,"given":"Yusuke","family":"Kawamoto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"issue":"4","key":"18_CR1","doi-asserted-by":"publisher","first-page":"903","DOI":"10.1109\/TRO.2014.2312453","volume":"30","author":"M Althoff","year":"2014","unstructured":"Althoff, M., Dolan, J.M.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Rob. 30(4), 903\u2013918 (2014)","journal-title":"IEEE Trans. Rob."},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_30"},{"issue":"2","key":"18_CR3","doi-asserted-by":"publisher","first-page":"1143","DOI":"10.1109\/LRA.2020.2966414","volume":"5","author":"A Amini","year":"2020","unstructured":"Amini, A., et al.: Learning robust control policies for end-to-end autonomous driving from data-driven simulation. IEEE Rob. Autom. Lett. 5(2), 1143\u20131150 (2020)","journal-title":"IEEE Rob. Autom. Lett."},{"issue":"3","key":"18_CR4","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1020083231504","volume":"17","author":"B Bennett","year":"2002","unstructured":"Bennett, B., Cohn, A.G., Wolter, F., Zakharyaschev, M.: Multi-dimensional modal logic as a framework for spatio-temporal reasoning. Appl. Intell. 17(3), 239\u2013251 (2002)","journal-title":"Appl. Intell."},{"issue":"3","key":"18_CR5","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1093\/jigpal\/8.3.339","volume":"8","author":"P Blackburn","year":"2000","unstructured":"Blackburn, P.: Representation, reasoning, and relational structures: a hybrid logic manifesto. Logic J. IGPL 8(3), 339\u2013365 (2000)","journal-title":"Logic J. IGPL"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Bohrer, R., Platzer, A.: A hybrid, dynamic logic for hybrid-dynamic information flow. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 115\u2013124 (2018)","DOI":"10.1145\/3209108.3209151"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Bra\u00fcner, T.: Hybrid logic and Its Proof-Theory, vol.\u00a037. Springer Science & Business Media (2010)","DOI":"10.1007\/978-94-007-0002-4"},{"issue":"1","key":"18_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TPAMI.2021.3137605","volume":"45","author":"X Chang","year":"2021","unstructured":"Chang, X., Ren, P., Xu, P., Li, Z., Chen, X., Hauptmann, A.: A comprehensive survey of scene graphs: generation and application. IEEE Trans. Pattern Anal. Mach. Intell. 45(1), 1\u201326 (2021)","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"issue":"22","key":"18_CR9","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.5900","volume":"33","author":"H Cheng","year":"2021","unstructured":"Cheng, H., Li, P., Wang, R., Xu, H.: Dynamic spatio-temporal logic based on RCC-8. Concurrency Comput. Pract. Experience 33(22), e5900 (2021)","journal-title":"Concurrency Comput. Pract. Experience"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-662-49224-6_24","volume-title":"Software Engineering and Formal Methods","author":"V Ciancia","year":"2015","unstructured":"Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Bianculli, D., Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9509, pp. 297\u2013311. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-49224-6_24"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model checking spatial logics for closure spaces. Logical Methods Comput. Sci. 12 (2017)","DOI":"10.2168\/LMCS-12(4:2)2016"},{"key":"18_CR12","unstructured":"Dosovitskiy, A., Ros, G., Codevilla, F., Lopez, A., Koltun, V.: CARLA: an open urban driving simulator. In: Conference on Robot Learning, pp. 1\u201316. PMLR (2017)"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Eberhart, C., Dubut, J., Haydon, J., Hasuo, I.: Formal verification of safety architectures for automated driving. In: 2023 IEEE Intelligent Vehicles Symposium (IV), pp.\u00a01\u20138. IEEE (2023)","DOI":"10.1109\/IV55152.2023.10186763"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-41528-4_29","volume-title":"Computer Aided Verification","author":"C Fan","year":"2016","unstructured":"Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 531\u2013538. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_29"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Fern\u00e1ndez-Duque, D., Montacute, Y.: Untangled: a complete dynamic topological logic. In: Williams, B., Chen, Y., Neville, J. (eds.) Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, 7\u201314 February 2023, pp. 6355\u20136362. AAAI Press (2023). https:\/\/doi.org\/10.1609\/AAAI.V37I5.25782","DOI":"10.1609\/AAAI.V37I5.25782"},{"key":"18_CR16","doi-asserted-by":"publisher","unstructured":"Fern\u00e1ndez-Duque, D., Montacute, Y.: Dynamic tangled derivative logic of metric spaces. In: Wooldridge, M.J., Dy, J.G., Natarajan, S. (eds.) Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pp. 10509\u201310516. AAAI Press (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I9.28920","DOI":"10.1609\/AAAI.V38I9.28920"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1613\/JAIR.1.11256","volume":"63","author":"V Fionda","year":"2018","unstructured":"Fionda, V., Greco, G.: LTL on finite and process traces: complexity results and a practical reasoner. J. Artif. Intell. Res. 63, 557\u2013623 (2018). https:\/\/doi.org\/10.1613\/JAIR.1.11256","journal-title":"J. Artif. Intell. Res."},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: a language for scenario specification and scene generation. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 63\u201378 (2019)","DOI":"10.1145\/3314221.3314633"},{"issue":"4","key":"18_CR19","doi-asserted-by":"publisher","first-page":"3040","DOI":"10.1109\/TIV.2022.3169762","volume":"8","author":"I Hasuo","year":"2022","unstructured":"Hasuo, I., et al.: Goal-aware RSS for complex scenarios via program logic. IEEE Trans. Intell. Veh. 8(4), 3040\u20133072 (2022)","journal-title":"IEEE Trans. Intell. Veh."},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-642-24559-6_28","volume-title":"Formal Methods and Software Engineering","author":"M Hilscher","year":"2011","unstructured":"Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic Manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 404\u2013419. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24559-6_28"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: Spatial logic+ temporal logic=? In: Handbook of Spatial Logics, pp. 497\u2013564. Springer (2007)","DOI":"10.1007\/978-1-4020-5587-4_9"},{"issue":"6","key":"18_CR22","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Rob. 25(6), 1370\u20131381 (2009)","journal-title":"IEEE Trans. Rob."},{"issue":"1","key":"18_CR23","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1146\/annurev-control-060117-104838","volume":"1","author":"H Kress-Gazit","year":"2018","unstructured":"Kress-Gazit, H., Lahijanian, M., Raman, V.: Synthesis for robots: guarantees and feedback for robot behavior. Ann. Rev. Control Rob. Auton. Syst. 1(1), 211\u2013236 (2018)","journal-title":"Ann. Rev. Control Rob. Auton. Syst."},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Li, T., et al.: STSL: a novel spatio-temporal specification language for cyber-physical systems. In: 2020 IEEE 20th International Conference on Software Quality, Reliability and Security (QRS), pp. 309\u2013319. IEEE (2020)","DOI":"10.1109\/QRS51102.2020.00048"},{"issue":"6","key":"18_CR25","doi-asserted-by":"publisher","first-page":"2392","DOI":"10.1007\/s11036-021-01779-5","volume":"26","author":"T Li","year":"2021","unstructured":"Li, T., et al.: Runtime verification of spatio-temporal specification language. Mob. Netw. Appl. 26(6), 2392\u20132406 (2021)","journal-title":"Mob. Netw. Appl."},{"issue":"4","key":"18_CR26","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1109\/9.664155","volume":"43","author":"J Lygeros","year":"2002","unstructured":"Lygeros, J., Godbole, D.N., Sastry, S.: Verified hybrid controllers for automated vehicles. IEEE Trans. Autom. Control 43(4), 522\u2013539 (2002)","journal-title":"IEEE Trans. Autom. Control"},{"key":"18_CR27","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2022.108245","volume":"242","author":"AV Malawade","year":"2022","unstructured":"Malawade, A.V., Yu, S.Y., Hsu, B., Kaeley, H., Karra, A., Al Faruque, M.A.: ROADSCENE2VEC: a tool for extracting and embedding road scene-graphs. Knowl.-Based Syst. 242, 108245 (2022)","journal-title":"Knowl.-Based Syst."},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Mylavarapu, S., Sandhu, M., Vijayan, P., Krishna, K.M., Ravindran, B., Namboodiri, A.: Towards accurate vehicle behaviour classification with multi-relational graph convolutional networks. In: 2020 IEEE Intelligent Vehicles Symposium (IV), pp. 321\u2013327. IEEE (2020)","DOI":"10.1109\/IV47402.2020.9304822"},{"issue":"9","key":"18_CR29","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1038\/s42256-020-0225-y","volume":"2","author":"C Pek","year":"2020","unstructured":"Pek, C., Manzinger, S., Koschi, M., Althoff, M.: Using online verification to prevent autonomous vehicles from causing accidents. Nat. Mach. Intell. 2(9), 518\u2013528 (2020)","journal-title":"Nat. Mach. Intell."},{"issue":"1","key":"18_CR30","doi-asserted-by":"publisher","first-page":"151","DOI":"10.3233\/AIC-150682","volume":"29","author":"E Plaku","year":"2015","unstructured":"Plaku, E., Karaman, S.: Motion planning with temporal-logic specifications: progress and challenges. AI Commun. 29(1), 151\u2013162 (2015)","journal-title":"AI Commun."},{"issue":"6","key":"18_CR31","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.entcs.2006.11.026","volume":"174","author":"A Platzer","year":"2007","unstructured":"Platzer, A.: Towards a hybrid dynamic logic for hybrid dynamic systems. Electron. Notes Theor. Comput. Sci. 174(6), 63\u201377 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer (2018)","DOI":"10.1007\/978-3-319-63588-0"},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"Prior, A.N.: Past, Present and Future. Oxford University Press (1967)","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001"},{"key":"18_CR34","unstructured":"Randell, D.A., Cui, Z., Cohn, A.G., et\u00a0al.: A spatial logic based on regions and connection. KR 92(165-176), 40\u201340 (1992)"},{"key":"18_CR35","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.tcs.2018.05.028","volume":"744","author":"M Schwammberger","year":"2018","unstructured":"Schwammberger, M.: An abstract model for proving safety of autonomous urban traffic. Theoret. Comput. Sci. 744, 143\u2013169 (2018)","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Schwammberger, M., Alves, G.V.: Extending urban multi-lane spatial logic to formalise road junction rules. arXiv preprint arXiv:2110.12583 (2021)","DOI":"10.4204\/EPTCS.348.1"},{"issue":"1","key":"18_CR37","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1146\/annurev-control-060117-105157","volume":"1","author":"W Schwarting","year":"2018","unstructured":"Schwarting, W., Alonso-Mora, J., Rus, D.: Planning and decision-making for autonomous vehicles. Ann. Rev. Control Rob. Auton. Syst. 1(1), 187\u2013210 (2018)","journal-title":"Ann. Rev. Control Rob. Auton. Syst."},{"key":"18_CR38","unstructured":"Shalev-Shwartz, S., Shammah, S., Shashua, A.: On a formal model of safe and scalable self-driving cars. arXiv preprint arXiv:1708.06374 (2017)"},{"issue":"14","key":"18_CR39","doi-asserted-by":"publisher","first-page":"1695","DOI":"10.1177\/0278364911417911","volume":"30","author":"SL Smith","year":"2011","unstructured":"Smith, S.L., T\u016fmov\u00e1, J., Belta, C., Rus, D.: Optimal path planning for surveillance with temporal-logic constraints. Int. J. Rob. Res. 30(14), 1695\u20131708 (2011)","journal-title":"Int. J. Rob. Res."},{"key":"18_CR40","doi-asserted-by":"crossref","unstructured":"Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 147\u2013156 (2019)","DOI":"10.1145\/3302504.3311802"},{"key":"18_CR41","doi-asserted-by":"crossref","unstructured":"Toledo, F., Woodlief, T., Elbaum, S., Dwyer, M.B.: Specifying and monitoring safe driving properties with scene graphs. In: 2024 IEEE International Conference on Robotics and Automation (ICRA), pp. 15577\u201315584. IEEE (2024)","DOI":"10.1109\/ICRA57147.2024.10610973"},{"key":"18_CR42","doi-asserted-by":"publisher","unstructured":"Tuncali, C.E., Fainekos, G., Ito, H., Kapinski, J.: Simulation-based adversarial test generation for autonomous vehicles with machine learning components. In: 2018 IEEE Intelligent Vehicles Symposium, IV 2018, Changshu, Suzhou, China, 26\u201330 June 2018, pp. 1555\u20131562. IEEE (2018). https:\/\/doi.org\/10.1109\/IVS.2018.8500421","DOI":"10.1109\/IVS.2018.8500421"},{"key":"18_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"Formal Methods and Software Engineering","author":"S Wang","year":"2015","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382\u2013399. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_25"},{"key":"18_CR44","doi-asserted-by":"crossref","unstructured":"Wang, X., Liang, A., Sprinkle, J., Johnson, T.T.: Robustness verification for knowledge-based logic of risky driving scenes. In: Future of Information and Communication Conference, pp. 572\u2013585. Springer (2025)","DOI":"10.1007\/978-3-031-84460-7_36"},{"key":"18_CR45","doi-asserted-by":"crossref","unstructured":"Woodlief, T., Toledo, F., Elbaum, S., Dwyer, M.B.: Closing the gap between sensor inputs and driving properties: a scene graph generator for CARLA. In: 2025 IEEE\/ACM 47th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), pp. 29\u201332. IEEE (2025)","DOI":"10.1109\/ICSE-Companion66252.2025.00017"},{"issue":"7","key":"18_CR46","doi-asserted-by":"publisher","first-page":"7941","DOI":"10.1109\/TITS.2021.3074854","volume":"23","author":"SY Yu","year":"2021","unstructured":"Yu, S.Y., Malawade, A.V., Muthirayan, D., Khargonekar, P.P., Al Faruque, M.A.: Scene-graph augmented data-driven risk assessment of autonomous vehicle decisions. IEEE Trans. Intell. Transp. Syst. 23(7), 7941\u20137951 (2021)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"issue":"12","key":"18_CR47","doi-asserted-by":"publisher","first-page":"22971","DOI":"10.1109\/TITS.2022.3196623","volume":"23","author":"Y Yu","year":"2022","unstructured":"Yu, Y., Shan, D., Benderius, O., Berger, C., Kang, Y.: Formally robust and safe trajectory planning and tracking for autonomous vehicles. IEEE Trans. Intell. Transp. Syst. 23(12), 22971\u201322987 (2022)","journal-title":"IEEE Trans. Intell. Transp. Syst."}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:51:21Z","timestamp":1779033081000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}