{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,7]],"date-time":"2026-06-07T04:48:51Z","timestamp":1780807731008,"version":"3.54.1"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,2,8]],"date-time":"2026-02-08T00:00:00Z","timestamp":1770508800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,2,8]],"date-time":"2026-02-08T00:00:00Z","timestamp":1770508800000},"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":["J Sign Process Syst"],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1007\/s11265-026-01986-x","type":"journal-article","created":{"date-parts":[[2026,2,8]],"date-time":"2026-02-08T09:31:56Z","timestamp":1770543116000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Analysis of Lane-Changing Algorithms using Probabilistic Model Checking"],"prefix":"10.1007","volume":"98","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-1789-6514","authenticated-orcid":false,"given":"Muhammad Bilal","family":"Sarwar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,2,8]]},"reference":[{"key":"1986_CR1","doi-asserted-by":"publisher","unstructured":"Anderson, J., Kalra, N., Stanley, K., Sorensen, P., Samaras, C., Oluwatola, T. Autonomous Vehicle Technology: A Guide for Policymakers. RAND Corporation, Santa Monica, CA (2016). https:\/\/doi.org\/10.7249\/rr443-2","DOI":"10.7249\/rr443-2"},{"key":"1986_CR2","doi-asserted-by":"publisher","unstructured":"Reda, M., Onsy, A., Haikal, A.Y., Ghanbari, A. Path planning algorithms in the autonomous driving system: A comprehensive review. Robotics and Autonomous Systems 174, 104630 (2024) https:\/\/doi.org\/10.1016\/j.robot.2024.104630","DOI":"10.1016\/j.robot.2024.104630"},{"issue":"3","key":"1986_CR3","doi-asserted-by":"publisher","first-page":"157","DOI":"10.3328\/tl.2010.02.03.157-173","volume":"2","author":"S Moridpour","year":"2010","unstructured":"Moridpour, S., Sarvi, M., & Rose, G. (2010). Lane changing models: a critical review. Transportation Letters, 2(3), 157\u2013173. https:\/\/doi.org\/10.3328\/tl.2010.02.03.157-173","journal-title":"Transportation Letters"},{"key":"1986_CR4","unstructured":"Steven, P. Autopilot & first responder scenes. [Preliminary Evaluation Report] (2022). https:\/\/static.nhtsa.gov\/odi\/inv\/2021\/INOA-PE21020-1893.PDF"},{"key":"1986_CR5","unstructured":"SAE International Taxonomy and Definitions for Terms Related to Driving Automation Systems for On-Road Motor Vehicles. Technical Report J3016, SAE International (2021). Edition: April 2021. https:\/\/www.sae.org\/standards\/content\/j3016_201806\/"},{"key":"1986_CR6","doi-asserted-by":"publisher","DOI":"10.7249\/RR1478","author":"N Kalra","year":"2016","unstructured":"Kalra, N., & Paddock, S. M. (2016). Driving to safety: How many miles of driving would it take to demonstrate autonomous vehicle reliability? Technical report. RAND Corporation. https:\/\/doi.org\/10.7249\/RR1478","journal-title":"RAND Corporation"},{"key":"1986_CR7","unstructured":"Defense Advanced Research Projects Agency DARPA Urban Challenge. https:\/\/www.darpa.mil\/about-us\/timeline\/darpa-urban-challenge"},{"key":"1986_CR8","doi-asserted-by":"publisher","unstructured":"Wongpiromsarn, T. Formal methods for design and verification of embedded control systems: Application to an autonomous vehicle. PhD thesis, California Institute of Technology (2010). https:\/\/doi.org\/10.7907\/XZ3X-7V51","DOI":"10.7907\/XZ3X-7V51"},{"key":"1986_CR9","doi-asserted-by":"publisher","unstructured":"Hasan, O., Tahar, S. Formal verification methods. In: Khosrow-Pour, M. (ed.) Encyclopedia of Information Science and Technology, pp. 7162\u20137170. IGI Global, Hershey, PA (2015). https:\/\/doi.org\/10.4018\/978-1-4666-5888-2.ch705","DOI":"10.4018\/978-1-4666-5888-2.ch705"},{"key":"1986_CR10","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking. Cambridge, MA: The MIT Press."},{"key":"1986_CR11","doi-asserted-by":"crossref","unstructured":"Puterman, M.L. Markov Decision Processes. Wiley Series in Probability & Mathematical Statistics: Applied Probability & Statistics. John Wiley & Sons, Nashville, TN (1994)","DOI":"10.1002\/9780470316887"},{"key":"1986_CR12","doi-asserted-by":"publisher","unstructured":"Hansson, H., Jonsson, B. A logic for reasoning about time and reliability. In: Formal Aspects of Computing, vol. 6, pp. 512\u2013535. Springer, Heidelberg, Germany (1994). https:\/\/doi.org\/10.1007\/BF01211866","DOI":"10.1007\/BF01211866"},{"issue":"1","key":"1986_CR13","doi-asserted-by":"publisher","first-page":"86","DOI":"10.3141\/1999-10","volume":"1999","author":"A Kesting","year":"2007","unstructured":"Kesting, A., Treiber, M., & Helbing, D. (2007). General lane-changing model mobil for car-following models. Transportation Research Record: Journal of the Transportation Research Board, 1999(1), 86\u201394. https:\/\/doi.org\/10.3141\/1999-10","journal-title":"Transportation Research Record: Journal of the Transportation Research Board"},{"key":"1986_CR14","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., & Parker, D. (2011). PRISM 4.0: Verification of probabilistic real-time systems. Lecture notes in computer scienceComputer Aided Verification (pp. 585\u2013591). Heidelberg, Germany: Springer.","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"1986_CR15","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/bf01386390","volume":"1","author":"EW Dijkstra","year":"1959","unstructured":"Dijkstra, E. W. (1959). A note on two problems in connexion with graphs. Numerische Mathematik, 1(1), 269\u2013271. https:\/\/doi.org\/10.1007\/bf01386390","journal-title":"Numerische Mathematik"},{"issue":"2","key":"1986_CR16","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/tssc.1968.300136","volume":"4","author":"P Hart","year":"1968","unstructured":"Hart, P., Nilsson, N., & Raphael, B. (1968). A formal basis for the heuristic determination of minimum cost paths. IEEE Transactions on Systems Science and Cybernetics, 4(2), 100\u2013107. https:\/\/doi.org\/10.1109\/tssc.1968.300136","journal-title":"IEEE Transactions on Systems Science and Cybernetics"},{"issue":"4","key":"1986_CR17","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1109\/70.508439","volume":"12","author":"LE Kavraki","year":"1996","unstructured":"Kavraki, L. E., Svestka, P., Latombe, J.-C., & Overmars, M. H. (1996). Probabilistic roadmaps for path planning in high-dimensional configuration spaces. IEEE Transactions on Robotics and Automation, 12(4), 566\u2013580. https:\/\/doi.org\/10.1109\/70.508439","journal-title":"IEEE Transactions on Robotics and Automation"},{"key":"1986_CR18","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511546877","volume-title":"Planning Algorithms","author":"SM LaValle","year":"2006","unstructured":"LaValle, S. M. (2006). Planning Algorithms. Cambridge, UK: Cambridge University Press."},{"key":"1986_CR19","doi-asserted-by":"publisher","unstructured":"Karaman, S., Frazzoli, E. Incremental Sampling-based Algorithms for Optimal Motion Planning. arXiv (2010). https:\/\/doi.org\/10.48550\/ARXIV.1005.0416","DOI":"10.48550\/ARXIV.1005.0416"},{"issue":"4","key":"1986_CR20","doi-asserted-by":"publisher","first-page":"173","DOI":"10.3390\/wevj15040173","volume":"15","author":"Z Yang","year":"2024","unstructured":"Yang, Z., Wu, Z., Wang, Y., & Wu, H. (2024). Deep reinforcement learning lane-changing decision algorithm for intelligent vehicles combining lstm trajectory prediction. World Electric Vehicle Journal, 15(4), 173. https:\/\/doi.org\/10.3390\/wevj15040173","journal-title":"World Electric Vehicle Journal"},{"key":"1986_CR21","doi-asserted-by":"publisher","unstructured":"Ghimire, M., Choudhury, M.R., Lagudu, G.S.S.H. Lane Change Decision-Making through Deep Reinforcement Learning. arXiv (2021). https:\/\/doi.org\/10.48550\/ARXIV.2112.14705","DOI":"10.48550\/ARXIV.2112.14705"},{"issue":"4","key":"1986_CR22","doi-asserted-by":"publisher","first-page":"3995","DOI":"10.1109\/tie.2022.3177788","volume":"70","author":"H Tian","year":"2023","unstructured":"Tian, H., Wei, C., Jiang, C., Li, Z., & Hu, J. (2023). Personalized lane change planning and control by imitation learning from drivers. IEEE Transactions on Industrial Electronics, 70(4), 3995\u20134006. https:\/\/doi.org\/10.1109\/tie.2022.3177788","journal-title":"IEEE Transactions on Industrial Electronics"},{"key":"1986_CR23","doi-asserted-by":"publisher","unstructured":"Shi, J., Zhang, T., Zhan, J., Chen, S., Xin, J., Zheng, N. Efficient lane-changing behavior planning via reinforcement learning with imitation learning initialization. In: 2023 IEEE Intelligent Vehicles Symposium (IV), pp. 1\u20138. IEEE, Anchorage, AK (2023). https:\/\/doi.org\/10.1109\/iv55152.2023.10186577","DOI":"10.1109\/iv55152.2023.10186577"},{"key":"1986_CR24","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. IEEE, Xi\u2019an, China (2017). https:\/\/doi.org\/10.1109\/coase.2017.8256223","DOI":"10.1109\/coase.2017.8256223"},{"issue":"1","key":"1986_CR25","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/s11036-023-02089-8","volume":"28","author":"X Yang","year":"2023","unstructured":"Yang, X., Wei, Y., Shi, L., & Chen, L. (2023). Applying probabilistic model checking to path planning for a smart multimodal transportation system using iot sensor data. Mobile Networks and Applications, 28(1), 382\u2013393. https:\/\/doi.org\/10.1007\/s11036-023-02089-8","journal-title":"Mobile Networks and Applications"},{"key":"1986_CR26","doi-asserted-by":"publisher","unstructured":"Dhonthi, A., Schischka, N., Hahn, E.M., Hashemi, V. Autonomous Vehicles Path Planning under Temporal Logic Specifications. arXiv (2024). https:\/\/doi.org\/10.48550\/ARXIV.2410.07845","DOI":"10.48550\/ARXIV.2410.07845"},{"key":"1986_CR27","doi-asserted-by":"publisher","unstructured":"Chen, B., Li, T. Formal modeling and verification of autonomous driving scenario. In: 2021 IEEE International Conference on Information Communication and Software Engineering (ICICSE), pp. 313\u2013321. IEEE, Chengdu, China (2021). https:\/\/doi.org\/10.1109\/icicse52190.2021.9404128","DOI":"10.1109\/icicse52190.2021.9404128"},{"key":"1986_CR28","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Logics of Programs, pp. 52\u201371. Springer, Berlin\/Heidelberg (2005)","DOI":"10.1007\/BFb0025774"},{"key":"1986_CR29","unstructured":"PRISM Model Checker Manual. http:\/\/www.prismmodelchecker.org\/manual"},{"key":"1986_CR30","doi-asserted-by":"publisher","unstructured":"Khan, U., Basaras, P., Schmidt-Thieme, L., Nanopoulos, A., Katsaros, D. Analyzing cooperative lane change models for connected vehicles. In: 2014 IEEE International Conference on Connected Vehicles and Expo (ICCVE), pp. 565\u2013570. IEEE, Vienna, Austria (2014). https:\/\/doi.org\/10.1109\/ICCVE.2014.136","DOI":"10.1109\/ICCVE.2014.136"},{"key":"1986_CR31","doi-asserted-by":"publisher","unstructured":"Abtahi, S.M., Azim, A. Algorithmic Approaches to Enhance Safety in Autonomous Vehicles: Minimizing Lane Changes and Merging. arXiv (2025). https:\/\/doi.org\/10.48550\/ARXIV.2506.15026","DOI":"10.48550\/ARXIV.2506.15026"},{"issue":"5","key":"1986_CR32","doi-asserted-by":"publisher","first-page":"918","DOI":"10.3390\/electronics14050918","volume":"14","author":"Z Wang","year":"2025","unstructured":"Wang, Z., Jiang, M., Gu, S., Gu, Y., & Wang, J. (2025). Enhancing lane change safety and efficiency in autonomous driving through improved reinforcement learning for highway decision-making. Electronics, 14(5), 918. https:\/\/doi.org\/10.3390\/electronics14050918","journal-title":"Electronics"}],"container-title":["Journal of Signal Processing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11265-026-01986-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11265-026-01986-x","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11265-026-01986-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,8]],"date-time":"2026-02-08T09:31:59Z","timestamp":1770543119000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11265-026-01986-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,8]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["1986"],"URL":"https:\/\/doi.org\/10.1007\/s11265-026-01986-x","relation":{},"ISSN":["1939-8018","1939-8115"],"issn-type":[{"value":"1939-8018","type":"print"},{"value":"1939-8115","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,8]]},"assertion":[{"value":"10 March 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 November 2025","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 January 2026","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2026","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics Approval and Consent to Participate"}},{"value":"Not applicable.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for Publication"}}],"article-number":"16"}}