Formal Verification for Human-Robot Interaction in Medical Environments

Abstract

We present a formal verification method that provides a model-based approach to human-robot interaction (HRI) in medical settings by utilizing linear temporal logic (LTL). We define high-level HRI procedures with an LTL-based framework to create algorithmically sound robots that can function independently in dynamic HRI environments. Our approach's theoretical infallibility confers particular advantages for medical robots, where safety and informative communications are crucial. In order to establish the viability of our proposed method, and with the ongoing COVID-19 pandemic in mind, we developed an LTL knowledge base for a medical robot tasked with HRI-intensive roles of patient reception and triage. We designed robotic simulations based on our LTL architecture to test our approach, employing randomized inputs to generate unpredictable HRI environments. We then conducted formal verification via an automata-theoretic approach by evaluating our simulated robot against generalized Büchi automata. We hope our LTL-based approach can enable future achievements in HRI.