CoSy: Minimal Assume-Guarantee Co-Synthesis for Robotics

As autonomous robots move from encolosed environments to the real-world, the importance of making sure that they work as expected grows.

To that end, formal synthesis offers automated computation of correct-by-design plans or controls for an autonomous robot with respect to complex specifications.

While formal synthesis has been successfully applied in constrained settings in past years, its applicability in the real world has been limited due to high degrees of uncertainty in the environment and presence of people.In CoSy, we aim to develop theory to overcome this limitation by proposing minimal assume-guarantee co-synthesis, i.e. synthesis of rigorous guarantees alongside with minimal assumptions on the robot´s environment.

Furthermore, we aim to investigate how these assumption can be posed as advice to humans around a robot and to what extent the humans will comply.

With this, we target a significant gap in the state of the art -- the topic of rigorous guarantees in Human-Robot Interaction (HRI). CoSy will run over four years.

Two partially funded postdocs will tackle the theoretical aspects of the project together with the applicant (expert in formal synthesis for robotics).

We will explore automata-based approach as well as differential games to address co-synthesis for linear temporal logic (LTL) and signal temporal logic (STL).

The three researchers together with the co-applicant (expert in HRI) will also address applicability of the developed theory in HRI studies.