{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T19:17:04Z","timestamp":1792264624679,"version":"4.4.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031197581","type":"print"},{"value":"9783031197598","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-19759-8_6","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T09:07:32Z","timestamp":1666170452000},"page":"82-96","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Modelling Flocks of\u00a0Birds from\u00a0the\u00a0Bottom Up"],"prefix":"10.1007","author":[{"given":"Rocco","family":"De Nicola","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luca","family":"Di Stefano","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Omar","family":"Inverso","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Serenella","family":"Valiani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-319-22416-9_4","volume-title":"Towards Autonomous Robotic Systems","author":"L Antu\u00f1a","year":"2015","unstructured":"Antu\u00f1a, L., Araiza-Illan, D., Campos, S., Eder, K.: Symmetry reduction enables model checking of more complex emergent behaviours of swarm navigation algorithms. In: Dixon, C., Tuyls, K. (eds.) TAROS 2015. LNCS (LNAI), vol. 9287, pp. 26\u201337. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22416-9_4"},{"issue":"4","key":"6_CR2","doi-asserted-by":"publisher","first-page":"1232","DOI":"10.1073\/pnas.0711437105","volume":"105","author":"M Ballerini","year":"2008","unstructured":"Ballerini, M., et al.: Interaction ruling animal collective behavior depends on topological rather than metric distance: evidence from a field study. Proc. Natl. Acad. Sci. 105(4), 1232\u20131237 (2008). https:\/\/doi.org\/10.1073\/pnas.0711437105","journal-title":"Proc. Natl. Acad. Sci."},{"issue":"13","key":"6_CR3","doi-asserted-by":"publisher","first-page":"4786","DOI":"10.1073\/pnas.1118633109","volume":"109","author":"W Bialek","year":"2012","unstructured":"Bialek, W., et al.: Statistical mechanics for natural flocks of birds. Proc. Natl. Acad. Sci. 109(13), 4786\u20134791 (2012)","journal-title":"Proc. Natl. Acad. Sci."},{"issue":"1","key":"6_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11721-012-0075-2","volume":"7","author":"M Brambilla","year":"2013","unstructured":"Brambilla, M., Ferrante, E., Birattari, M., Dorigo, M.: Swarm robotics: a review from the swarm engineering perspective. Swarm Intell. 7(1), 1\u201341 (2013). https:\/\/doi.org\/10.1007\/s11721-012-0075-2","journal-title":"Swarm Intell."},{"issue":"Suppl 3","key":"6_CR5","doi-asserted-by":"publisher","first-page":"7296","DOI":"10.1073\/pnas.082081099","volume":"99","author":"LE Cederman","year":"2002","unstructured":"Cederman, L.E.: Endogenizing geopolitical boundaries with agent-based modeling. Proc. Natl. Acad. Sci. 99(Suppl 3), 7296\u20137303 (2002). https:\/\/doi.org\/10.1073\/pnas.082081099","journal-title":"Proc. Natl. Acad. Sci."},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"De Nicola, R., Di Stefano, L., Inverso, O.: Multi-agent systems with virtual stigmergy. Sci. Comput. Program. 187, 102345 (2020). https:\/\/doi.org\/10.1016\/j.scico.2019.102345","DOI":"10.1016\/j.scico.2019.102345"},{"issue":"3","key":"6_CR8","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1162\/ARTL\\_a_00135","volume":"20","author":"J Demsar","year":"2014","unstructured":"Demsar, J., Lebar Bajec, I.: Simulated predator attacks on flocks: a comparison of tactics. Artif. Life 20(3), 343\u2013359 (2014). https:\/\/doi.org\/10.1162\/ARTL_a_00135","journal-title":"Artif. Life"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Desai, A., Saha, I., Yang, J., Qadeer, S., Seshia, S.A.: DRONA: a framework for safe distributed mobile robotics. In: ICCPS (2017). https:\/\/doi.org\/10.1145\/3055004.3055022","DOI":"10.1145\/3055004.3055022"},{"issue":"3","key":"6_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3490387","volume":"31","author":"L Di Stefano","year":"2022","unstructured":"Di Stefano, L., De Nicola, R., Inverso, O.: Verification of distributed systems via sequential emulation. ACM Trans. Softw. Eng. Methodol. 31(3), 1\u201341 (2022). https:\/\/doi.org\/10.1145\/3490387","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-030-89159-6_29","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"L Di Stefano","year":"2021","unstructured":"Di Stefano, L., Lang, F.: Verifying temporal properties of stigmergic collective systems using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2021. LNCS, vol. 13036, pp. 473\u2013489. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89159-6_29"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-030-50029-0_23","volume-title":"Coordination Models and Languages","author":"L Di Stefano","year":"2020","unstructured":"Di Stefano, L., Lang, F., Serwe, W.: Combining SLiVER with CADP to analyze multi-agent systems. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 370\u2013385. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50029-0_23"},{"issue":"2","key":"6_CR13","doi-asserted-by":"publisher","first-page":"160","DOI":"10.2307\/4081266","volume":"69","author":"JT Emlen","year":"1952","unstructured":"Emlen, J.T.: Flocking behavior in birds. Auk 69(2), 160\u2013170 (1952)","journal-title":"Auk"},{"issue":"1","key":"6_CR14","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1137\/080719376","volume":"41","author":"D Finkelshtein","year":"2009","unstructured":"Finkelshtein, D., Kondratiev, Y., Kutoviy, O.: Individual based model with competition in spatial ecology. SIAM J. Math. Anal. 41(1), 297\u2013317 (2009). https:\/\/doi.org\/10.1137\/080719376","journal-title":"SIAM J. Math. Anal."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-23820-3_5","volume-title":"Runtime Verification","author":"A Francalanza","year":"2015","unstructured":"Francalanza, A., Aceto, L., Ingolfsdottir, A.: On verifying Hennessy-Milner logic with recursion at runtime. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 71\u201386. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_5"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Inverso, O., Trubiani, C.: Parallel and distributed bounded model checking of multi-threaded programs. In: 25th Symposium on Principles and Practice of Parallel Programming (PPoPP), pp. 202\u2013216. ACM (2020). https:\/\/doi.org\/10.1145\/3332466.3374529","DOI":"10.1145\/3332466.3374529"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Koenig, N., Howard, A.: Design and use paradigms for Gazebo, an open-source multi-robot simulator. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), vol. 3, pp. 2149\u20132154. IEEE (2004). https:\/\/doi.org\/10.1109\/IROS.2004.1389727","DOI":"10.1109\/IROS.2004.1389727"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Kouvaros, P., Lomuscio, A.: A counter abstraction technique for the verification of robot swarms. In: 29th Conference on Artificial Intelligence (AAAI), pp. 2081\u20132088. AAAI (2015)","DOI":"10.1609\/aaai.v29i1.9442"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-030-50371-0_28","volume-title":"Computational Science \u2013 ICCS 2020","author":"E Kuylen","year":"2020","unstructured":"Kuylen, E., Liesenborgs, J., Broeckhove, J., Hens, N.: Using individual-based models to look beyond the horizon: the changing effects of household-based clustering of susceptibility to measles in the next 20 years. In: Krzhizhanovskaya, V.V., et al. (eds.) ICCS 2020. LNCS, vol. 12137, pp. 385\u2013398. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50371-0_28"},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.jtbi.2004.10.003","volume":"233","author":"I Lebar Bajec","year":"2005","unstructured":"Lebar Bajec, I., Zimic, N., Mraz, M.: Simulating flocks on the wing: the fuzzy approach. J. Theor. Biol. 233, 199\u2013220 (2005). https:\/\/doi.org\/10.1016\/j.jtbi.2004.10.003","journal-title":"J. Theor. Biol."},{"issue":"5","key":"6_CR21","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Program. 78(5), 293\u2013303 (2009). https:\/\/doi.org\/10.1016\/j.jlap.2008.08.004","journal-title":"J. Log. Algebraic Program."},{"issue":"1","key":"6_CR22","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2015","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19(1), 9\u201330 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0378-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-45231-5_1","volume-title":"Foundations of Software Science and Computation Structures","author":"U Mehmood","year":"2020","unstructured":"Mehmood, U., Roy, S., Grosu, R., Smolka, S.A., Stoller, S.D., Tiwari, A.: Neural flocking: MPC-based supervised learning of flocking controllers. In: Goubault-Larrecq, J., K\u00f6nig, B. (eds.) FoSSaCS 2020. LNCS, vol. 12077, pp. 1\u201316. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_1"},{"issue":"3","key":"6_CR24","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/TAC.2005.864190","volume":"51","author":"R Olfati-Saber","year":"2006","unstructured":"Olfati-Saber, R.: Flocking for multi-agent dynamic systems: algorithms and theory. IEEE Trans. Autom. Control 51(3), 401\u2013420 (2006). https:\/\/doi.org\/10.1109\/TAC.2005.864190","journal-title":"IEEE Trans. Autom. Control"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Pinciroli, C., Beltrame, G.: Buzz: an extensible programming language for heterogeneous swarm robotics. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3794\u20133800. IEEE (2016). https:\/\/doi.org\/10.1109\/IROS.2016.7759558","DOI":"10.1109\/IROS.2016.7759558"},{"issue":"4","key":"6_CR26","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/S11721-012-0072-5","volume":"6","author":"C Pinciroli","year":"2012","unstructured":"Pinciroli, C., et al.: ARGoS: a modular, parallel, multi-engine simulator for multi-robot systems. Swarm Intell. 6(4), 271\u2013295 (2012). https:\/\/doi.org\/10.1007\/S11721-012-0072-5","journal-title":"Swarm Intell."},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 46\u201357. IEEE (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"6_CR28","unstructured":"Quigley, M., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software (2009)"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Reynolds, C.W.: Flocks, herds and schools: a distributed behavioral model. In: Proceedings of the 14th Annual Conference on Computer Graphics and Interactive Techniques, SIGGRAPH 1987, Anaheim, California, USA, 27\u201331 July 1987, pp. 25\u201334. ACM (1987). https:\/\/doi.org\/10.1145\/37401.37406","DOI":"10.1145\/37401.37406"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Rohmer, E., Singh, S.P.N., Freese, M.: V-REP: a versatile and scalable robot simulation framework. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 1321\u20131326. IEEE (2013). https:\/\/doi.org\/10.1109\/IROS.2013.6696520","DOI":"10.1109\/IROS.2013.6696520"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202\u2013215. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_16"},{"issue":"1","key":"6_CR32","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1080\/00207170801983091","volume":"82","author":"H Shi","year":"2009","unstructured":"Shi, H., Wang, L., Chu, T.: Flocking of multi-agent systems with a dynamic virtual leader. Int. J. Control 82(1), 43\u201358 (2009). https:\/\/doi.org\/10.1080\/00207170801983091","journal-title":"Int. J. Control"},{"issue":"1","key":"6_CR33","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1057\/eej.2010.33","volume":"37","author":"JE Stiglitz","year":"2011","unstructured":"Stiglitz, J.E., Gallegati, M.: Heterogeneous interacting agent models for understanding monetary economies. East. Econ. J. 37(1), 6\u201312 (2011). https:\/\/doi.org\/10.1057\/eej.2010.33","journal-title":"East. Econ. J."},{"issue":"4","key":"6_CR34","doi-asserted-by":"publisher","first-page":"4828","DOI":"10.1103\/PhysRevE.58.4828","volume":"58","author":"J Toner","year":"1998","unstructured":"Toner, J., Tu, Y.: Flocks, herds, and schools: a quantitative theory of flocking. Phys. Rev. E 58(4), 4828\u20134858 (1998). https:\/\/doi.org\/10.1103\/PhysRevE.58.4828","journal-title":"Phys. Rev. E"},{"key":"6_CR35","doi-asserted-by":"publisher","unstructured":"V\u00e1s\u00e1rhelyi, G., et al.: Outdoor flocking and formation flight with autonomous aerial robots. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3866\u20133873. IEEE (2014). https:\/\/doi.org\/10.1109\/IROS.2014.6943105","DOI":"10.1109\/IROS.2014.6943105"},{"issue":"2\u20134","key":"6_CR36","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/s11721-008-0018-0","volume":"2","author":"AFT Winfield","year":"2008","unstructured":"Winfield, A.F.T., Liu, W., Nembrini, J., Martinoli, A.: Modelling a wireless connected swarm of mobile robots. Swarm Intell. 2(2\u20134), 241\u2013266 (2008). https:\/\/doi.org\/10.1007\/s11721-008-0018-0","journal-title":"Swarm Intell."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19759-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T23:18:19Z","timestamp":1666221499000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19759-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031197581","9783031197598"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19759-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}