{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:45:18Z","timestamp":1742949918964,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030974565"},{"type":"electronic","value":"9783030974572"}],"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-030-97457-2_12","type":"book-chapter","created":{"date-parts":[[2022,3,9]],"date-time":"2022-03-09T11:03:04Z","timestamp":1646823784000},"page":"198-217","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification of a Map Merging Protocol in the Multi-agent Programming Contest"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6444-9312","authenticated-orcid":false,"given":"Matt","family":"Luckcuck","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6666-6954","authenticated-orcid":false,"given":"Rafael C.","family":"Cardoso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,10]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Ahlbrecht, T., Dix, J., Fiekas, N., Krausburg, T.: The multi-agent programming contest: a r\u00e9sum\u00e9. In: Ahlbrecht, T., Dix, J., Fiekas, N., Krausburg, T. (eds.) MAPC 2019, pp. 3\u201327. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59299-8_1","DOI":"10.1007\/978-3-030-59299-8_1"},{"key":"12_CR2","unstructured":"Akhtar, N., Missen, M.M.S.: Contribution to the formal specification and verification of a multi-agent robotic system. Eur. J. Sci. Res. 117(1), 35\u201355 (2014). http:\/\/www.europeanjournalofscientificresearch.com"},{"issue":"5","key":"12_CR3","doi-asserted-by":"publisher","first-page":"1251","DOI":"10.1007\/s10489-017-1112-z","volume":"48","author":"NA Bakar","year":"2018","unstructured":"Bakar, N.A., Selamat, A.: Agent systems verification: systematic literature review and mapping. Appl. Intell. 48(5), 1251\u20131274 (2018). https:\/\/doi.org\/10.1007\/s10489-017-1112-z","journal-title":"Appl. Intell."},{"key":"12_CR4","volume-title":"Multi-Agent Oriented Programming: Programming Multi-Agent Systems Using JaCaMo. Intelligent Robotics and Autonomous Agents Series","author":"O Boissier","year":"2020","unstructured":"Boissier, O., Bordini, R., Hubner, J., Ricci, A.: Multi-Agent Oriented Programming: Programming Multi-Agent Systems Using JaCaMo. Intelligent Robotics and Autonomous Agents Series. MIT Press, Cambridge (2020)"},{"issue":"6","key":"12_CR5","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1016\/j.scico.2011.10.004","volume":"78","author":"O Boissier","year":"2013","unstructured":"Boissier, O., Bordini, R.H., H\u00fcbner, J.F., Ricci, A., Santi, A.: Multi-agent oriented programming with JaCaMo. Sci. Comput. Program. 78(6), 747\u2013761 (2013). https:\/\/doi.org\/10.1016\/j.scico.2011.10.004","journal-title":"Sci. Comput. Program."},{"key":"12_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71956-4","volume-title":"Programming Multi-Agent Systems in AgentSpeak Using Jason","author":"RH Bordini","year":"2007","unstructured":"Bordini, R.H., Wooldridge, M., H\u00fcbner, J.F.: Programming Multi-Agent Systems in AgentSpeak Using Jason. Wiley, Hoboken (2007)"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Cardoso, R.C., Farrell, M., Luckcuck, M., Ferrando, A., Fisher, M.: Heterogeneous verification of an autonomous curiosity rover. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NASA Formal Methods, pp. 353\u2013360. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_20","DOI":"10.1007\/978-3-030-55754-6_20"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Cardoso, R.C., Ferrando, A., Papacchini, F.: LFC: combining autonomous agents and automated planning in the multi-agent programming contest. In: Ahlbrecht, T., Dix, J., Fiekas, N., Krausburg, T. (eds.) MAPC 2019, pp. 31\u201358. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59299-8_2","DOI":"10.1007\/978-3-030-59299-8_2"},{"key":"12_CR9","unstructured":"Dennis, L.A., Farwer, B.: Gwendolen: a BDI language for verifiable agents. In: Workshop on Logic and the Simulation of Interaction and Reasoning. AISB (2008)"},{"issue":"1","key":"12_CR10","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","volume":"19","author":"LA Dennis","year":"2012","unstructured":"Dennis, L.A., Fisher, M., Webster, M., Bordini, R.H.: Model checking agent programming languages. Autom. Softw. Eng. 19(1), 5\u201363 (2012). https:\/\/doi.org\/10.1007\/s10515-011-0088-x","journal-title":"Autom. Softw. Eng."},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"van Eijk, R.M., de Boer, F.S., van der Hoek, W., Meyer, J.J.C.: Process algebra for agent communication: a general semantic approach. In: Huget, M.P. (ed.) Communication in Multiagent Systems. LNCS, pp. 113\u2013128. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-44972-0_5","DOI":"10.1007\/978-3-540-44972-0_5"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Farrell, M., Luckcuck, M., Fisher, M.: Robotics and integrated formal methods: necessity meets opportunity. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 161\u2013171. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_10","DOI":"10.1007\/978-3-319-98938-9_10"},{"key":"12_CR13","unstructured":"Ferrando, A., Ancona, D., Mascardi, V.: Decentralizing MAS monitoring with DecAMon. In: Larson, K., Winikoff, M., Das, S., Durfee, E.H. (eds.) Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, S\u00e3o Paulo, Brazil, 8\u201312 May 2017, pp. 239\u2013248. ACM (2017). http:\/\/dl.acm.org\/citation.cfm?id=3091164"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.: FDR3 - a modern model checker for CSP. In: TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Gracanin, D., Singh, H.L., Hinchey, M.G., Eltoweissy, M., Bohner, S.A.: A CSP-based agent modeling framework for the Cougaar agent-based architecture. In: 12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS 2005), pp. 255\u2013262. IEEE (2005). https:\/\/doi.org\/10.1109\/ECBS.2005.6","DOI":"10.1109\/ECBS.2005.6"},{"issue":"8","key":"12_CR16","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978). https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997). 10\/d7wqxt. http:\/\/ieeexplore.ieee.org\/document\/588521\/","DOI":"10.1109\/32.588521"},{"key":"12_CR18","unstructured":"Huang, X., van der Meyden, R.: Symbolic model checking epistemic strategy logic. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, pp. 1426\u20131432. AAAI Press (2014). https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/8894"},{"issue":"3\/4","key":"12_CR19","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1504\/IJAOSE.2007.016266","volume":"1","author":"JF H\u00fcbner","year":"2007","unstructured":"H\u00fcbner, J.F., Sichman, J.S., Boissier, O.: Developing organised multiagent systems using the MOISE+, model: programming issues at the system and agent levels. Int. J. Agent-Oriented Softw. Eng. 1(3\/4), 370\u2013395 (2007). https:\/\/doi.org\/10.1504\/IJAOSE.2007.016266","journal-title":"Int. J. Agent-Oriented Softw. Eng."},{"key":"12_CR20","first-page":"213","volume":"42","author":"N Izumi","year":"1990","unstructured":"Izumi, N., Takamatsu, S., Kise, K., Fukunaga, K.: CSP-based formulation of multi-agent communication for a first-order agent theory. Commitment 42, 213\u2013261 (1990)","journal-title":"Commitment"},{"key":"12_CR21","unstructured":"Kacem, A.H., Kacem, N.H.: From formal specification to model checking of MAS using CSP-Z and SPIN. Int. J. Comput. Inf. Sci. 5(1) (2007). http:\/\/www.ijcis.info\/Vol5N1.htm"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Lomuscio, A., Raimondi, F.: MCMAS: a model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450\u2013454. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_31","DOI":"10.1007\/11691372_31"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal Specification and Verification of Autonomous Robotic Systems: a Survey. ACM Comput. Surv. 52(5), 1\u201341 (2019). https:\/\/doi.org\/10.1145\/3342355. http:\/\/dl.acm.org\/citation.cfm?doid=3362097.3342355","DOI":"10.1145\/3342355"},{"issue":"2\u20133","key":"12_CR24","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/s11721-013-0079-6","volume":"7","author":"M Massink","year":"2013","unstructured":"Massink, M., Brambilla, M., Latella, D., Dorigo, M., Birattari, M.: On the use of Bio-PEPA for modelling and analysing collective behaviours in swarm robotics. Swarm Intell. 7(2\u20133), 201\u2013228 (2013). https:\/\/doi.org\/10.1007\/s11721-013-0079-6","journal-title":"Swarm Intell."},{"key":"12_CR25","unstructured":"Rao, A.S., Georgeff, M.: BDI agents: from theory to practice. In: Proceedings of the 1st International Conference on Multi-Agent Systems (ICMAS), San Francisco, USA, pp. 312\u2013319, June 1995"},{"key":"12_CR26","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-0-387-89299-3_8","volume-title":"Multi-Agent Programming","author":"A Ricci","year":"2009","unstructured":"Ricci, A., Piunti, M., Viroli, M., Omicini, A.: Environment programming in CArtAgO. In: El Fallah Seghrouchni, A., Dix, J., Dastani, M., Bordini, R.H. (eds.) Multi-Agent Programming, pp. 259\u2013288. Springer, Boston, MA (2009). https:\/\/doi.org\/10.1007\/978-0-387-89299-3_8"},{"key":"12_CR27","series-title":"International Series in Computer Science","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. International Series in Computer Science, Prentice-Hall, New York (1992)"},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Van Eijk, R.M., De Boer, F.S., Van Der Hoek, W., Meyer, J.J.C.: A verification framework for agent communication. Auton. Agents Multi-Agent Syst. 6(2), 185\u2013219 (2003). 10\/dzcsw4. https:\/\/doi.org\/10.1023\/A:1021836202093","DOI":"10.1023\/A:1021836202093"},{"key":"12_CR29","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1613\/jair.2221","volume":"29","author":"R Vieira","year":"2007","unstructured":"Vieira, R., Moreira, \u00c1.F., Wooldridge, M., Bordini, R.H.: On the formal semantics of speech-act based communication in an agent-oriented programming language. J. Artif. Intell. Res. (JAIR) 29, 221\u2013267 (2007). https:\/\/doi.org\/10.1613\/jair.2221","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"issue":"5","key":"12_CR30","doi-asserted-by":"publisher","first-page":"1094","DOI":"10.1007\/s10458-016-9356-2","volume":"31","author":"M Winikoff","year":"2017","unstructured":"Winikoff, M.: BDI agent testability revisited. Auton. Agents Multi-Agent Syst. 31(5), 1094\u20131132 (2017). https:\/\/doi.org\/10.1007\/s10458-016-9356-2","journal-title":"Auton. Agents Multi-Agent Syst."},{"issue":"11","key":"12_CR31","doi-asserted-by":"publisher","first-page":"13555","DOI":"10.1016\/j.eswa.2011.04.067","volume":"38","author":"WL Yeung","year":"2011","unstructured":"Yeung, W.L.: Behavioral modeling and verification of multi-agent systems for manufacturing control. Expert Syst. Appl. 38(11), 13555\u201313562 (2011). https:\/\/doi.org\/10.1016\/j.eswa.2011.04.067","journal-title":"Expert Syst. Appl."},{"issue":"2\/3","key":"12_CR32","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1504\/IJAOSE.2016.080889","volume":"5","author":"MR Zatelli","year":"2016","unstructured":"Zatelli, M.R., Ricci, A., H\u00fcbner, J.F.: Integrating interaction with agents, environment, and organisation in JaCaMo. Int. J. Agent-Oriented Softw. Eng. 5(2\/3), 266\u2013302 (2016). https:\/\/doi.org\/10.1504\/IJAOSE.2016.080889","journal-title":"Int. J. Agent-Oriented Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Engineering Multi-Agent Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-97457-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,9]],"date-time":"2022-03-09T11:06:44Z","timestamp":1646824004000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-97457-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030974565","9783030974572"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-97457-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"10 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"EMAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Engineering Multi-Agent Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 May 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"emas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/emas2021.in.tu-clausthal.de\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"74% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}