Guarantees for Real Robotic Systems: Unifying Formal Controller Synthesis and Reachset-Conformant Identification
This addresses safety-critical scenarios like robotic surgery by providing verifiable guarantees, though it is incremental as it builds on existing formal methods.
The paper tackles the problem of ensuring safety guarantees for real robots by combining formal controller synthesis with reachset-conformant model identification, demonstrating transferability through experiments on a real robot with synthesized tracking controllers.
Robots are used increasingly often in safety-critical scenarios, such as robotic surgery or human-robot interaction. To ensure stringent performance criteria, formal controller synthesis is a promising direction to guarantee that robots behave as desired. However, formally ensured properties only transfer to the real robot when the model is appropriate. We address this problem by combining the identification of a reachset-conformant model with controller synthesis. Since the reachset-conformant model contains all the measured behaviors of the real robot, the safety properties of the model transfer to the real robot. The transferability is demonstrated by experiments on a real robot, for which we synthesize tracking controllers.