{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T02:48:11Z","timestamp":1782874091060,"version":"3.54.5"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227515","type":"print"},{"value":"9783032227522","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-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T00:00:00Z","timestamp":1776297600000},"content-version":"vor","delay-in-days":105,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22752-2_31","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T21:51:35Z","timestamp":1776289895000},"page":"597-619","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7840-1459","authenticated-orcid":false,"given":"Lukas","family":"K\u00f6nig","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-6989-7527","authenticated-orcid":false,"given":"Christian","family":"Schildw\u00e4chter","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6353-227X","authenticated-orcid":false,"given":"Michaela","family":"Klauck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2144-6215","authenticated-orcid":false,"given":"Christian","family":"Heinzemann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"31_CR1","unstructured":"Abeywickrama, D.B., Mamei, M., Zambonelli, F.: Engineering collectives of self-driving vehicles: The sota approach. In: Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III 8. pp. 79\u201393. Springer (2018)"},{"key":"31_CR2","doi-asserted-by":"publisher","unstructured":"Abeywickrama, D.B., Zambonelli, F.: Model checking goal-oriented requirements for self-adaptive systems. In: 2012 IEEE 19th International Conference and Workshops on Engineering of Computer-Based Systems. pp. 33\u201342 (2012). https:\/\/doi.org\/10.1109\/ECBS.2012.30","DOI":"10.1109\/ECBS.2012.30"},{"key":"31_CR3","doi-asserted-by":"publisher","unstructured":"Arcile, J., Devillers, R.R., Klaudel, H.: Verifcar: a framework for modeling and model checking communicating autonomous vehicles. Auton. Agents Multi Agent Syst. 33(3), 353\u2013381 (2019). https:\/\/doi.org\/10.1007\/S10458-019-09409-X, https:\/\/doi.org\/10.1007\/s10458-019-09409-x","DOI":"10.1007\/S10458-019-09409-X"},{"key":"31_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge, MA, USA (2008)"},{"key":"31_CR5","doi-asserted-by":"publisher","unstructured":"Bakar, N.A., Selamat, A.: Agent systems verification: systematic literaturereview and mapping. Applied Intelligence 48(5), 1251\u20131274 (May 2018). https:\/\/doi.org\/10.1007\/s10489-017-1112-z,https:\/\/doi.org\/10.1007\/s10489-017-1112-z","DOI":"10.1007\/s10489-017-1112-z"},{"key":"31_CR6","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems. pp. 125\u2013126. QEST 2006, IEEE Computer Society, Los Alamitos, CA, USA (Sep 2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv Symbolic Model Checker. In: Computer Aided Verification. CAV 2014 (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Chu, T., Kalabi\u0107, U.: Model-based deep reinforcement learning for cacc in mixed-autonomy vehicle platoon. In: 2019 IEEE 58th Conference on Decision and Control (CDC). pp. 4079\u20134084. IEEE (2019)","DOI":"10.1109\/CDC40024.2019.9030110"},{"key":"31_CR9","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, strong, and strong cyclic planning via symbolic model checking. Artificial Intelligence 147(1), 35\u201384 (2003). https:\/\/doi.org\/10.1016\/S0004-3702(02)00374-0, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0004370202003740, planning with Uncertainty and Incomplete Information","DOI":"10.1016\/S0004-3702(02)00374-0"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M.: Conformant planning via symbolic model checking. J.Artif. Int. Res. 13(1), 305\u2013338 (Dec 2000)","DOI":"10.1613\/jair.774"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Committee, O.R.A.D.: Taxonomy and definitions for terms related to driving automation systems for on-road motor vehicles (2021), https:\/\/doi.org\/10.4271\/J3016_202104, accessed: 2026-01-20","DOI":"10.4271\/J3016_202104"},{"key":"31_CR12","doi-asserted-by":"publisher","unstructured":"Committee, O.R.A.D.O.: Definitions for Terms Related to Automated Driving Systems Reference Architecture, Fig. 1 (Mar 2022). https:\/\/doi.org\/10.4271\/J3131_202203","DOI":"10.4271\/J3131_202203"},{"key":"31_CR13","unstructured":"Coulter, C.: Implementation of the pure pursuit path tracking algorithm. Tech. rep., Robotics Institute Carnegie Mellon University (1992), https:\/\/api.semanticscholar.org\/CorpusID:62550799"},{"key":"31_CR14","doi-asserted-by":"publisher","unstructured":"Cubuktepe, M., Jansen, N., Alshiekh, M., Topcu, U.: Synthesis of provably correct autonomy protocols for shared control. IEEE Transactions on Automatic Control 66(7), 3251\u20133258 (Jul 2021). https:\/\/doi.org\/10.1109\/TAC.2020.3018029","DOI":"10.1109\/TAC.2020.3018029"},{"key":"31_CR15","doi-asserted-by":"publisher","unstructured":"Daw, Z., Cleaveland, R., Vetter, M.: Integrating model checking and uml based model-driven development for embedded systems. In: Automated Verification of Critical Systems 2013. Electronic Communications of the EASST, vol.\u00a066 (2013). https:\/\/doi.org\/10.14279\/tuj.eceasst.66.888","DOI":"10.14279\/tuj.eceasst.66.888"},{"key":"31_CR16","doi-asserted-by":"crossref","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.) Computer Aided Verification. pp. 592\u2013600. Springer International Publishing, Cham (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"Dinneweth, J., Boubezoul, A., Mandiau, R., Espi\u00e9, S.: Multi-agent reinforcement learning for autonomous vehicles: A survey. Autonomous Intelligent Systems 2(1), \u00a027 (2022)","DOI":"10.1007\/s43684-022-00045-z"},{"key":"31_CR18","doi-asserted-by":"publisher","unstructured":"Eckardt, T., Heinzemann, C., Henkler, S., Hirsch, M., Priesterjahn, C., Sch\u00e4fer, W.: Modeling and verifying dynamic communication structures based on graph transformations. Computer Science - Research and Development 28(1), 3\u201322 (Feb 2013). https:\/\/doi.org\/10.1007\/s00450-011-0184-y, published online July 2011","DOI":"10.1007\/s00450-011-0184-y"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: \"A Mathematical Introduction to Logic\". Academic Press, Boston, MA, USA, 2. edn. (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"31_CR20","doi-asserted-by":"publisher","unstructured":"Etigowni, S., Hossain-McKenzie, S., Kazerooni, M., Davis, K., Zonouz, S.: Crystal (ball): I look at physics and predict control flow! just-ahead-of-time controller recovery. In: Proceedings of the 34th Annual Computer Security Applications Conference. p. 553\u2013565. ACSAC \u201918, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3274694.3274724, https:\/\/doi.org\/10.1145\/3274694.3274724","DOI":"10.1145\/3274694.3274724"},{"key":"31_CR21","doi-asserted-by":"publisher","unstructured":"Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45(2), 343 \u2013 352 (2009). https:\/\/doi.org\/10.1016\/j.automatica.2008.08.008","DOI":"10.1016\/j.automatica.2008.08.008"},{"key":"31_CR22","doi-asserted-by":"crossref","unstructured":"Feiler, J., Hoffmann, S., Diermeyer, F.: Concept of a control center for an automated vehicle fleet. In: 2020 IEEE 23rd international conference on intelligent transportation systems (ITSC). pp.\u00a01\u20136. IEEE (2020)","DOI":"10.1109\/ITSC45102.2020.9294411"},{"key":"31_CR23","doi-asserted-by":"publisher","unstructured":"Gardner, R.W., Genin, D., McDowell, R., Rouff, C., Saksena, A., Schmidt, A.: Probabilistic model checking of the next-generation airborne collision avoidance system. In: 2016 IEEE\/AIAA 35th Digital Avionics Systems Conference (DASC). pp. 1\u201310 (2016). https:\/\/doi.org\/10.1109\/DASC.2016.7777963","DOI":"10.1109\/DASC.2016.7777963"},{"key":"31_CR24","unstructured":"Gerking, C., Dziwok, S., Heinzemann, C., Sch\u00e4fer, W.: Domain-specific model checking for cyber-physical systems. In: 12th Workshop on Model-Driven Engineering, Verification and Validation. pp. 18\u201327. MoDeVVa 2015, CEUR-WS.org Vol-1514, Ottawa (Sep 2015)"},{"key":"31_CR25","doi-asserted-by":"publisher","unstructured":"Haslum, P., Lipovetzky, N., Magazzeni, D., Muise, C.: An Introduction to the Planning Domain Definition Language. Springer Cham, 1st edn. (2019). https:\/\/doi.org\/10.1007\/978-3-031-01584-7","DOI":"10.1007\/978-3-031-01584-7"},{"key":"31_CR26","doi-asserted-by":"publisher","unstructured":"Heinzemann, C., Lange, R.: vTSL \u2013 a formally verifiable dsl for specifying robot tasks. In: 2018 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS). pp. 8308\u20138314. IROS\u201918, IEEE Computer Society, Madrid, Spain (2018). https:\/\/doi.org\/10.1109\/IROS.2018.8593559","DOI":"10.1109\/IROS.2018.8593559"},{"key":"31_CR27","doi-asserted-by":"publisher","unstructured":"Helmert, M.: The fast downward planning system. Journal Artificial Intelligence Research (JAIR) 26, 191\u2013246 (2006). https:\/\/doi.org\/10.1613\/jair.1705","DOI":"10.1613\/jair.1705"},{"key":"31_CR28","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J.: The model checker spin. Software Engineering, IEEE Transactions on 23(5), 279 \u2013295 (may 1997). https:\/\/doi.org\/10.1109\/32.588521","DOI":"10.1109\/32.588521"},{"key":"31_CR29","doi-asserted-by":"crossref","unstructured":"Huang, Z., Li, B., Du, D., Li, Q.: A model checking based approach to detect safety-critical adversarial examples on autonomous driving systems. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) Theoretical Aspects of Computing \u2013 ICTAC 2022. pp. 238\u2013254. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-031-17715-6_16"},{"key":"31_CR30","doi-asserted-by":"crossref","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, USA (2004), page 175","DOI":"10.1017\/CBO9780511810275"},{"key":"31_CR31","doi-asserted-by":"crossref","unstructured":"Jin, W., Du, H., Zhao, B., Tian, X., Shi, B., Yang, G.: A comprehensive survey on multi-agent cooperative decision-making: Scenarios, approaches, challenges and perspectives (2025), https:\/\/arxiv.org\/abs\/2503.13415","DOI":"10.2139\/ssrn.5106265"},{"key":"31_CR32","doi-asserted-by":"publisher","unstructured":"Johnson, B., Kress-Gazit, H.: Probabilistic guarantees for high-level robotbehavior in the presence of sensor error. Autonomous Robots 33(3),309\u2013321 (Oct 2012). https:\/\/doi.org\/10.1007\/s10514-012-9301-4","DOI":"10.1007\/s10514-012-9301-4"},{"key":"31_CR33","doi-asserted-by":"publisher","unstructured":"Johnson, B., Kress-Gazit, H.: Analyzing and revising high-level robot behaviors under actuator error. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems. pp. 741\u2013748. IROS\u201913, IEEE Computer Society (Nov 2013). https:\/\/doi.org\/10.1109\/IROS.2013.6696434","DOI":"10.1109\/IROS.2013.6696434"},{"key":"31_CR34","doi-asserted-by":"crossref","unstructured":"Kamali, M., Dennis, L.A., McAree, O., Fisher, M., Veres, S.M.: Formal verification of autonomous vehicle platooning. Science of computer programming 148, 88\u2013106 (2017)","DOI":"10.1016\/j.scico.2017.05.006"},{"key":"31_CR35","doi-asserted-by":"publisher","unstructured":"Keating, D., McInnes, A., Hayes, M.: An industrial application of model checking to a vessel control system. In: 2011 Sixth IEEE International Symposium on Electronic Design, Test and Application. pp. 83\u201388 (2011). https:\/\/doi.org\/10.1109\/DELTA.2011.24","DOI":"10.1109\/DELTA.2011.24"},{"key":"31_CR36","doi-asserted-by":"publisher","unstructured":"K\u00f6nig, L., Heinzemann, C., Klauck, M., Heinzemann, C.: Supplementary material for \"driving by disproof: A model checking approach to fleet coordination\" (Aug 2025). https:\/\/doi.org\/10.5281\/zenodo.16738026","DOI":"10.5281\/zenodo.16738026"},{"key":"31_CR37","doi-asserted-by":"publisher","unstructured":"K\u00f6nig, L., Heinzemann, C., Klauck, M., Heinzemann, C.: Artifact for \"driving by disproof: A model checking approach to fleet coordination\" (Jan 2026). https:\/\/doi.org\/10.5281\/zenodo.18171064","DOI":"10.5281\/zenodo.18171064"},{"key":"31_CR38","doi-asserted-by":"crossref","unstructured":"K\u00f6nig, L., Heinzemann, C., Griggio, A., Klauck, M., Cimatti, A., Henze, F., Tonetta, S., K\u00fcperkoch, S., Fassbender, D., Hanselmann, M.: Towards safe autonomous driving: Model checking a behavior planner during development. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 44\u201365. Springer Nature Switzerland, Cham (2024)","DOI":"10.1007\/978-3-031-57249-4_3"},{"key":"31_CR39","unstructured":"K\u00f6nig, L., Henze, F., Klauck, M., Heinzemann, C., Griggio, A., Cimatti, A., Tonetta, S.: Formally verifying a behavior planner: Balancing efficiency and precision. IEEE Transactions on Intelligent Vehicles Under Review(x), xx\u2013yy (2025). https:\/\/doi.org\/xxdoixx"},{"key":"31_CR40","doi-asserted-by":"publisher","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactivemission and motion planning. IEEE Transactions on Robotics 25(6),1370\u20131381 (Dec 2009). https:\/\/doi.org\/10.1109\/TRO.2009.2030225","DOI":"10.1109\/TRO.2009.2030225"},{"key":"31_CR41","doi-asserted-by":"publisher","unstructured":"Krook, J., Kianfar, R., Fabian, M.: Formal synthesis of safe stop tactical planners for an automated vehicle. IFAC-PapersOnLine 53(4), 445\u2013452 (2020). https:\/\/doi.org\/10.1016\/j.ifacol.2021.04.059, 15th IFAC Workshop on Discrete Event Systems WODES 2020 \u2013 Rio de Janeiro, Brazil, 11-13 November 2020","DOI":"10.1016\/j.ifacol.2021.04.059"},{"key":"31_CR42","doi-asserted-by":"publisher","unstructured":"Krook, J., Svensson, L., Li, Y., Feng, L., Fabian, M.: Design and formal verification of a safe stop supervisor for an automated vehicle. In: 2019 International Conference on Robotics and Automation (ICRA). pp. 5607\u20135613 (2019). https:\/\/doi.org\/10.1109\/ICRA.2019.8793636","DOI":"10.1109\/ICRA.2019.8793636"},{"key":"31_CR43","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911). LNCS, vol.\u00a06806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"31_CR44","unstructured":"Leurent, E.: An environment for autonomous driving decision-making. https:\/\/github.com\/eleurent\/highway-env (2018)"},{"key":"31_CR45","doi-asserted-by":"crossref","unstructured":"Liu, J., Wang, Z., Hang, P., Sun, J.: Delay-aware multi-agent reinforcement learning for cooperative adaptive cruise control with model-based stability enhancement. arXiv preprint arXiv:2404.15696 (2024)","DOI":"10.1109\/ITSC58415.2024.10919632"},{"key":"31_CR46","doi-asserted-by":"publisher","unstructured":"Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: A survey. ACM Comput. Surv. 52(5) (2019). https:\/\/doi.org\/10.1145\/3342355, https:\/\/doi.org\/10.1145\/3342355","DOI":"10.1145\/3342355"},{"key":"31_CR47","doi-asserted-by":"publisher","unstructured":"Ma, Y., Sun, C., Chen, J., Cao, D., Xiong, L.: Verification and validation methods for decision-making and planning of automated vehicles: A review. IEEE Transactions on Intelligent Vehicles 7(3), 480\u2013498 (2022). https:\/\/doi.org\/10.1109\/TIV.2022.3196396","DOI":"10.1109\/TIV.2022.3196396"},{"key":"31_CR48","doi-asserted-by":"crossref","unstructured":"Mariani, S., Cabri, G., Zambonelli, F.: Coordination of autonomous vehicles: taxonomy and survey. ACM Computing Surveys (CSUR) 54(1), 1\u201333 (2021)","DOI":"10.1145\/3431231"},{"key":"31_CR49","doi-asserted-by":"publisher","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 (2023).https:\/\/doi.org\/10.1016\/j.automatica.2022.110692","DOI":"10.1016\/j.automatica.2022.110692"},{"key":"31_CR50","doi-asserted-by":"crossref","unstructured":"Provan, G.: Formal methods for autonomous vehicles. IT Professional 26(1), 50\u201356 (2024)","DOI":"10.1109\/MITP.2024.3356158"},{"key":"31_CR51","doi-asserted-by":"publisher","unstructured":"Rao, A., Wang, Y.: Formal verification of autonomous vehicles: Bridging the gap between model-based design and model checking. SAE Int. J. Adv. & Curr. Prac. in Mobility 6(2), 814\u2013826 (2024).https:\/\/doi.org\/10.4271\/2023-01-0116","DOI":"10.4271\/2023-01-0116"},{"key":"31_CR52","doi-asserted-by":"publisher","unstructured":"Rashid, A., Siddique, U., Hasan, O.: Formal verification of platoon control strategies. In: Johnsen, E.B., Schaefer, I. (eds.) Software Engineering and Formal Methods - 16th International Conference, SEFM 2018, Held as Part of STAF 2018, Toulouse, France, June 27-29, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10886, pp. 223\u2013238. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92970-5_14, https:\/\/doi.org\/10.1007\/978-3-319-92970-5_14","DOI":"10.1007\/978-3-319-92970-5_14"},{"key":"31_CR53","doi-asserted-by":"publisher","unstructured":"Riedmaier, S., Ponn, T., Ludwig, D., Schick, B., Diermeyer, F.: Survey on scenario-based safety assessment of automated vehicles. IEEE Access 8, 87456\u201387477 (2020). https:\/\/doi.org\/10.1109\/ACCESS.2020.2993730","DOI":"10.1109\/ACCESS.2020.2993730"},{"key":"31_CR54","doi-asserted-by":"publisher","unstructured":"Schmidt, \u00c1., Varr\u00f3, D.: Checkvml: A tool for model checking visual modeling languages. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003 - The Unified Modeling Language. Modeling Languages and Applications, Lecture Notes in Computer Science, vol.\u00a02863, pp. 92\u201395. Springer Berlin Heidelberg (Oct 2003). https:\/\/doi.org\/10.1007\/978-3-540-45221-8_8","DOI":"10.1007\/978-3-540-45221-8_8"},{"key":"31_CR55","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-030-27008-7_9","volume-title":"Formal Methods for Industrial Critical Systems","author":"Y Selvaraj","year":"2019","unstructured":"Selvaraj, Y., Ahrendt, W., Fabian, M.: Verification of decision making software in an autonomous vehicle: An industrial case study. In: Larsen, K.G., Willemse, T. (eds.) Formal Methods for Industrial Critical Systems. pp. 143\u2013159. Springer International Publishing, Cham (2019)"},{"key":"31_CR56","doi-asserted-by":"crossref","unstructured":"Siegel, M.: The sense-think-act paradigm revisited. In: 1st International Workshop on Robotic Sensing, 2003. ROSE\u201903. pp. 5\u2013pp. IEEE (2003)","DOI":"10.1109\/ROSE.2003.1218700"},{"key":"31_CR57","unstructured":"Soni, A., Hu, H.: Formation control for a fleet of autonomous ground vehicles: A survey. Robotics 7(4), \u00a067 (2018)"},{"key":"31_CR58","doi-asserted-by":"publisher","unstructured":"Torre\u00f1o, A., Onaindia, E., Komenda, A., \u0160tolba, M.: Cooperative multi-agent planning: A survey. ACM Comput. Surv. 50(6) (Nov 2017). https:\/\/doi.org\/10.1145\/3128584, https:\/\/doi.org\/10.1145\/3128584","DOI":"10.1145\/3128584"},{"key":"31_CR59","doi-asserted-by":"publisher","unstructured":"Tran, S.C., Pontelli, E., Balduccini, M., Schaub, T.: Answer set planning: A survey. Theory and Practice of Logic Programming 23(1), 226\u2013298 (2023). https:\/\/doi.org\/10.1017\/S1471068422000072","DOI":"10.1017\/S1471068422000072"},{"key":"31_CR60","doi-asserted-by":"publisher","unstructured":"Van, T.N., Geihs, K.: Formal verification of multi-agent plans for vehicle platooning. In: Vinh, P.C., Rakib, A. (eds.) Context-Aware Systems and Applications, and Nature of Computation and Communication - 9th EAI International Conference, ICCASA 2020, and 6th EAI International Conference, ICTCC 2020, Thai Nguyen, Vietnam, November 26-27, 2020, Proceedings. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol.\u00a0343, pp. 3\u201315. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-67101-3_1, https:\/\/doi.org\/10.1007\/978-3-030-67101-3_1","DOI":"10.1007\/978-3-030-67101-3_1"},{"key":"31_CR61","doi-asserted-by":"crossref","unstructured":"Van\u00a0Arem, B., Van\u00a0Driel, C.J., Visser, R.: The impact of cooperative adaptive cruise control on traffic-flow characteristics. IEEE Transactions on intelligent transportation systems 7(4), 429\u2013436 (2006)","DOI":"10.1109\/TITS.2006.884615"},{"key":"31_CR62","doi-asserted-by":"crossref","unstructured":"Wang, Z., Wu, G., Barth, M.J.: A review on cooperative adaptive cruise control (cacc) systems: Architectures, controls, and applications. In: 2018 21st International Conference on Intelligent Transportation Systems (ITSC). pp. 2884\u20132891. IEEE (2018)","DOI":"10.1109\/ITSC.2018.8569947"},{"key":"31_CR63","doi-asserted-by":"crossref","unstructured":"Waqas, M., Murtaza, M.A., Nuzzo, P., Ioannou, P.: Correct-by-construction design of adaptive cruise control with control barrier functions under safety and regulatory constraints. In: 2022 American Control Conference (ACC). pp. 5140\u20135146. IEEE (2022)","DOI":"10.23919\/ACC53348.2022.9867464"},{"key":"31_CR64","unstructured":"Werling, M., Faller, R., Betz, W., Straub, D.: Safety integrity framework for automated driving (2025), https:\/\/arxiv.org\/abs\/2503.20544"},{"key":"31_CR65","doi-asserted-by":"crossref","unstructured":"Waqas, M., Murtaza, M.A., Nuzzo, P., Ioannou, P.: Correct-by-construction design of adaptive cruise control with control barrier functions under safety and regulatory constraints. In: 2022 American Control Conference (ACC). pp. 5140\u20135146. IEEE (2022)","DOI":"10.23919\/ACC53348.2022.9867464"},{"issue":"4","key":"31_CR66","doi-asserted-by":"publisher","first-page":"936","DOI":"10.1109\/TRO.2018.2830353","volume":"34","author":"KW Wong","year":"2018","unstructured":"Wong, K.W., Ehlers, R., Kress-Gazit, H.: Resilient, provably-correct, andhigh-level robot behaviors. IEEE Transactions on Robotics 34(4),936\u2013952 (Aug 2018). https:\/\/doi.org\/10.1109\/TRO.2018.2830353","journal-title":"IEEE Transactions on Robotics"},{"key":"31_CR67","doi-asserted-by":"crossref","unstructured":"Xu, X., Grizzle, J.W., Tabuada, P., Ames, A.D.: Correctness guarantees for the composition of lane keeping and adaptive cruise control. IEEE Transactions on Automation Science and Engineering 15(3), 1216\u20131229 (2017)","DOI":"10.1109\/TASE.2017.2760863"},{"key":"31_CR68","doi-asserted-by":"crossref","unstructured":"Yan, S., K\u00f6nig, L., Burgard, W.: Agent-agnostic centralized training for decentralized multi-agent cooperative driving (2024), https:\/\/arxiv.org\/abs\/2403.11914","DOI":"10.1109\/IROS58592.2024.10801946"},{"key":"31_CR69","doi-asserted-by":"publisher","unstructured":"Zita, A., Mohajerani, S., Fabian, M.: Application of formal verification to the lane change module of an autonomous vehicle. In: 2017 13th IEEE Conference on Automation Science and Engineering (CASE). pp. 932\u2013937 (2017).https:\/\/doi.org\/10.1109\/COASE.2017.8256223","DOI":"10.1109\/COASE.2017.8256223"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22752-2_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T02:28:01Z","timestamp":1782872881000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22752-2_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227515","9783032227522"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22752-2_31","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":"16 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}