{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T06:45:09Z","timestamp":1775803509548,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"4","funder":[{"name":"EPSRC Smart Solutions towards Cellular-Connected Unmanned Aerial Vehicles System","award":["EP\/W004364\/1"],"award-info":[{"award-number":["EP\/W004364\/1"]}]},{"name":"Explainable Human-Swarm Systems project funded by UKRI Trustworthy Autonomous Systems Hub","award":["EP\/V00784X\/1"],"award-info":[{"award-number":["EP\/V00784X\/1"]}]},{"name":"UKRI MINDS-CDT","award":["EP\/S024298\/1"],"award-info":[{"award-number":["EP\/S024298\/1"]}]},{"name":"Amazon Research Award on Automated Reasoning"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. Hum.-Robot Interact."],"published-print":{"date-parts":[[2025,12,31]]},"abstract":"<jats:p>Formal Modelling is often used as part of the design and testing process of software development to ensure that components operate within suitable bounds even in unexpected circumstances. We conducted a user study evaluation of predictive formal modelling (PFM) at runtime in a human-swarm mission to determine the benefit of PFM on performance and human-swarm interaction. A total of 180 participants were recruited to perform the role of aerial swarm operators delivering parcels to target locations in a simulation environment. The PFM model was integrated into the simulation software to inform the operator of the estimated mission completion time given the current number of drones deployed. The operator could increase the number of parcels delivered in any timestep by adding drones, which also increased costs, thus requiring the use of the minimum number of drones necessary to complete the task in the given time. We collected user feedback using standard survey questionnaires and measured performance using data obtained from the Human and Robot Interactive Swarm (HARIS) simulator. Our results show that PFM increased the performance of the human swarm team without significantly increasing the operators\u2019 workload or affecting the system\u2019s usability.<\/jats:p>","DOI":"10.1145\/3727989","type":"journal-article","created":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T00:25:44Z","timestamp":1743726344000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A User Study Evaluation of Predictive Formal Modelling at Runtime in Human-Swarm Interaction"],"prefix":"10.1145","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4637-3278","authenticated-orcid":false,"given":"Ayodeji O.","family":"Abioye","sequence":"first","affiliation":[{"name":"School of Electronics and Computer Science, University of Southampton, Southampton, United Kingdom of Great Britain and Northern Ireland and School of Computing and Communications, The Open University, Milton Keynes, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4269-5050","authenticated-orcid":false,"given":"William","family":"Hunt","sequence":"additional","affiliation":[{"name":"School of Electronics and Computer Science, University of Southampton, Southampton, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8134-5822","authenticated-orcid":false,"given":"Yue","family":"Gu","sequence":"additional","affiliation":[{"name":"School of Computing Science, University of Glasgow, Glasgow, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8372-1684","authenticated-orcid":false,"given":"Eike","family":"Schneiders","sequence":"additional","affiliation":[{"name":"School of Electronics and Computer Science, University of Southampton, Southampton, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4927-5086","authenticated-orcid":false,"given":"Mohammad","family":"Naiseh","sequence":"additional","affiliation":[{"name":"Department of Computing and Informatics, Bournemouth University, Poole, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3699-6658","authenticated-orcid":false,"given":"Blair","family":"Archibald","sequence":"additional","affiliation":[{"name":"School of Computing Science, University of Glasgow, Glasgow, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6773-9481","authenticated-orcid":false,"given":"Michele","family":"Sevegnani","sequence":"additional","affiliation":[{"name":"School of Computing Science, University of Glasgow, Glasgow, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9686-4302","authenticated-orcid":false,"given":"Sarvapali D.","family":"Ramchurn","sequence":"additional","affiliation":[{"name":"School of Electronics and Computer Science, University of Southampton, Southampton, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8878-2454","authenticated-orcid":false,"given":"Joel E.","family":"Fischer","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Nottingham, Nottingham, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6954-1284","authenticated-orcid":false,"given":"Mohammad D.","family":"Soorati","sequence":"additional","affiliation":[{"name":"School of Electronics and Computer Science, University of Southampton, Southampton, United Kingdom of Great Britain and Northern Ireland"}]}],"member":"320","published-online":{"date-parts":[[2025,6,11]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Ayodeji O. Abioye William Hunt Yue Gu Eike Schneiders Mohammad Naiseh Blair Archibald Michele Sevegnani Sarvapali D. Ramchurn Joel E. Fischer and Mohammad D. Soorati. 2025. Research data for paper: A user study evaluation of predictive formal modelling at runtime in human-swarm interaction. Dataset (Mar. 2025). Figshare. DOI: 10.6084\/m9.figshare.28687238","DOI":"10.6084\/m9.figshare.28687238"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3610978.3640725"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/RO-MAN57019.2023.10309454"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.3390\/su14010360"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2012.292"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.326"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2909824.3020211"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.5555\/2936924.2937100"},{"key":"e_1_3_2_12_2","first-page":"189","volume-title":"Usability Evaluation in Industry","author":"Brooke John","year":"1996","unstructured":"John Brooke. 1996. Chapter 21: SUS: A quick and dirty usability scale. In Usability Evaluation in Industry. Patrick W. Jordan, B. Thomas, Ian Lyall McClelland, and Bernard Weerdmeester (Eds.), CRC Press, 189\u2013194."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.5898\/JHRI.5.1.Brown"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0270-3"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2017.2650901"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2021.3074883"},{"key":"e_1_3_2_17_2","first-page":"1","volume-title":"Proceedings of the AAAI 2022 Spring Symposium Series (Putting AI in the Critical Loop: Assured Trust and Autonomy in Human-Machine Teams)","author":"Clark Jediah R.","year":"2022","unstructured":"Jediah R. Clark, Mohammad Naiseh, Joel Fischer, Maris\u00e9 Galvez Trigo, Katie Parnell, Mario Brito, Adrian Bodenmann, Sarvapali D. Ramchurn, and Mohammad D. Soorati. 2022. Industry led use-case development for human-swarm operations. In Proceedings of the AAAI 2022 Spring Symposium Series (Putting AI in the Critical Loop: Assured Trust and Autonomy in Human-Machine Teams). AAAI, 1\u20136."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3442679"},{"key":"e_1_3_2_19_2","unstructured":"DHHS. 2013. System Usability Scale (SUS)\u2014Department of Health and Human Services. Retrieved from https:\/\/www.usability.gov\/how-to-and-tools\/methods\/system-usability-scale.html"},{"key":"e_1_3_2_20_2","first-page":"189","article-title":"Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges","volume":"10","author":"Erlang Agner Krarup","year":"1917","unstructured":"Agner Krarup Erlang. 1917. Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges. Post Office Electrical Engineer\u2019s Journal 10 (1917), 189\u2013197.","journal-title":"Post Office Electrical Engineer\u2019s Journal"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00609-z"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531146.3533202"},{"issue":"2","key":"e_1_3_2_23_2","doi-asserted-by":"crossref","first-page":"1664","DOI":"10.1109\/TIV.2022.3172342","article-title":"Toward safe and efficient human\u2013swarm collaboration: A hierarchical multi-agent pickup and delivery framework","volume":"8","author":"Gong Xin","year":"2022","unstructured":"Xin Gong, Tieniu Wang, Tingwen Huang, and Yukang Cui. 2022. Toward safe and efficient human\u2013swarm collaboration: A hierarchical multi-agent pickup and delivery framework. IEEE Transactions on Intelligent Vehicles 8, 2 (2022), 1664\u20131675.","journal-title":"IEEE Transactions on Intelligent Vehicles"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/RO-MAN57019.2023.10309626"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-4115(08)62386-9"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/3545946.3599173"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1207\/S15327566IJCE0401_04"},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1109\/UR57808.2023.10202489","volume-title":"Proceedings of the 2023 20th International Conference on Ubiquitous Robots (UR)","author":"Khavas Zahra Rezaei","year":"2023","unstructured":"Zahra Rezaei Khavas, Amin Majdi, S. Reza Ahmadzadeh, and Paul Robinette. 2023. Human trust after drone failure: Study of the effects of drone type and failure type on human-drone trust. In Proceedings of the 2023 20th International Conference on Ubiquitous Robots (UR). IEEE, 685\u2013692."},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/s43154-020-00029-y"},{"issue":"2","key":"e_1_3_2_30_2","first-page":"104","article-title":"Human swarm interaction: An experimental study of two types of interaction with foraging swarms","volume":"2","author":"Kolling Andreas","year":"2013","unstructured":"Andreas Kolling, Katia Sycara, Steve Nunnally, and Michael Lewis. 2013. Human swarm interaction: An experimental study of two types of interaction with foraging swarms. Journal of Human-Robot Interaction 2, 2 (2013), 104\u2013129.","journal-title":"Journal of Human-Robot Interaction"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/THMS.2015.2480801"},{"issue":"6","key":"e_1_3_2_32_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3529225","article-title":"The placebo effect of artificial intelligence in human\u2013computer interaction","volume":"29","author":"Kosch Thomas","year":"2023","unstructured":"Thomas Kosch, Robin Welsch, Lewis Chuang, and Albrecht Schmidt. 2023. The placebo effect of artificial intelligence in human\u2013computer interaction. ACM Transactions on Computer-Human Interaction 29, 6 (2023), 1\u201332.","journal-title":"ACM Transactions on Computer-Human Interaction"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/2832249.2832399"},{"key":"e_1_3_2_34_2","first-page":"585","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV \u201911)","author":"Kwiatkowska Marta","year":"2011","unstructured":"Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV \u201911). Springer, 585\u2013591."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1177\/2515245918770963"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.chb.2022.107539"},{"key":"e_1_3_2_37_2","volume-title":"Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS)","author":"Liu Minghua","year":"2019","unstructured":"Minghua Liu, Hang Ma, Jiaoyang Li, and Sven Koenig. 2019. Task and path planning for multi-agent pickup and delivery. In Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS)."},{"key":"e_1_3_2_38_2","first-page":"325","volume-title":"Proceedings of the 29th International Conference on International Joint Conferences on Artificial Intelligence","author":"Lomuscio Alessio","year":"2021","unstructured":"Alessio Lomuscio and Edoardo Pirovano. 2021. Verifying fault-tolerance in probabilistic swarm systems. In Proceedings of the 29th International Conference on International Joint Conferences on Artificial Intelligence, 325\u2013331."},{"key":"e_1_3_2_39_2","volume-title":"Proceedings of the AAAI Conference on Artificial Intelligence","volume":"30","author":"Ma Hang","year":"2016","unstructured":"Hang Ma, Craig Tovey, Guni Sharon, T. K. Kumar, and Sven Koenig. 2016. Multi-agent path finding with payload transfers and the package-exchange robot-routing problem. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 30."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3610578"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3368854"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11280-021-00916-0"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-51497-5_3"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-017-9269-4"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1080\/10447318.2022.2108961"},{"key":"e_1_3_2_46_2","first-page":"1184","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI)","author":"Ramchurn Sarvapali D.","year":"2015","unstructured":"Sarvapali D. Ramchurn, Joel E. Fischer, Yuki Ikuno, Feng Wu, Jack Flann, and Antony Waldock. 2015. A study of human-agent collaboration for multi-UAV task allocation in dynamic environments. In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI), 1184\u20131192."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/HRI.2016.7451740"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.5555\/3398761.3398959"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3488242"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-443-15988-6.00008-X"},{"key":"e_1_3_2_51_2","first-page":"376","volume-title":"Proceedings of the International Conference on Computing, Intelligence and Data Analytics","author":"Suffian Muhammad","year":"2023","unstructured":"Muhammad Suffian. 2023. Explainable AI assisted decision-making and human behaviour. In Proceedings of the International Conference on Computing, Intelligence and Data Analytics. Springer, 376\u2013385."},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0968-090X(96)00025-3"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3613905.3636304"},{"key":"e_1_3_2_54_2","doi-asserted-by":"crossref","first-page":"3567","DOI":"10.1109\/SMC.2014.6974483","volume-title":"Proceedings of the 2014 IEEE International Conference on Systems, Man, and Cybernetics (SMC)","author":"Walker Phillip","year":"2014","unstructured":"Phillip Walker, Saman Amirpour Amraii, Michael Lewis, Nilanjan Chakraborty, and Katia Sycara. 2014. Control of swarms with multiple leader agents. In Proceedings of the 2014 IEEE International Conference on Systems, Man, and Cybernetics (SMC). IEEE, 3567\u20133572."},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.5555\/647771.760735"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3368589"}],"container-title":["ACM Transactions on Human-Robot Interaction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3727989","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T16:40:14Z","timestamp":1749660014000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3727989"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,11]]},"references-count":55,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12,31]]}},"alternative-id":["10.1145\/3727989"],"URL":"https:\/\/doi.org\/10.1145\/3727989","relation":{},"ISSN":["2573-9522"],"issn-type":[{"value":"2573-9522","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,11]]},"assertion":[{"value":"2024-05-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-28","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}