{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T19:53:12Z","timestamp":1790538792642,"version":"4.1.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T00:00:00Z","timestamp":1556668800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Auton Agent Multi-Agent Syst"],"published-print":{"date-parts":[[2019,5]]},"DOI":"10.1007\/s10458-019-09409-x","type":"journal-article","created":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T12:05:00Z","timestamp":1556885100000},"page":"353-381","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["VerifCar: a framework for modeling and model checking communicating autonomous vehicles"],"prefix":"10.1007","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9979-3829","authenticated-orcid":false,"given":"Johan","family":"Arcile","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Raymond","family":"Devillers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hanna","family":"Klaudel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,5,3]]},"reference":[{"issue":"1","key":"9409_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., & Dill, D. (1993). Model checking in dense real-time. Information and Computation, 104(1), 2\u201334.","journal-title":"Information and Computation"},{"key":"9409_CR2","unstructured":"Alur, R., & Dill, D. (1990). Automata for modelling real-time systems. In Proceedings of the international colloquium on automata, languages and programming (ICALP\u201990), volume 443 of LNCS (pp. 322\u2013335). Springer."},{"issue":"2","key":"9409_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., & Dill, D. (1994). A theory of timed automata. Theoretical Computer Science, 126(2), 183\u2013235.","journal-title":"Theoretical Computer Science"},{"key":"9409_CR4","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-62410-5_21","volume-title":"Distributed computing and artificial intelligence, 14th international conference","author":"J Arcile","year":"2018","unstructured":"Arcile, J., Devillers, R., Klaudel, H., Klaudel, W., & Wo\u017ana-Szcze\u015bniak, B. (2018). Modeling and checking robustness of communicating autonomous vehicles. In S. Omatu, S. Rodr\u00edguez, G. Villarrubia, P. Faria, P. Sitek, & J. Prieto (Eds.), Distributed computing and artificial intelligence, 14th international conference (pp. 173\u2013180). Berlin: Springer."},{"key":"9409_CR5","volume-title":"Multi-agent systems and agreement technologies","author":"J Arcile","year":"2018","unstructured":"Arcile, J., Sobieraj, J., Klaudel, H., & Hutzler, G. (2018). Combination of simulation and model-checking for the analysis of autonomous vehicles\u2019 behaviors: A case study. In F. Belardinelli & E. Argente (Eds.), Multi-agent systems and agreement technologies. Berlin: Springer."},{"key":"9409_CR6","unstructured":"Bai, F., & Krishnan, H. (September, 2006). Reliability analysis of DSRC wireless communication for vehicle safety applications. In IEEE intelligent transportation systems conference (pp. 355\u2013362)."},{"key":"9409_CR7","doi-asserted-by":"crossref","unstructured":"Bilstrup, K., Uhlemann, E., Strom, E.\u00a0G., & Bilstrup, U. (September, 2008). Evaluation of the IEEE 802.11p MAC method for vehicle-to-vehicle communication. In IEEE vehicular technology conference (pp. 1\u20135).","DOI":"10.1109\/VETECF.2008.446"},{"issue":"1","key":"9409_CR8","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1109\/MCOM.2006.1580935","volume":"44","author":"S Biswas","year":"2006","unstructured":"Biswas, S., Tatchikou, R., & Dion, F. (2006). Vehicle-to-vehicle wireless communication protocols for enhancing highway traffic safety. IEEE Communications Magazine, 44(1), 74\u201382.","journal-title":"IEEE Communications Magazine"},{"key":"9409_CR9","doi-asserted-by":"crossref","unstructured":"Blokpoel, R.\u00a0J., Krajzewicz, D., & Nippold, R. (2010) Unambiguous metrics for evaluation of traffic networks. In IEEE intelligent transportation systems conference (pp. 1277\u20131282).","DOI":"10.1109\/ITSC.2010.5625135"},{"key":"9409_CR10","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge: MIT Press."},{"key":"9409_CR11","doi-asserted-by":"crossref","unstructured":"Devillers, R., & Klaudel, H. (2016). Abstraction strategies for computing travelling or looping durations in networks of timed automata. In M. Fr\u00e4nzle & N. Markey (Eds.), 14th international conference, FORMATS 2016, proceedings, volume 9884 of LNCS (pp. 140\u2013156). Springer.","DOI":"10.1007\/978-3-319-44878-7_9"},{"key":"9409_CR12","first-page":"995","volume-title":"Handbook of theoretical computer science","author":"EA Emerson","year":"1990","unstructured":"Emerson, E. A. (1990). Temporal and modal logic. In J. van Leeuwen (Ed.), Handbook of theoretical computer science (Vol. b, pp. 995\u20131072). Cambridge, MA: MIT Press."},{"key":"9409_CR13","doi-asserted-by":"crossref","unstructured":"Foughali, M., Berthomieu, B., Dal\u00a0Zilio, S., Ingrand, F., & Mallet, A. (November 2016). Model checking real-time properties on the functional layer of autonomous robots. In International conference on formal engineering methods (ICFEM 2016), Tokyo, Japan.","DOI":"10.1007\/978-3-319-47846-3_24"},{"issue":"1","key":"9409_CR14","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/MITS.2011.940472","volume":"3","author":"A Furda","year":"2011","unstructured":"Furda, A., & Vlacic, L. (2011). Enabling safe autonomous driving in real-world city traffic using multiple criteria decision making. IEEE Intelligent Transportation Systems Magazine, 3(1), 4\u201317.","journal-title":"IEEE Intelligent Transportation Systems Magazine"},{"issue":"3","key":"9409_CR15","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1109\/TITS.2010.2046037","volume":"11","author":"S Glaser","year":"2010","unstructured":"Glaser, S., Vanholme, B., Mammar, S., Gruyer, D., & Nouveliere, L. (2010). Maneuver-based trajectory planning for highly autonomous vehicles on real road with traffic and driver interaction. IEEE Transactions on Intelligent Transportation Systems, 11(3), 589\u2013606.","journal-title":"IEEE Transactions on Intelligent Transportation Systems"},{"key":"9409_CR16","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/j.scico.2017.05.006","volume":"148","author":"M Kamali","year":"2017","unstructured":"Kamali, M., Dennis, L. A., McAree, O., Fisher, M., & Veres, S. M. (2017). Formal verification of autonomous vehicle platooning. Science of Computer Programming, 148, 88\u2013106.","journal-title":"Science of Computer Programming"},{"key":"9409_CR17","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1016\/j.trc.2015.09.011","volume":"60","author":"C Katrakazas","year":"2015","unstructured":"Katrakazas, C., Quddus, M., Chen, W.-H., & Deka, L. (2015). Real-time motion planning methods for autonomous on-road driving: State-of-the-art and future research directions. Transportation Research Part C: Emerging Technologies, 60, 416\u2013442.","journal-title":"Transportation Research Part C: Emerging Technologies"},{"key":"9409_CR18","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-662-46681-0_15","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"S Kong","year":"2015","unstructured":"Kong, S., Gao, S., Chen, W., & Clarke, E. (2015). dreach: $$\\delta $$-reachability analysis for hybrid systems. In C. Baier & C. Tinelli (Eds.), Tools and algorithms for the construction and analysis of systems (pp. 200\u2013205). Berlin: Springer."},{"issue":"5","key":"9409_CR19","doi-asserted-by":"publisher","first-page":"1105","DOI":"10.1109\/TCST.2008.2012116","volume":"17","author":"Y Kuwata","year":"2009","unstructured":"Kuwata, Y., Teo, J., Fiore, G., Karaman, S., Frazzoli, E., & How, J. P. (2009). Real-time motion planning with applications to autonomous urban driving. IEEE Transactions on Control Systems Technology, 17(5), 1105\u20131118.","journal-title":"IEEE Transactions on Control Systems Technology"},{"key":"9409_CR20","doi-asserted-by":"crossref","unstructured":"Levinson, J., & Thrun, S. (May 2010). Robust vehicle localization in urban environments using probabilistic maps. In IEEE international conference on robotics and automation (pp. 4372\u20134378).","DOI":"10.1109\/ROBOT.2010.5509700"},{"issue":"8","key":"9409_CR21","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1177\/0278364909340445","volume":"28","author":"M Likhachev","year":"2009","unstructured":"Likhachev, M., & Ferguson, D. (2009). Planning long dynamically feasible maneuvers for autonomous vehicles. The International Journal of Robotics Research, 28(8), 933\u2013945.","journal-title":"The International Journal of Robotics Research"},{"issue":"1","key":"9409_CR22","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/S0001-4575(00)00019-1","volume":"33","author":"M Minderhoud","year":"2001","unstructured":"Minderhoud, M., & Bovy, P. (2001). Extended time-to-collision measures for road traffic safety assessment. Accident Analysis & Prevention, 33(1), 89\u201397.","journal-title":"Accident Analysis & Prevention"},{"key":"9409_CR23","doi-asserted-by":"crossref","unstructured":"O\u2019Kelly, M., Abbas, H., & Mangharam, R. (2016). APEX : Autonomous vehicle plan verification and execution. In SAE World Congress.","DOI":"10.4271\/2016-01-0019"},{"key":"9409_CR24","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-10373-5_13","volume-title":"Formal methods and software engineering","author":"A Platzer","year":"2009","unstructured":"Platzer, A., & Quesel, J.-D. (2009). European train control system: A case study in formal verification. In K. Breitman & A. Cavalcanti (Eds.), Formal methods and software engineering (pp. 246\u2013265). Berlin: Springer."},{"key":"9409_CR25","doi-asserted-by":"crossref","unstructured":"Quottrup, M.\u00a0M., Bak, T., & Zamanabadi, R.\u00a0I. (April, 2004). Multi-robot planning: A timed automata approach. In IEEE international conference on robotics and automation, 2004. Proceedings. ICRA \u201904. 2004 (Vol.\u00a05, pp. 4417\u20134422).","DOI":"10.1109\/ROBOT.2004.1302413"},{"key":"9409_CR26","unstructured":"Stanley, K. D., Sorensen, P., Samaras, C., Anderson, J. M., Kalra, N., & Oluwatola, T.\u00a0A. (2016). Autonomous vehicle technology. A guide for policymakers. Research Reports. RAND Corporation. ISBN: 978-0-8330-8398-2."},{"key":"9409_CR27","first-page":"7","volume-title":"Trajectory and floating-car data","author":"M Treiber","year":"2013","unstructured":"Treiber, M., & Kesting, A. (2013). Trajectory and floating-car data (pp. 7\u201312). Berlin: Springer."},{"key":"9409_CR28","unstructured":"Uppaal. \n                    http:\/\/www.uppaal.org\/\n                    \n                  . Accessed 29 Apr 2019."},{"issue":"8","key":"9409_CR29","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1002\/rob.20255","volume":"25","author":"C Urmson","year":"2008","unstructured":"Urmson, C., et al. (2008). Autonomous driving in urban environments: Boss and the urban challenge. Journal of Field Robotics, 25(8), 425\u2013466.","journal-title":"Journal of Field Robotics"},{"issue":"3","key":"9409_CR30","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1016\/S0001-4575(02)00022-2","volume":"35","author":"K Vogel","year":"2003","unstructured":"Vogel, K. (2003). A comparison of headway and time to collision as safety indicators. Accident Analysis & Prevention, 35(3), 427\u2013433.","journal-title":"Accident Analysis & Prevention"},{"issue":"2","key":"9409_CR31","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/SURV.2009.090202","volume":"11","author":"TL Willke","year":"2009","unstructured":"Willke, T. L., Tientrakool, P., & Maxemchuk, N. F. (2009). A survey of inter-vehicle communication protocols and their applications. IEEE Communications Surveys Tutorials, 11(2), 3\u201320.","journal-title":"IEEE Communications Surveys Tutorials"},{"key":"9409_CR32","volume-title":"An introduction to multi-agent systems","author":"M Wooldridge","year":"2009","unstructured":"Wooldridge, M. (2009). An introduction to multi-agent systems (2nd ed.). Hoboken: Wiley.","edition":"2"},{"key":"9409_CR33","doi-asserted-by":"crossref","unstructured":"Zhang, S., Deng, W., Zhao, Q., Sun, H., & Litkouhi, B. (2013). Dynamic trajectory planning for vehicle autonomous driving. In IEEE international conference on systems, man, and cybernetics (pp. 4161\u20134166).","DOI":"10.1109\/SMC.2013.709"}],"container-title":["Autonomous Agents and Multi-Agent Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-019-09409-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10458-019-09409-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-019-09409-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T23:05:34Z","timestamp":1588374334000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10458-019-09409-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,5]]}},"alternative-id":["9409"],"URL":"https:\/\/doi.org\/10.1007\/s10458-019-09409-x","relation":{},"ISSN":["1387-2532","1573-7454"],"issn-type":[{"value":"1387-2532","type":"print"},{"value":"1573-7454","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,5]]},"assertion":[{"value":"3 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}