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.

翻译：机器人越来越多地被用于安全关键场景中，例如机器人手术或人机交互。为确保严格的性能标准，形式化控制器合成是一条有前景的途径，可保障机器人按预期行为运行。然而，只有当模型适当时，形式化保证的特性才能传递到真实机器人。我们通过将可达集一致性模型的辨识与控制器合成相结合来解决这一问题。由于可达集一致性模型包含了真实机器人的所有实测行为，因此该模型的安全特性可传递至真实机器人。通过在真实机器人上进行的实验（我们为其合成了跟踪控制器）验证了这种可传递性。