VE5: Formal verification and learning for robotics

Autonomous systems are systems functioning without external control. There are several fields in which autonomous systems play an increasing role like, e.g., aerospace, automotive engineering, and robotics. Both the outcome of autonomous actions as well as the behavior of the system’s environment are inherently random in nature, e.g., sensor imprecisions of a robot, message loss, or unpredictable behavior of the environment. Moreover, it might be the case that certain information—such as cost caused by energy consumption—is not exactly known prior to exploring and observation. The randomness and uncertainty, together with the high complexity of autonomous systems, makes the construction of efficient and safe autonomous systems highly challenging. Whereas formal methods are well established in several other areas for controller synthesis and analysis, their potential in the area of robotics is still rarely exploited. The aim of this dissertation project is to develop new approaches to enable the integration of different types of formal methods for probabilistic systems into the design process of autonomous robots, resulting in (1) improved functionality, (2) increased efficiency, and (3) guaranteed quality/safety.

Though there are successful symbolic reasoning methods to solve planning problems, most of them provide no quality guarantees. A promising but not yet exploited approach to obtain such guarantees is to employ SMT solvers. These powerful tools have been developed for checking the satisfiability of logical formulas that also contain sub-formulas over some theory, such as e.g., linear arithmetic over the real numbers. SMT techniques are frequently used in verification and have recently also been used for optimisation. Of particular interest to this project is the SMT solver SMT-RAT, developed in Ábrahám’s group, which focuses on real and integer arithmetic problems. The first objective of this dissertation project is to employ SMT techniques such as offered by SMT-RAT to the high-level planning for robots.

Model-free reinforcement learning for Markov decision processes (MDPs) is a popular approach for low-level controller synthesis. As the aforementioned symbolic methods, this approach is missing quality guarantees. Probabilistic model checking is an approach that can overcome this deficiency, but typically relies on an MDP in which all transition probabilities and costs (aka: rewards) are fixed. Model repair remedies this by allowing for adapting these attributes on the basis of system runs or counterexamples indicating that the system deviates from the indicated attribute values. The second objective of this dissertation project is to combine reinforcement learning with probabilistic model checking, model repair, and runtime monitoring (or counterexample generation) so as to synthesise safe low-level robot controllers in an automated manner. Initial work towards this direction has recently been published.

In addition to theoretical investigations, a prototypical implementation of the developed approaches is planned. Empirical evaluation is planned on case studies from the RoboCup Logistics League and some low-level movement tasks (e.g., the challenging standing-up task).

(This dissertation project is related to the project AP5.)