In this paper, we address the runtime verification problem of robot motion planning with human-in-the-loop. By bringing together approaches from runtime verification, trust model, and symbolic motion planning, we developed a framework which guarantees that a robot is able to safely satisfy task specifications while improving task efficiency by switches between human supervision and autonomous motion planning. A simple robot model in a domain path planning scenario is considered and the robot is assumed to have perfect localization capabilities. The task domain is partitioned into a finite number of identical cells. A trust model based on the robot and human performance is used to provide a switching logic between different modes. Model checking techniques are utilized to generate plans in autonomous motion planning and for this purpose, Linear Temporal Logic (LTL) as a task specification language is employed to formally express specifications in model checking. The whole system is implemented in a runtime verification framework to monitor and verifies the system execution at runtime using ROSRV. Finally, we illustrated the effectiveness of this framework as well as its feasibility through a simulated case study.
Combining Model Checking and Runtime Verification for Safe Robotics
