Formal Verification and Learning For Robotics
Autonomous systems are systems functioning without external control. There are several ﬁelds in which autonomous systems play an increasing role like, for example aerospace, automotive engineering, and robotics. Both the outcome of autonomous actions as well as the behaviour of the system’s environment are inherently random in nature, for example sensor imprecisions of a robot, message loss, or unpredictable behaviour 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 efﬁcient 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 efﬁciency, and 3. guaranteed quality and 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 satisﬁability of logical formulas that also contain sub-formulas over some theory, for example linear arithmetic over the real numbers. SMT techniques are frequently used in veriﬁcation and have recently also been used for optimization. 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 ﬁrst 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, as 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 deﬁciency, but typically relies on an MDP in which all transition probabilities and costs, also known as rewards, are ﬁxed. 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 run time monitoring or counter example generation so as to synthesize safe low-level robot controllers in an automated manner. Initial work towards this direction has recently been published in. 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 for example the challenging standing-up task.