{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T15:53:09Z","timestamp":1762876389183,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T00:00:00Z","timestamp":1652832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,5,18]]},"DOI":"10.1145\/3524482.3527653","type":"proceedings-article","created":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T22:06:57Z","timestamp":1658441217000},"page":"80-90","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Formal modeling and verification of multi-robot interactive scenarios in service settings"],"prefix":"10.1145","author":[{"given":"Livia","family":"Lestingi","sequence":"first","affiliation":[{"name":"Politecnico di Milano, Milan, Italy"}]},{"given":"Cristian","family":"Sbrolli","sequence":"additional","affiliation":[{"name":"Politecnico di Milano, Milan, Italy"}]},{"given":"Pasquale","family":"Scarmozzino","sequence":"additional","affiliation":[{"name":"Politecnico di Milano, Milan, Italy"}]},{"given":"Giorgio","family":"Romeo","sequence":"additional","affiliation":[{"name":"Politecnico di Milano, Milan, Italy"}]},{"given":"Marcello M.","family":"Bersani","sequence":"additional","affiliation":[{"name":"Politecnico di Milano, Milan, Italy"}]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[{"name":"Politecnico di Milano, Milan, Italy"}]}],"member":"320","published-online":{"date-parts":[[2022,7,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3472307.3484672"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00509-0"},{"key":"e_1_3_2_1_5_1","unstructured":"BlueBotics. 2021. Automated Hospital Logistics: How AGVs are Keeping PPE Moving. https:\/\/bluebotics.com\/agvs-hospital-logistics\/.  BlueBotics. 2021. Automated Hospital Logistics: How AGVs are Keeping PPE Moving. https:\/\/bluebotics.com\/agvs-hospital-logistics\/."},{"key":"e_1_3_2_1_6_1","first-page":"37","article-title":"Free will is compatible with randomness","volume":"4","author":"Calude CSKF","year":"2016","unstructured":"CSKF Calude and N Poznanovic . 2016 . Free will is compatible with randomness . Philosophical Inquiries 4 , 2 (2016), 37 -- 52 . CSKF Calude and N Poznanovic. 2016. Free will is compatible with randomness. Philosophical Inquiries 4, 2 (2016), 37--52.","journal-title":"Philosophical Inquiries"},{"key":"e_1_3_2_1_7_1","volume-title":"Formal Verification for Human-Robot Interaction in Medical Environments. In Intl. Conf. on Human-Robot Interaction. ACM","author":"Choi Benjamin J.","year":"2021","unstructured":"Benjamin J. Choi , Ju-Youn Park , and Chung Hyuk Park . 2021 . Formal Verification for Human-Robot Interaction in Medical Environments. In Intl. Conf. on Human-Robot Interaction. ACM , Boulder, CO, USA, 181--185. Benjamin J. Choi, Ju-Youn Park, and Chung Hyuk Park. 2021. Formal Verification for Human-Robot Interaction in Medical Environments. In Intl. Conf. on Human-Robot Interaction. ACM, Boulder, CO, USA, 181--185."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/26.4.404"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0361-y"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24310-3_7"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.3389\/frobt.2018.00094"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2015.11.012"},{"key":"e_1_3_2_1_13_1","volume-title":"Simultaneous Task Allocation and Planning Under Uncertainty. In Intl. Conf. on Intelligent Robots and Systems. IEEE","author":"Faruq Fatma","year":"2018","unstructured":"Fatma Faruq , David Parker , Bruno Lacerda , and Nick Hawes . 2018 . Simultaneous Task Allocation and Planning Under Uncertainty. In Intl. Conf. on Intelligent Robots and Systems. IEEE , Madrid, Spain, 3559--3564. Fatma Faruq, David Parker, Bruno Lacerda, and Nick Hawes. 2018. Simultaneous Task Allocation and Planning Under Uncertainty. In Intl. Conf. on Intelligent Robots and Systems. IEEE, Madrid, Spain, 3559--3564."},{"key":"e_1_3_2_1_14_1","volume-title":"On Implementable Timed Automata. In Intl. Conf. on Formal Techniques for Distributed Objects, Components, and Systems. Springer, Valletta, Malta, 78--95","author":"Feo-Arenis Sergio","year":"2020","unstructured":"Sergio Feo-Arenis , Milan Vujinovi\u0107 , and Bernd Westphal . 2020 . On Implementable Timed Automata. In Intl. Conf. on Formal Techniques for Distributed Objects, Components, and Systems. Springer, Valletta, Malta, 78--95 . Sergio Feo-Arenis, Milan Vujinovi\u0107, and Bernd Westphal. 2020. On Implementable Timed Automata. In Intl. Conf. on Formal Techniques for Distributed Objects, Components, and Systems. Springer, Valletta, Malta, 78--95."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3447246"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Sergio Garc\u00eda Daniel Str\u00fcber Davide Brugali Thorsten Berger and Patrizio Pelliccione. 2020. Robotics software engineering: a perspective from the service robotics domain. In ESEC\/FSE. ACM Virtual Event USA 593--604.  Sergio Garc\u00eda Daniel Str\u00fcber Davide Brugali Thorsten Berger and Patrizio Pelliccione. 2020. Robotics software engineering: a perspective from the service robotics domain. In ESEC\/FSE. ACM Virtual Event USA 593--604.","DOI":"10.1145\/3368089.3409743"},{"key":"e_1_3_2_1_17_1","volume-title":"Stochastic processes and statistical inference. Arkiv f\u00f6r matematik 1, 3","author":"Grenander Ulf","year":"1950","unstructured":"Ulf Grenander . 1950. Stochastic processes and statistical inference. Arkiv f\u00f6r matematik 1, 3 ( 1950 ), 195--277. Ulf Grenander. 1950. Stochastic processes and statistical inference. Arkiv f\u00f6r matematik 1, 3 (1950), 195--277."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/3101290.3101303"},{"volume-title":"Robots and robotic devices - Safety requirements for personal care robots","author":"ISO","key":"e_1_3_2_1_19_1","unstructured":"ISO 13482. 2014. Robots and robotic devices - Safety requirements for personal care robots . ISO , Geneva, Switzerland . ISO 13482. 2014. Robots and robotic devices - Safety requirements for personal care robots. ISO, Geneva, Switzerland."},{"key":"e_1_3_2_1_20_1","first-page":"38","article-title":"Work\/rest: Part ii-the scientific basis (knowledge base) for the guide 1","volume":"1","author":"Konz Stephan","year":"2000","unstructured":"Stephan Konz . 2000 . Work\/rest: Part ii-the scientific basis (knowledge base) for the guide 1 . EGPS 1 , 401 (2000), 38 . Stephan Konz. 2000. Work\/rest: Part ii-the scientific basis (knowledge base) for the guide 1. EGPS 1, 401 (2000), 38.","journal-title":"EGPS"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3433637"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"volume-title":"Software Engineering and Formal Methods","author":"Lestingi Livia","key":"e_1_3_2_1_23_1","unstructured":"Livia Lestingi , Mehrnoosh Askarpour , Marcello M Bersani , and Matteo Rossi . 2020. Formal Verification of Human-Robot Interaction in Healthcare Scenarios . In Software Engineering and Formal Methods . Springer , Amsterdam, The Netherlands, 303--324. Livia Lestingi, Mehrnoosh Askarpour, Marcello M Bersani, and Matteo Rossi. 2020. Formal Verification of Human-Robot Interaction in Healthcare Scenarios. In Software Engineering and Formal Methods. Springer, Amsterdam, The Netherlands, 303--324."},{"key":"e_1_3_2_1_24_1","volume-title":"Intl. Conf, on Systems, Man, and Cybernetics","author":"Lestingi Livia","year":"1907","unstructured":"Livia Lestingi , Mehrnoosh Askarpour , Marcello M Bersani , and Matteo Rossi . 2020. A Model-driven Approach for the Formal Analysis of Human-Robot Interaction Scenarios . In Intl. Conf, on Systems, Man, and Cybernetics . IEEE, Toronto, ON , Canada , 1907 --1914. Livia Lestingi, Mehrnoosh Askarpour, Marcello M Bersani, and Matteo Rossi. 2020. A Model-driven Approach for the Formal Analysis of Human-Robot Interaction Scenarios. In Intl. Conf, on Systems, Man, and Cybernetics. IEEE, Toronto, ON, Canada, 1907--1914."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3117852"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1080\/00140139.2017.1416180"},{"key":"e_1_3_2_1_27_1","volume-title":"Probabilistic Verification of Multi-robot Missions in Uncertain Environments. In Intl. Conf. on Tools with Artificial Intelligence. IEEE Computer Society, Vietri sul Mare, Italy, 56--63","author":"Lyons Damian M.","year":"2015","unstructured":"Damian M. Lyons , Ronald C. Arkin , Shu Jiang , Dagan Harrington , Feng Tang , and Peng Tang . 2015 . Probabilistic Verification of Multi-robot Missions in Uncertain Environments. In Intl. Conf. on Tools with Artificial Intelligence. IEEE Computer Society, Vietri sul Mare, Italy, 56--63 . Damian M. Lyons, Ronald C. Arkin, Shu Jiang, Dagan Harrington, Feng Tang, and Peng Tang. 2015. Probabilistic Verification of Multi-robot Missions in Uncertain Environments. In Intl. Conf. on Tools with Artificial Intelligence. IEEE Computer Society, Vietri sul Mare, Italy, 56--63."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3195046"},{"key":"e_1_3_2_1_29_1","unstructured":"PAL Robotics. 2020. TIAGo Delivery makes an impact in hospitals tackling COVID-19 thanks to DIH-HERO. https:\/\/tinyurl.com\/muvtr5m8.  PAL Robotics. 2020. TIAGo Delivery makes an impact in hospitals tackling COVID-19 thanks to DIH-HERO. https:\/\/tinyurl.com\/muvtr5m8."},{"key":"e_1_3_2_1_30_1","volume-title":"Computational Tools for Human-Robot Interaction Design. In Intl. Conf. on Human-Robot Interaction. IEEE","author":"Porfirio David","year":"2019","unstructured":"David Porfirio , Allison Saupp\u00e9 , Aws Albarghouthi , and Bilge Mutlu . 2019 . Computational Tools for Human-Robot Interaction Design. In Intl. Conf. on Human-Robot Interaction. IEEE , Daegu, South Korea, 733--735. David Porfirio, Allison Saupp\u00e9, Aws Albarghouthi, and Bilge Mutlu. 2019. Computational Tools for Human-Robot Interaction Design. In Intl. Conf. on Human-Robot Interaction. IEEE, Daegu, South Korea, 733--735."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2004.1302413"},{"volume-title":"Towards the formal verification of human-agent-robot teamwork. Ph. D. Dissertation","author":"Stocker Richard","key":"e_1_3_2_1_32_1","unstructured":"Richard Stocker . 2013. Towards the formal verification of human-agent-robot teamwork. Ph. D. Dissertation . University of Liverpool , UK. Richard Stocker. 2013. Towards the formal verification of human-agent-robot teamwork. Ph. D. Dissertation. University of Liverpool, UK."},{"key":"e_1_3_2_1_33_1","volume-title":"Multi-Robot Planning Under Uncertainty with Congestion-Aware Models. In Intl. Conf. on Autonomous Agents and Multiagent Systems. International Foundation for Autonomous Agents and Multiagent Systems","author":"Street Charlie","year":"2020","unstructured":"Charlie Street , Bruno Lacerda , Manuel M\u00fchlig , and Nick Hawes . 2020 . Multi-Robot Planning Under Uncertainty with Congestion-Aware Models. In Intl. Conf. on Autonomous Agents and Multiagent Systems. International Foundation for Autonomous Agents and Multiagent Systems , Auckland, New Zealand, 1314--1322. Charlie Street, Bruno Lacerda, Manuel M\u00fchlig, and Nick Hawes. 2020. Multi-Robot Planning Under Uncertainty with Congestion-Aware Models. In Intl. Conf. on Autonomous Agents and Multiagent Systems. International Foundation for Autonomous Agents and Multiagent Systems, Auckland, New Zealand, 1314--1322."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15651-9_26"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1177\/0278364919883338"},{"volume-title":"Safety Analysis and Risk Assessment for Personal Care Robots. In Intl. Conf. on Intelligent Robots and Systems. IEEE","author":"Yakymets N.","key":"e_1_3_2_1_36_1","unstructured":"N. Yakymets , M. Sango , S. Dhouib , and R. Gelin . 2018. Model-Based Engineering , Safety Analysis and Risk Assessment for Personal Care Robots. In Intl. Conf. on Intelligent Robots and Systems. IEEE , Madrid, Spain, 6136--6141. N. Yakymets, M. Sango, S. Dhouib, and R. Gelin. 2018. Model-Based Engineering, Safety Analysis and Risk Assessment for Personal Care Robots. In Intl. Conf. on Intelligent Robots and Systems. IEEE, Madrid, Spain, 6136--6141."}],"event":{"name":"FormaliSE '22: International Conference on Formal Methods in Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Pittsburgh Pennsylvania","acronym":"FormaliSE '22"},"container-title":["Proceedings of the IEEE\/ACM 10th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527653","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3524482.3527653","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:51Z","timestamp":1750183791000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524482.3527653"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,18]]},"references-count":36,"alternative-id":["10.1145\/3524482.3527653","10.1145\/3524482"],"URL":"https:\/\/doi.org\/10.1145\/3524482.3527653","relation":{},"subject":[],"published":{"date-parts":[[2022,5,18]]},"assertion":[{"value":"2022-07-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}