The development of correct-by-construction robot control software is difficult. To capture the interaction between the humans involved as operators, interactors,
or even as mere obstacles to the robot in a setting, the scenario has to be modeled precisely before verification activities can be performed. While modeling
this interaction is a problem in itself, the implementation is not easier. As a consequence, developing robot control software is time-consuming and specifications
are hard to get right.
To provide relief to the system engineer, we can synthesize robot controllers automatically from a specification. This not only saves her/him the time to actually implement a robot controller, but also serves as a means of debugging the specification -- if an important property of the controller to construct is forgotten, then this typically becomes obvious from the observed robot behavior. This is in contrast to manually constructed controllers, where forgotten cases are typically hidden deeply. Also, the application of synthesis technology allows to rapidly change specifications and implementations at the same time. In this manner, different interaction schemes between the robot and a human can be tried out in the field with little hassle.
Synthesis of reactive systems is computationally expensive in theory, which lead to the belief that the widespread application of this idea is infeasible. Yet, researchers have shown in various contexts that the concept is well-applicable in practice. While this seems to be a contradiction at first, it is in fact not. By choosing both the specification language and the optimization criterion carefully, we can combine efficiency of the synthesis process and a high quality of the obtained implementation at the same time. In this manner, synthesis is clearly superior to the manual construction of robot controllers, as then the optimality of the controller with respect to the optimization criterion is guaranteed along with its correctness. As an example, it was recently shown by Jing, Ehlers, and Kress-Gazit that in the scope of robotics, the synthesis problem actually becomes easier when exchanging the optimization criteria that are commonly used in the formal methods domain by one that is based on reaching the next robot goal with the least possible cost, which is more suitable for robotics anyway.
The driving question of this research agenda is: How can we adapt the basic idea of synthesis to allow the efficient engineering of robot control software of high quality for complex tasks, but still with little effort?
The key to achieving this goal is to carefully balance and refine the specification classes and quality criteria needed in the practice of robotics and the complexity and algorithmic properties of the resulting synthesis problems, which we study in this project.
This project is supported by the Institutional Strategy of the University of Bremen, Funded by the German Excellence Initiative.