Verifying Safety Properties of Robotic Plans Operating in Real-World Environments via Logic-Based Environment Modeling

These days, robotic agents are finding their way into the personal environment of many people. With robotic vacuum cleaners commercially available already, comprehensive cognition-enabled agents assisting around the house autonomously are a highly relevant research topic. To execute these kinds of tasks in constantly changing environments, complex goal-driven control programs, so-called plans, are required. They incorporate perception, manipulation, and navigation capabilities among others. As with all technological innovation, consequently, safety and correctness concerns arise. In this paper, we present a methodology for the verification of safety properties of robotic plans in household environments by a combination of environment reasoning using Discrete Event Calculus (DEC) and Symbolic Execution for effectively handling symbolic input variables (e. g. object positions). We demonstrate the applicability of our approach in an experimental evaluation by verifying safety properties of robotic plans controlling a two-armed, human-sized household robot packing and unpacking a shelf. Our experiments demonstrate our approach’s capability to verify several robotic plans in a realistic, logically formalized environment.