Abstraction Learning with Guarantees: Data-Driven Approaches to Symbolic Control and Verification

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....