{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T15:43:03Z","timestamp":1779896583669,"version":"3.53.1"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319224152","type":"print"},{"value":"9783319224169","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22416-9_4","type":"book-chapter","created":{"date-parts":[[2015,7,17]],"date-time":"2015-07-17T12:41:16Z","timestamp":1437136876000},"page":"26-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Symmetry Reduction Enables Model Checking of More Complex Emergent Behaviours of Swarm Navigation Algorithms"],"prefix":"10.1007","author":[{"given":"Laura","family":"Antu\u00f1a","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dejanira","family":"Araiza-Illan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S\u00e9rgio","family":"Campos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kerstin","family":"Eder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,7,18]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Appold, C.: Efficient symmetry reduction and the use of state symmetries for symbolic model checking. In: Proc. GandALF, pp. 173\u2013187 (2010)","DOI":"10.4204\/EPTCS.25.17"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Bosnacki, D., Dams, D., Holenderski, L.: Symmetric SPIN. In: SPIN Model Checking and Software Verification, Stanford, CA, USA, pp. 1\u201319 (2000)","DOI":"10.1007\/10722468_1"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV version 2: an opensource tool for symbolic model checking. In: Computer-Aided Verification, Copenhagen, Denmark. pp. 359\u2013364 (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"4_CR4","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"1\u20132","key":"4_CR5","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E Clarke","year":"1996","unstructured":"Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(1\u20132), 77\u2013104 (1996)","journal-title":"Formal Methods in System Design"},{"key":"4_CR6","unstructured":"Dixon, C., Winfield, A.F., Fisher, M.: Verification of swarm robots: the Alpha algorithm. In: Proc. ARW, Westminster, UK, pp. 10\u201311 (2010)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-642-23232-9_30","volume-title":"Towards Autonomous Robotic Systems","author":"C Dixon","year":"2011","unstructured":"Dixon, C., Winfield, A., Fisher, M.: Towards temporal verification of emergent behaviours in swarm robotic systems. In: Gro\u00df, R., Alboul, L., Melhuish, C., Witkowski, M., Prescott, T.J., Penders, J. (eds.) TAROS 2011. LNCS, vol. 6856, pp. 336\u2013347. Springer, Heidelberg (2011)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Dixon, C., Winfield, A.F., Fisher, M., Zeng, C.: Towards temporal verification of swarm robotic systems. In: Robotics and Autonomous Systems, Bristol, UK, pp. 1429\u20131441 (2012)","DOI":"10.1016\/j.robot.2012.03.003"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/11526841_32","volume-title":"FM 2005: Formal Methods","author":"AF Donaldson","year":"2005","unstructured":"Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 481\u2013496. Springer, Heidelberg (2005)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-39724-3_20","volume-title":"Correct Hardware Design and Verification Methods","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Wahl, T.: On combining symmetry reduction and symbolic representation for efficient model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 216\u2013230. Springer, Heidelberg (2003)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-31980-1_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EA Emerson","year":"2005","unstructured":"Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382\u2013396. Springer, Heidelberg (2005)"},{"key":"4_CR12","unstructured":"Gomes, P.d.C.: Verification of symmetric models using semiautomatic abstractions. Master\u2019s thesis, Computer Science, Belo Horizonte, Brazil (2010)"},{"issue":"1","key":"4_CR13","doi-asserted-by":"publisher","first-page":"48","DOI":"10.3176\/proc.2011.1.05","volume":"60","author":"S Juurik","year":"2011","unstructured":"Juurik, S., Vain, J.: Model checking of emergent behaviour properties of robot swarms. Proceedings of the Estonian Academy of Sciences 60(1), 48\u201354 (2011)","journal-title":"Proceedings of the Estonian Academy of Sciences"},{"issue":"2","key":"4_CR14","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1109\/TRO.2006.889492","volume":"23","author":"M Kloetzer","year":"2007","unstructured":"Kloetzer, M., Belta, C.: Temporal logic planning and control of robotic swarms by hierachical abstractions. IEEE Transactions on Robotics 23(2), 320\u2013330 (2007)","journal-title":"IEEE Transactions on Robotics"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.robot.2011.10.005","volume":"60","author":"S Konur","year":"2012","unstructured":"Konur, S., Dixon, C., Fisher, M.: Analysing robot swarm behaviour via probabilistic model checking. Robotics and Autonomous Systems 60, 199\u2013213 (2012)","journal-title":"Robotics and Autonomous Systems"},{"key":"4_CR16","unstructured":"Kouvaros, P., Lomuscio, A.: A counter abstraction technique for the verification of robot swarms. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25\u201330, 2015, Austin, Texas, USA, pp. 2081\u20132088 (2015)"},{"key":"4_CR17","unstructured":"Nembrini, J.: Minimalist Coherent Swarming of Wireless Networked Autonomous Mobile Robots. Ph.D. thesis, Bristol, UK (2005)"},{"issue":"1\u20132","key":"4_CR18","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"C Norris Ip","year":"1996","unstructured":"Norris Ip, C., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9(1\u20132), 41\u201375 (1996)","journal-title":"Formal Methods in System Design"},{"key":"4_CR19","unstructured":"Rouff, C., Hinchey, M., Truszkowski, W., Rash, J.: Formal methods for autonomic and swarm-based systems. In: Proc. ISoLA, Paphos, Cyprus, pp. 100\u2013102 (2004)"},{"issue":"4","key":"4_CR20","doi-asserted-by":"crossref","first-page":"363","DOI":"10.5772\/5769","volume":"2","author":"AF Winfield","year":"2005","unstructured":"Winfield, A.F., Sa, J., Fernandez-Gago, M.C., Dixon, C., Fisher, M.: On formal specification of emergent behaviours of swarm robotic systems. International Journal of Advanced Robotic Systems 2(4), 363\u2013370 (2005)","journal-title":"International Journal of Advanced Robotic Systems"}],"container-title":["Lecture Notes in Computer Science","Towards Autonomous Robotic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22416-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T06:22:45Z","timestamp":1676960565000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22416-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319224152","9783319224169"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22416-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"18 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}