The Effect of Predictive Formal Modelling at Runtime on Performance in Human-Swarm Interaction
Ayodeji O. Abioye, William Hunt, Yue Gu, Eike Schneiders, Mohammad Naiseh, Joel E. Fischer, Sarvapali D. Ramchurn, Mohammad D. Soorati, Blair Archibald, Michele Sevegnani
TL;DR
The paper addresses how runtime predictive formal modelling (PFM) can support decision-making in human-swarm interaction for UAV delivery tasks. It integrates PFM into the HARIS simulator to provide real-time feasibility estimates and an estimated completion time when the probability of success reaches $0.99$, guiding operator actions. A within-subject study with 60 participants shows that PFM improves task completion speed and the number of tasks completed without increasing mental workload or reducing usability, though it does not significantly change total agent count or per-task cost. The contributions include implementing a runtime PFM pipeline within HARIS and providing empirical evidence of performance gains under time and budget constraints, while future work should explore trust, explainability, and operator guidance with potential neurophysiological workload measures.$0.99$.
Abstract
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. In this paper, we use predictive formal modelling (PFM) at runtime in a human-swarm mission and show that this integration can be used to improve the performance of human-swarm teams. We recruited 60 participants to operate a simulated aerial swarm to deliver parcels to target locations. In the PFM condition, operators were informed of the estimated completion times given the number of drones deployed, whereas in the No-PFM condition, operators did not have this information. The operators could control the mission by adding or removing drones from the mission and thereby, increasing or decreasing the overall mission cost. The evaluation of human-swarm performance relied on four key metrics: the time taken to complete tasks, the number of agents involved, the total number of tasks accomplished, and the overall cost associated with the human-swarm task. Our results show that PFM modelling at runtime improves mission performance without significantly affecting the operator's workload or the system's usability.