Abstraction Learning with Guarantees
Data-Driven Approaches to Symbolic Control and Verification
R. Coppola (TU Delft - Team Manuel Mazo Jr)
M. Mazo Espinosa – Promotor (TU Delft - Team Manuel Mazo Jr)
L. Laurenti – Copromotor (TU Delft - Team Luca Laurenti)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Modern engineering systems, ranging from autonomous vehicles to energy storage devices, are required to operate reliably under uncertainty while satisfying increasingly complex performance and safety requirements. Ensuring that such systems behave as intended is the domain of verification, while the even more ambitious goal of designing controllers that guarantee correct behaviour by construction is known as controller synthesis. Achieving these objectives is especially difficult when systems are nonlinear or only partially known.
A central paradigm to address this challenge is the use of symbolic abstractions: simplified models that preserve the essential behaviours of the underlying system while improving analytical tractability. Abstractions enable the use of automated methods for verification and controller synthesis, making it possible to reason about safety, reachability, or performance in a mathematically rigorous way. In particular, symbolic control leverages finite-state abstractions to enable automated algorithmic synthesis of controllers that come with formal correctness guarantees. Yet, traditional abstraction techniques require complete system knowledge, limiting their applicability in practical scenarios where model knowledge is scarce, while data is abundant.
This thesis investigates how to overcome this limitation by learning abstractions directly from data and learning abstractions in combination with data when partial knowledge of the dyamics is available; further, we demonstrate how such abstractions can be used for verification and control under uncertainty....