Formal verification of maneuver automata for parameterized motion primitives

An increasing amount of robotic systems is developed for safety-critical scenarios, such as automated cars operating in public road traffic or robots collaborating with humans in flexible manufacturing systems. For this reason, it is important to provide methods that formally verify the safety of robotic systems. This is challenging since robots operate in continuous action spaces in partially unknown environments so that there exists no finite set of scenarios that can be verified before deployment. Verifying the safety during the operation based on the current perception of the environment is often infeasible due to the computational demand of formal verification methods. In this work, we compute sets of behaviors for parameterized motion primitives using reachability analysis, which is used to build a maneuver automaton that connects motion primitives in a safe way. Thus, the computationally expensive task of building a maneuver automaton is performed offline. The proposed analysis method provides the whole set of possible behaviors so that it can be verified whether forbidden state-space regions are avoided during the operation of the robot, to e.g. avoid colliding with obstacles. The method is applied to continuous sets of parameterized motion primitives, making it possible to verify infinitely many motions within the parameter space, which to the best knowledge of the authors has not been published before. The approach is demonstrated for collision avoidance of road vehicles.