Formal Modeling and Verification of Multi-Robot Interactive Scenarios in Service Settings

Service robots are increasingly widespread in healthcare and domestic assistance settings. Nevertheless, the literature still lacks robotic application development approaches that can deal with the complexity of multi-agent systems and the unpredictability of human behavior. We target this issue by building upon a model-driven development framework for human-robot interactive scenarios that relies on formal analysis (Statistical Model Checking) to estimate the probability of success of the robotic mission. We extend the framework's scope to scenarios featuring multi-robot fleets, a broader range of human-robot interaction contingencies, and task handover between robots. We also present an extended model of human behavior to capture interaction patterns implying close contact or competition with the robot. In the latter case, the user can specify alternative mission plans for the robot, depending on the competition outcome. We illustrate the approach's effectiveness and scalability through a case study from the healthcare setting, featuring multiple mobile robots and humans with diverse physiological characteristics and requesting a broad spectrum of services.