{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T15:40:57Z","timestamp":1779896457460,"version":"3.53.1"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/N007565\/1"],"award-info":[{"award-number":["EP\/N007565\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/V026801"],"award-info":[{"award-number":["EP\/V026801"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000287","name":"Royal Academy of Engineering","doi-asserted-by":"crossref","award":["Chairs in Emerging Technologies 2019 - Cohort 4 - Professor Michael Fisher"],"award-info":[{"award-number":["Chairs in Emerging Technologies 2019 - Cohort 4 - Professor Michael Fisher"]}],"id":[{"id":"10.13039\/501100000287","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>Swarm robotic systems consist of numerous simple robots coordinating in a decentralised manner to achieve a common goal. Ensuring that individual robot behaviours lead to the desired swarm-level outcomes is challenging due to the lack of a central controller. This article uses two frameworks to facilitate formal specification and verification of robot swarms: (1) NuXMV, which models the system as a Finite State Machine, specifies properties using temporal logic, and verifies them through model checking with BDDs and SMT-solvers; and (2) GROOVE, which models the system as a Graph Grammar, specifies properties using temporal logic with graphical states, and verifies them via graph-specific model checking algorithms. We compare these formal approaches by modelling the Alpha swarm aggregation algorithm, which ensures that any robot disconnected from the swarm, capable only of short-range wireless communications, will eventually return to it. We find that GROOVE effectively leverages symmetry to reduce the state space, while NuXMV excels in handling models requiring extensive calculations and data manipulations not optimally expressed through graphs. We discuss the suitability of each approach for different systems and properties, suggesting future directions that combine the strengths of both approaches.<\/jats:p>","DOI":"10.1145\/3736689","type":"journal-article","created":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T07:13:06Z","timestamp":1749193986000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Specification and Verification of the Alpha Swarm Algorithm using NuXMV and GROOVE"],"prefix":"10.1145","volume":"38","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5010-505X","authenticated-orcid":false,"given":"Maryam","family":"Ghaffari Saadat","sequence":"first","affiliation":[{"name":"Computer Science, The University of Manchester","place":["Manchester, United Kingdom of Great Britain and Northern Ireland"]},{"name":"Computer Science, University of Bristol","place":["Bristol, United Kingdom of Great Britain and Northern Ireland"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5995-7494","authenticated-orcid":false,"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[{"name":"Computer Science, The University of Manchester","place":["Manchester, United Kingdom of Great Britain and Northern Ireland"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0875-3862","authenticated-orcid":false,"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"Computer Science, The University of Manchester","place":["Manchester, United Kingdom of Great Britain and Northern Ireland"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,2,13]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19759-8_23"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22416-9_4"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","unstructured":"Abdelkader Behdenna Clare Dixon and Michael Fisher. 2009. Deductive verification of simple foraging robotic behaviours. International Journal of Intelligent Computing and Cybernetics 2 4 (2009) 604\u2013643. DOI:10.1108\/17563780911005818","DOI":"10.1108\/17563780911005818"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-457"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_3_7_2","unstructured":"Roberto Cavada Alessandro Cimatti Gavin Keighren Emanuele Olivetti Marco Pistore and Marco Roveri. 2004. NuSMV 2.2 Tutorial. https:\/\/nusmv.fbk.eu\/tutorial\/v22\/tutorial.pdf. Accessed: 2025-06-17."},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_1"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_72"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","unstructured":"Pepijn Crouzen Jaco van de Pol and Arend Rensink. 2008. Applying formal methods to gossiping networks with mCRL and GROOVE. SIGMETRICS Performance Evaluation Review 36 3(2008) 7\u201316. DOI:10.1145\/1481506.1481510","DOI":"10.1145\/1481506.1481510"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","unstructured":"Giorgio Delzanno Arend Rensink and Riccardo Traverso. 2014. Graph- versus vector-based analysis of a consensus protocol. In Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering GRAPHITE 2014 Grenoble France 5th April 2014 (EPTCS Vol. 159) Dragan Bosnacki Stefan Edelkamp Alberto Lluch-Lafuente and Anton Wijs (Eds.). Electronic Proceedings in Theoretical Computer Science 44\u201357. DOI:10.4204\/EPTCS.159.5","DOI":"10.4204\/EPTCS.159.5"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","unstructured":"Clare Dixon Alan F. T. Winfield Michael Fisher and Chengxiu Zeng. 2012. Towards temporal verification of swarm robotic systems. Robotics and Autonomous Systems 60 11 (2012) 1429\u20131441. DOI:10.1016\/J.ROBOT.2012.03.003","DOI":"10.1016\/J.ROBOT.2012.03.003"},{"key":"e_1_3_3_14_2","unstructured":"Hartmut Ehrig Karsten Ehrig Ulrike Prange and Gabriele Taentzer. 2006. Fundamental theory for typed attributed graphs and graph transformation based on adhesive HLR categories. Fundamenta Informaticae 74 1 (2006) 31\u201361. Retrieved from http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi74-1-03"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","unstructured":"John E. Hopcroft Rajeev Motwani and Jeffrey D. Ullman. 2001. Introduction to automata theory languages and computation 2nd edition. SIGACT News 32 1(2001) 60\u201365. DOI:10.1145\/568438.568455","DOI":"10.1145\/568438.568455"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_19"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","unstructured":"Savas Konur Clare Dixon and Michael Fisher. 2012. Analysing robot swarm behaviour via probabilistic model checking. Robotics and Autonomous Systems 60 2 (2012) 199\u2013213. DOI:10.1016\/J.ROBOT.2011.10.005","DOI":"10.1016\/J.ROBOT.2011.10.005"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v29i1.9442"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/45"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","unstructured":"Matt Luckcuck Marie Farrell Louise A. Dennis Clare Dixon and Michael Fisher. 2019. Formal specification and verification of autonomous robotic systems: A survey. ACM Computing Surveys 52 5 (2019) 100:1\u2013100:41. DOI:10.1145\/3342355","DOI":"10.1145\/3342355"},{"key":"e_1_3_3_21_2","volume-title":"Minimalist Coherent Swarming of Wireless Networked Autonomous Mobile Robots","author":"Nembrini Julien","year":"2005","unstructured":"Julien Nembrini. 2005. Minimalist Coherent Swarming of Wireless Networked Autonomous Mobile Robots. Ph.D. Dissertation. University of the West of England, Bristol. Retrieved from https:\/\/infoscience.epfl.ch\/handle\/20.500.14299\/213997"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","unstructured":"Arend Rensink. 2006. Isomorphism checking in GROOVE. In The Proceedings of the Third International Workshop on Graph Based Tools (GraBaTs\u201906) (Electronic Communications of the EASST Vol. 1). Berlin Universities Publishing Berlin Germany 1\u201311. DOI:10.14279\/TUJ.ECEASST.1.77","DOI":"10.14279\/TUJ.ECEASST.1.77"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68270-9_10"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30203-2_17"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1142\/3303"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30552-1_2"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","unstructured":"Melanie Schranz Martina Umlauft Micha Sende and Wilfried Elmenreich. 2020. Swarm robotic behaviors and current applications. Frontiers in Robotics and AI 7 (2020) 36. DOI:10.3389\/FROBT.2020.00036","DOI":"10.3389\/FROBT.2020.00036"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","unstructured":"Michael Sipser. 1996. Introduction to the theory of computation. ACM SIGACT News 27 1(1996) 27\u201329. DOI:10.1145\/230514.571645","DOI":"10.1145\/230514.571645"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1995.523248"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15461-4_1"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_15"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3736689","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T11:48:48Z","timestamp":1771242528000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3736689"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,13]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3736689"],"URL":"https:\/\/doi.org\/10.1145\/3736689","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,13]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-05-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}