Data-driven robust verification and control

Thesis

In recent years, the availability of data has exploded, leading to the so-called data era. This has led to a shift in the way we think about controlling systems, from time consuming model-based approaches, to data-driven techniques such as reinforcement learning, which can learn to control a system based only on data from that system. However, such techniques come at a cost, in particular, a lack of guarantees on system behaviour. In this thesis we explore how to make use of data to guarantee systems behave in a specified way, as well as how we can exploit data to control systems, whilst maintaining guarantees on future behaviour.

In order to verify and control our systems we require data from that system, obtaining this data may be, in general, difficult or expensive. As such, we seek to utilise all available data in order to optimise for a controller and provide guarantees, that is, we do not wish to withhold any data for testing. We therefore turn to the so-called scenario approach, which provides a framework for obtaining probably approximately correct bounds on the generalisability of a solution to a scenario program. In particular, given an optimisation program with data affecting the outcome, the scenario approach provides a guarantee on the probability of a newly sampled data point changing the result.

This thesis considers applying the scenario approach theory to increasingly complex control and verification problems. We begin by considering the synthesis of a controller for a class of finite-state models with uncertain probabilistic transitions between states. Then, we investigate a certificate synthesis problem for general continuous-state systems, introducing a novel algorithm with favourable properties for non-convex scenario programs. Finally, we turn to controller synthesis for continuous-state systems with uncertain state transitions.

Authors: Rickard, L

• DOI: 10.5287/ora-xoaezvmkv
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: formal verification; dynamical systems; data-driven techniques
• Subjects: Control theory