{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:00:55Z","timestamp":1750309255478,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,14]],"date-time":"2024-04-14T00:00:00Z","timestamp":1713052800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Natural Sciences and Engineering Research Council of Canada Discovery Grant"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,14]]},"DOI":"10.1145\/3644033.3644377","type":"proceedings-article","created":{"date-parts":[[2024,6,6]],"date-time":"2024-06-06T16:56:27Z","timestamp":1717692987000},"page":"77-87","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Compositional Analysis of Parametric Cooperative Cyber-Physical Systems"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-6568-3572","authenticated-orcid":false,"given":"Raniah A","family":"Alghamdi","sequence":"first","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"},{"name":"King Abdulaziz University, Jeddah, Saudi Arabia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-4235-9328","authenticated-orcid":false,"given":"Richard","family":"Trefler","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,6]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038685"},{"volume-title":"Hybrid systems","author":"Alur Rajeev","key":"e_1_3_2_1_2_1","unstructured":"Rajeev Alur, Costas Courcoubetis, Thomas A Henzinger, and Pei-Hsin Ho. 1992. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid systems. Springer, 209--229."},{"key":"e_1_3_2_1_3_1","volume-title":"Platoon management with cooperative adaptive cruise control enabled by VANET. Vehicular communications 2, 2","author":"Amoozadeh Mani","year":"2015","unstructured":"Mani Amoozadeh, Hui Deng, Chen-Nee Chuah, H Michael Zhang, and Dipak Ghosal. 2015. Platoon management with cooperative adaptive cruise control enabled by VANET. Vehicular communications 2, 2 (2015), 110--123."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"e_1_3_2_1_5_1","unstructured":"Roderick P. Bloem Swen Jacobs Ayrat Khalimov Igor Konnov Sasha Rubin Helmut Veith and Josef Widder. 2015. Decidability of parameterized verification. Morgan and Claypool."},{"key":"e_1_3_2_1_6_1","volume-title":"Computer Aided Verification: 10th International Conference, CAV'98 Vancouver, BC, Canada, June 28--July 2, 1998 Proceedings 10","author":"Clarke Edmund M","year":"1998","unstructured":"Edmund M Clarke, E Allen Emerson, Somesh Jha, and A Prasad Sistla. 1998. Symmetry reductions in model checking. In Computer Aided Verification: 10th International Conference, CAV'98 Vancouver, BC, Canada, June 28--July 2, 1998 Proceedings 10. Springer, 147--158."},{"volume-title":"Handbook of model checking","author":"Clarke Edmund M","key":"e_1_3_2_1_7_1","unstructured":"Edmund M Clarke, Thomas A Henzinger, Helmut Veith, and Roderick Bloem. 2018. Handbook of model checking. Vol. 10. Springer."},{"key":"e_1_3_2_1_8_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA, USA."},{"key":"e_1_3_2_1_9_1","volume-title":"International Workshop on Hybrid and Real-Time Systems. Springer, 154--170","author":"Dolginova Ekaterina","year":"1997","unstructured":"Ekaterina Dolginova and Nancy Lynch. 1997. Safety verification for automated platoon maneuvers: A case study. In International Workshop on Hybrid and Real-Time Systems. Springer, 154--170."},{"key":"e_1_3_2_1_10_1","volume-title":"2013 European Control Conference (ECC). IEEE, 4244--4251","author":"Donz\u00e9 Alexandre","year":"2013","unstructured":"Alexandre Donz\u00e9 and Goran Frehse. 2013. Modular, hierarchical models of control systems in SpaceEx. In 2013 European Control Conference (ECC). IEEE, 4244--4251."},{"key":"e_1_3_2_1_11_1","first-page":"119","article-title":"Compositional verification for reactive multi-agent systems applied to platoon non collision verification","volume":"10","author":"El-Zaher Madeleine","year":"2012","unstructured":"Madeleine El-Zaher, Jean-Michel Contet, Pablo Gruer, Franck Gechter, and Abderrafiaa Koukam. 2012. Compositional verification for reactive multi-agent systems applied to platoon non collision verification. Stud. Inform. Univ. 10, 3 (2012), 119--141.","journal-title":"Stud. Inform. Univ."},{"volume-title":"Compositional verification of hybrid systems using simulation relations. Ph. D. Dissertation","author":"Frehse Goran","key":"e_1_3_2_1_12_1","unstructured":"Goran Frehse. 2005. Compositional verification of hybrid systems using simulation relations. Ph. D. Dissertation. Radboud University Nijmegen."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"e_1_3_2_1_14_1","volume-title":"Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings 23","author":"Frehse Goran","year":"2011","unstructured":"Goran Frehse, Colas Le Guernic, Alexandre Donz\u00e9, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings 23. Springer, 379--395."},{"key":"e_1_3_2_1_15_1","volume-title":"Nonlinear dynamics of networks: the groupoid formalism. Bulletin of the american mathematical society 43, 3","author":"Golubitsky Martin","year":"2006","unstructured":"Martin Golubitsky and Ian Stewart. 2006. Nonlinear dynamics of networks: the groupoid formalism. Bulletin of the american mathematical society 43, 3 (2006), 305--364."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59615-5_13"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_48"},{"key":"e_1_3_2_1_18_1","volume-title":"A survey on platoon-based vehicular cyber-physical systems","author":"Jia Dongyao","year":"2015","unstructured":"Dongyao Jia, Kejie Lu, Jianping Wang, Xiang Zhang, and Xuemin Shen. 2015. A survey on platoon-based vehicular cyber-physical systems. IEEE communications surveys & tutorials 18, 1 (2015), 263--284."},{"key":"e_1_3_2_1_19_1","volume-title":"2012 IEEE\/ACM Third International Conference on Cyber-Physical Systems. IEEE, 161--170","author":"Johnson Taylor T","year":"2012","unstructured":"Taylor T Johnson and Sayan Mitra. 2012. Parametrized verification of distributed cyber-physical systems: An aircraft landing protocol case study. In 2012 IEEE\/ACM Third International Conference on Cyber-Physical Systems. IEEE, 161--170."},{"volume-title":"Formal Techniques for Distributed Systems","author":"Johnson Taylor T","key":"e_1_3_2_1_20_1","unstructured":"Taylor T Johnson and Sayan Mitra. 2012. A small model theorem for rectangular hybrid automata networks. In Formal Techniques for Distributed Systems. Springer, 18--34."},{"key":"e_1_3_2_1_21_1","volume-title":"Passel: A Verification Tool for Parameterized Networks of Hybrid Automata.","author":"Johnson Taylor T","year":"2013","unstructured":"Taylor T Johnson and Sayan Mitra. 2013. Passel: A Verification Tool for Parameterized Networks of Hybrid Automata. (2013)."},{"key":"e_1_3_2_1_22_1","volume-title":"Formal verification of autonomous vehicle platooning. Science of computer programming 148","author":"Kamali Maryam","year":"2017","unstructured":"Maryam Kamali, Louise A Dennis, Owen McAree, Michael Fisher, and Sandor M Veres. 2017. Formal verification of autonomous vehicle platooning. Science of computer programming 148 (2017), 88--106."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_6"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.664155"},{"key":"e_1_3_2_1_25_1","volume-title":"Hybrid i\/o automata. Information and computation 185, 1","author":"Lynch Nancy","year":"2003","unstructured":"Nancy Lynch, Roberto Segala, and Frits Vaandrager. 2003. Hybrid i\/o automata. Information and computation 185, 1 (2003), 105--157."},{"key":"e_1_3_2_1_26_1","unstructured":"Ibtissem Ben Makhlouf and Stefan Kowalewski. 2014. Networked Cooperative Platoon of Vehicles for Testing Methods and Verification Tools.. In ARCH@CPSWeek. 37--42."},{"key":"e_1_3_2_1_27_1","volume-title":"Trefler","author":"Namjoshi Kedar S.","year":"2012","unstructured":"Kedar S. Namjoshi and Richard J. Trefler. 2012. Local Symmetry and Compositional Verification. In Verification, Model Checking, and Abstract Interpretation, Viktor Kuncak and Andrey Rybalchenko (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 348--362."},{"key":"e_1_3_2_1_28_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 164--178","author":"Namjoshi Kedar S","year":"2015","unstructured":"Kedar S Namjoshi and Richard J Trefler. 2015. Analysis of dynamic process networks. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 164--178."},{"key":"e_1_3_2_1_29_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 589--606","author":"Namjoshi Kedar S","year":"2016","unstructured":"Kedar S Namjoshi and Richard J Trefler. 2016. Parameterized compositional model checking. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 589--606."},{"key":"e_1_3_2_1_30_1","volume-title":"Computer Aided Verification: 10th International Conference, CAV'98 Vancouver, BC, Canada, June 28--July 2, 1998 Proceedings 10","author":"Peled Doron","year":"1998","unstructured":"Doron Peled. 1998. Ten years of partial order reduction. In Computer Aided Verification: 10th International Conference, CAV'98 Vancouver, BC, Canada, June 28--July 2, 1998 Proceedings 10. Springer, 17--28."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2935423"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_15"},{"key":"e_1_3_2_1_33_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 82--97","author":"Pnueli Amir","year":"2001","unstructured":"Amir Pnueli, Sitvanit Ruah, and Lenore Zuck. 2001. Automatic deductive verification with invisible invariants. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 82--97."},{"key":"e_1_3_2_1_34_1","volume-title":"Proceedings of 1995 American Control Conference-ACC'95","volume":"5","author":"Puri Anuj","year":"1995","unstructured":"Anuj Puri and Pravin Varaiya. 1995. Driving safely in smart cars. In Proceedings of 1995 American Control Conference-ACC'95, Vol. 5. IEEE, 3597--3599."},{"volume-title":"Vehicle dynamics and control","author":"Rajamani Rajesh","key":"e_1_3_2_1_35_1","unstructured":"Rajesh Rajamani. 2012. Vehicle dynamics and control (second ed.). Springer Science & Business Media."}],"event":{"name":"FormaliSE '24: 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Lisbon Portugal","acronym":"FormaliSE '24"},"container-title":["Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644033.3644377","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3644033.3644377","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:56:58Z","timestamp":1750291018000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644033.3644377"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,14]]},"references-count":35,"alternative-id":["10.1145\/3644033.3644377","10.1145\/3644033"],"URL":"https:\/\/doi.org\/10.1145\/3644033.3644377","relation":{},"subject":[],"published":{"date-parts":[[2024,4,14]]},"assertion":[{"value":"2024-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}