{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:32:23Z","timestamp":1770276743415,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642342806","type":"print"},{"value":"9783642342813","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34281-3_7","type":"book-chapter","created":{"date-parts":[[2012,10,29]],"date-time":"2012-10-29T18:38:09Z","timestamp":1351535889000},"page":"54-70","source":"Crossref","is-referenced-by-count":21,"title":["Towards a Formal Verification Methodology for Collective Robotic Systems"],"prefix":"10.1007","author":[{"given":"Edmond","family":"Gjondrekaj","sequence":"first","affiliation":[]},{"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[]},{"given":"Rosario","family":"Pugliese","sequence":"additional","affiliation":[]},{"given":"Francesco","family":"Tiezzi","sequence":"additional","affiliation":[]},{"given":"Carlo","family":"Pinciroli","sequence":"additional","affiliation":[]},{"given":"Manuele","family":"Brambilla","sequence":"additional","affiliation":[]},{"given":"Mauro","family":"Birattari","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Dorigo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"14","key":"7_CR1","doi-asserted-by":"publisher","first-page":"1365","DOI":"10.1002\/spe.486","volume":"32","author":"L. Bettini","year":"2002","unstructured":"Bettini, L., De Nicola, R., Pugliese, R.: Klava: a Java Package for Distributed and Mobile Applications. Software - Practice and Experience\u00a032(14), 1365\u20131394 (2002)","journal-title":"Software - Practice and Experience"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Bonani, M., et al.: The marxbot, a miniature mobile robot opening new perspectives for the collective-robotic research. In: IROS, pp. 4187\u20134193. IEEE (2010)","DOI":"10.1109\/IROS.2010.5649153"},{"key":"7_CR3","unstructured":"Brambilla, M., Pinciroli, C., Birattari, M., Dorigo, M.: Property-driven design for swarm robotics. In: AAMAS. IFAAMAS (to appear, 2012)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/978-3-642-34005-5_7","volume-title":"WRLA 2012","author":"R. Bruni","year":"2012","unstructured":"Bruni, R., Corradini, A., Gadducci, F., Lluch Lafuente, A., Vandin, A.: Modelling and Analyzing Adaptive Self-assembly Strategies with Maude. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol.\u00a07571, pp. 118\u2013138. Springer, Heidelberg (2012)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-13414-2_9","volume-title":"Coordination Models and Languages","author":"F. Calzolai","year":"2010","unstructured":"Calzolai, F., Loreti, M.: Simulation and Analysis of Distributed Systems in Klaim. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol.\u00a06116, pp. 122\u2013136. Springer, Heidelberg (2010)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv.\u00a028, 626\u2013643 (1996)","journal-title":"ACM Comput. Surv."},{"issue":"5","key":"7_CR7","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1109\/32.685256","volume":"24","author":"R. Nicola De","year":"1998","unstructured":"De Nicola, R., Ferrari, G., Pugliese, R.: KLAIM: A Kernel Language for Agents Interaction and Mobility. Transactions on Software Engineering\u00a024(5), 315\u2013330 (1998)","journal-title":"Transactions on Software Engineering"},{"issue":"1","key":"7_CR8","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.tcs.2007.05.008","volume":"382","author":"R. Nicola De","year":"2007","unstructured":"De Nicola, R., Katoen, J., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theor. Comput. Sci.\u00a0382(1), 42\u201370 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR9","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.\u00a06856, pp. 336\u2013347. Springer, Heidelberg (2011)"},{"key":"7_CR10","series-title":"STAR","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/978-3-642-32723-0_41","volume-title":"Distributed Autonomous Robotic Systems","author":"E. Ferrante","year":"2013","unstructured":"Ferrante, E., Brambilla, M., Birattari, M., Dorigo, M.: Socially-Mediated Negotiation for Obstacle Avoidance in Collective Transport. In: Martinoli, A., Mondada, F., Correll, N., Mermoud, G., Egerstedt, M., Hsieh, M.A., Parker, L.E., St\u00f8y, K. (eds.) Distributed Autonomous Robotic Systems. STAR, vol.\u00a083, pp. 571\u2013583. Springer, Heidelberg (2013)"},{"issue":"1","key":"7_CR11","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1142\/S0218843097000057","volume":"6","author":"M. Fisher","year":"1997","unstructured":"Fisher, M., Wooldridge, M.: On the formal specification and verification of multi-agent systems. Int. Journal of Cooperative Information Systems\u00a06(1), 37\u201366 (1997)","journal-title":"Int. Journal of Cooperative Information Systems"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Galstyan, A., Hogg, T., Lerman, K.: Modeling and Mathematical Analysis of Swarms of Microscopic Robots. In: SIS, pp. 201\u2013208. IEEE (2005)","DOI":"10.1109\/SIS.2005.1501623"},{"key":"7_CR13","unstructured":"Gjondrekaj, E., Loreti, M., Pugliese, R., Tiezzi, F.: Specification and Analysis of a Collective Robotics Scenario in SAM (2011), SAM source file available at http:\/\/rap.dsi.unifi.it\/SAM\/"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Gjondrekaj, E., et al.: Towards a formal verification methodology for collective robotic systems. Technical report, Univ. Firenze (2011), http:\/\/rap.dsi.unifi.it\/~loreti\/papers\/collective_transport_verification.pdf","DOI":"10.1007\/978-3-642-34281-3_7"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Jeyaraman, S., et al.: Formal techniques for the modelling and validation of a co-operating UAV team that uses Dubins set for path planning. In: ACC, vol.\u00a07, pp. 4690\u20134695. IEEE (2005)","DOI":"10.1109\/ACC.2005.1470736"},{"key":"7_CR16","series-title":"STAR","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/11552246_40","volume-title":"Experimental Robotics IX","author":"C. Jones","year":"2004","unstructured":"Jones, C., Mataric, M.J.: Synthesis and Analysis of Non-Reactive Controllers for Multi-Robot Sequential Task Domains. In: Ang, M.H., Khatib, O. (eds.) Experimental Robotics IX. STAR, vol.\u00a021, pp. 417\u2013426. Springer, Heidelberg (2004)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-15461-4_42","volume-title":"Swarm Intelligence","author":"S. Konur","year":"2010","unstructured":"Konur, S., Dixon, C., Fisher, M.: Formal Verification of Probabilistic Swarm Behaviours. In: Dorigo, M., Birattari, M., Di Caro, G.A., Doursat, R., Engelbrecht, A.P., Floreano, D., Gambardella, L.M., Gro\u00df, R., \u015eahin, E., Sayama, H., St\u00fctzle, T. (eds.) ANTS 2010. LNCS, vol.\u00a06234, pp. 440\u2013447. Springer, Heidelberg (2010)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-540-30552-1_12","volume-title":"Swarm Robotics","author":"K. Lerman","year":"2005","unstructured":"Lerman, K., Martinoli, A., Galstyan, A.: A Review of Probabilistic Macroscopic Models for Swarm Robotic Systems. In: \u015eahin, E., Spears, W.M. (eds.) Swarm Robotics WS 2004. LNCS, vol.\u00a03342, pp. 143\u2013152. Springer, Heidelberg (2005)"},{"key":"7_CR19","unstructured":"Loreti, M.: SAM: Stochastic Analyser for Mobility, http:\/\/rap.dsi.unifi.it\/SAM\/"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1145\/242223.242291","volume":"28","author":"J.A. Stankovic","year":"1996","unstructured":"Stankovic, J.A.: Strategic directions in real-time and embedded systems. ACM Comput. Surv.\u00a028, 751\u2013763 (1996)","journal-title":"ACM Comput. Surv."},{"issue":"4","key":"7_CR21","doi-asserted-by":"crossref","first-page":"363","DOI":"10.5772\/5769","volume":"2","author":"A. Winfield","year":"2005","unstructured":"Winfield, A., et al.: On Formal Specification of Emergent Behaviours in Swarm Robotic Systems. Int. Journal of Advanced Robotic Systems\u00a02(4), 363\u2013370 (2005)","journal-title":"Int. Journal of Advanced Robotic Systems"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34281-3_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,19]],"date-time":"2025-04-19T21:24:26Z","timestamp":1745097866000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34281-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642342806","9783642342813"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34281-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}