{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T09:56:16Z","timestamp":1781258176715,"version":"3.54.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031731792","type":"print"},{"value":"9783031731808","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-73180-8_3","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T08:03:51Z","timestamp":1728720231000},"page":"38-53","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verification-Oriented Specification of\u00a0Multi-agent Interaction Patterns"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-4923-7831","authenticated-orcid":false,"given":"Alberto","family":"Tagliaferro","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8724-1541","authenticated-orcid":false,"given":"Livia","family":"Lestingi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9193-9560","authenticated-orcid":false,"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. (TOMACS) 28(1), 1\u201339 (2018)","journal-title":"ACM Trans. Model. Comput. Simul. (TOMACS)"},{"issue":"2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"3_CR3","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM (JACM) 43(1), 116\u2013146 (1996)","journal-title":"J. ACM (JACM)"},{"key":"3_CR4","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s00165-020-00509-0","volume":"32","author":"MM Bersani","year":"2020","unstructured":"Bersani, M.M., Soldo, M., Menghi, C., Pelliccione, P., Rossi, M.: PuRSUE-from specification of robotic environments to synthesis of controllers. Formal Aspects Comput. 32, 187\u2013227 (2020)","journal-title":"Formal Aspects Comput."},{"issue":"5","key":"3_CR5","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1109\/TSMCA.2011.2109709","volume":"41","author":"ML Bolton","year":"2011","unstructured":"Bolton, M.L., Siminiceanu, R.I., Bass, E.J.: A systematic approach to model checking human-automation interaction using task analytic models. IEEE Trans. Syst. Man, Cybern.-Part A: Syst. Humans 41(5), 961\u2013976 (2011)","journal-title":"IEEE Trans. Syst. Man, Cybern.-Part A: Syst. Humans"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Bozhinoski, D., Di\u00a0Ruscio, D., Malavolta, I., Pelliccione, P., Tivoli, M.: Flyaq: enabling non-expert users to specify and generate missions of autonomous multicopters. In: 2015 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 801\u2013806. IEEE (2015)","DOI":"10.1109\/ASE.2015.104"},{"issue":"4","key":"3_CR7","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1093\/biomet\/26.4.404","volume":"26","author":"CJ Clopper","year":"1934","unstructured":"Clopper, C.J., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404\u2013413 (1934)","journal-title":"Biometrika"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal smc tutorial. Int. J. Softw. Tools Technol. Transfer 17, 397\u2013415 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-24310-3_7","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A David","year":"2011","unstructured":"David, A., et al.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80\u201396. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24310-3_7"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-030-66494-7_12","volume-title":"Software Engineering for Robotics","author":"S Dragule","year":"2021","unstructured":"Dragule, S., Gonzalo, S.G., Berger, T., Pelliccione, P.: Languages for specifying missions of robotic applications. In: Software Engineering for Robotics, pp. 377\u2013411. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-66494-7_12"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-23217-6_6","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"P Bouyer","year":"2011","unstructured":"Bouyer, P., Larsen, K.G., Markey, N., Sankur, O., Thrane, C.: Timed automata can always be made implementable. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 76\u201391. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23217-6_6"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-030-49062-1_40","volume-title":"Human-Computer Interaction. Multimodal and Natural Interaction","author":"P Forbrig","year":"2020","unstructured":"Forbrig, P., Bundea, A.-N.: Modelling the collaboration of a patient and an assisting humanoid robot during training tasks. In: Kurosu, M. (ed.) HCII 2020. LNCS, vol. 12182, pp. 592\u2013602. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-49062-1_40"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Garc\u00eda, S., Pelliccione, P., Menghi, C., Berger, T., Bures, T.: High-level mission specification for multiple robots. In: ACM SIGPLAN International Conference on Software Language Engineering, pp. 127\u2013140 (2019)","DOI":"10.1145\/3357766.3359535"},{"key":"3_CR14","unstructured":"Lacerda, B., Lima, P.: Ltl plan specification for robotic tasks modelled as finite state automata. In: Proceedings of Workshop ADAPT\u2013Agent Design: Advancing from Practice to Theory, Workshop at AAMAS, vol.\u00a09 (2009)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. on Softw. Tools for Tech. Transf. 1(1-2), 134\u2013152 (1997)","DOI":"10.1007\/s100090050010"},{"key":"3_CR16","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2023.104387","volume":"163","author":"L Lestingi","year":"2023","unstructured":"Lestingi, L., Zerla, D., Bersani, M.M., Rossi, M.: Specification, stochastic modeling and analysis of interactive service robotic applications. Robot. Auton. Syst. 163, 104387 (2023)","journal-title":"Robot. Auton. Syst."},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1613\/jair.1.11243","volume":"63","author":"SJ Levine","year":"2018","unstructured":"Levine, S.J., Williams, B.C.: Watching and acting together: concurrent plan recognition and adaptation for human-robot teams. J. Artif. Intell. Res. 63, 281\u2013359 (2018)","journal-title":"J. Artif. Intell. Res."},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Menghi, C., Tsigkanos, C., Pelliccione, P., Ghezzi, C., Berger, T.: Specification patterns for robotic missions. IEEE Transactions on Software Engineering (2019)","DOI":"10.1145\/3183440.3195044"},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/1050-6411(91)90023-X","volume":"1","author":"R Merletti","year":"1991","unstructured":"Merletti, R., Conte, L.L., Orizio, C.: Indices of muscle fatigue. J. Electromyogr. Kinesiol. 1(1), 20\u201333 (1991)","journal-title":"J. Electromyogr. Kinesiol."},{"key":"3_CR20","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-11900-7_17","volume-title":"Simulation, Modeling, and Programming for Autonomous Robots","author":"A Nordmann","year":"2014","unstructured":"Nordmann, A., Hochgeschwender, N., Wrede, S.: A survey on domain-specific languages in robotics. In: Brugali, D., Broenink, J.F., Kroeger, T., MacDonald, B.A. (eds.) Simulation, Modeling, and Programming for Autonomous Robots, pp. 195\u2013206. Springer International Publishing, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11900-7_17"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-0-387-35175-9_58","volume-title":"Human-Computer Interaction INTERACT \u201997","author":"F Paterno","year":"1997","unstructured":"Paterno, F., Mancini, C., Meniconi, S.: ConcurTaskTrees: a diagrammatic notation for specifying task models. In: Howard, S., Hammond, J., Lindgaard, G. (eds.) Human-Computer Interaction INTERACT \u201997, pp. 362\u2013369. Springer US, Boston, MA (1997). https:\/\/doi.org\/10.1007\/978-0-387-35175-9_58"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Ruscio, D.D., Malavolta, I., Pelliccione, P., Tivoli, M.: Automatic generation of detailed flight plans from high-level mission descriptions. In: Proceedings of the ACM\/IEEE 19th International Conference on Model Driven Engineering Languages and Systems, pp. 45\u201355 (2016)","DOI":"10.1145\/2976767.2976794"},{"issue":"3","key":"3_CR23","doi-asserted-by":"publisher","first-page":"664","DOI":"10.1016\/S0377-2217(00)00292-7","volume":"134","author":"K Salimifard","year":"2001","unstructured":"Salimifard, K., Wright, M.: Petri net-based modelling of workflow systems: an overview. Eur. J. Oper. Res. 134(3), 664\u2013676 (2001)","journal-title":"Eur. J. Oper. Res."},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.ins.2014.07.047","volume":"288","author":"DC Silva","year":"2014","unstructured":"Silva, D.C., Abreu, P.H., Reis, L.P., Oliveira, E.: Development of a flexible language for mission description for multi-robot missions. Inf. Sci. 288, 27\u201344 (2014)","journal-title":"Inf. Sci."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Tagliaferro, A., Lestingi, L., Rossi, M.: Towards verifiable multi-agent interaction pattern specification. In: International Conference on Formal Methods in Software Engineering, pp. 122\u2013126. ACM (2024)","DOI":"10.1145\/3644033.3644379"},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.automatica.2016.04.006","volume":"70","author":"J Tumova","year":"2016","unstructured":"Tumova, J., Dimarogonas, D.V.: Multi-agent planning under local ltl specifications and event-based synchronization. Automatica 70, 239\u2013248 (2016)","journal-title":"Automatica"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Van, T.N., Fredivianus, N., Tran, H.T., Geihs, K., Huynh, T.T.B.: Formal verification of ALICA multi-agent plans using model checking. In: International Symposium on Information and Communication Technology, pp. 351\u2013358 (2018)","DOI":"10.1145\/3287921.3287947"},{"issue":"4","key":"3_CR28","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/j.is.2004.02.002","volume":"30","author":"WM Van Der Aalst","year":"2005","unstructured":"Van Der Aalst, W.M., Ter Hofstede, A.H.: YAWL: yet another workflow language. Inf. Syst. 30(4), 245\u2013275 (2005)","journal-title":"Inf. Syst."}],"container-title":["Communications in Computer and Information Science","Agents and Robots for reliable Engineered Autonomy"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-73180-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T08:04:37Z","timestamp":1728720277000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-73180-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031731792","9783031731808"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-73180-8_3","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"value":"1865-0929","type":"print"},{"value":"1865-0937","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,13]]},"assertion":[{"value":"13 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"AREA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Workshop on Agents and Robots for reliable Engineered Autonomy","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Santiago de Compostela","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"area2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/areaworkshop.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}