Reliable Controller Synthesis: Guarantees for Safety-Critical System Testing and Verification

Citation

Akella, Prithvi (2023) Reliable Controller Synthesis: Guarantees for Safety-Critical System Testing and Verification. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/jej3-4444. https://resolver.caltech.edu/CaltechTHESIS:06122023-162907795

Abstract

The well-known quote by George Box states that "All models are wrong, but some are useful", and the controls and robotics communities alike have followed a similar paradigm to make significant theoretical and practical advances in the study of controllable systems to date. However, recent robotic system requirements include formal considerations for system safety, especially as we engineer systems that are required to work alongside us in our daily lives. As such, current research directions require analyses that consider these inaccurate system models, our inaccurate understanding of the environments in which these systems operate, and their combined effects on safe, effective system operation, e.g. the canonical autonomous driving problem in exceedingly difficult-to-model urban environments. Recently, this has led to burgeoning efforts in a formal study of controller verification. Specifically, verification denotes the process of determining whether a controller steers its system to exhibit desired behaviors despite the variety of environments the system might face during operation, e.g. whether the autonomous car's controller successfully drives the car to a destination without crashing into obstacles or pedestrians along the way. However, formalization of such a verification pipeline has proved difficult to date, especially since both the models we use for controller synthesis and our understanding of system environments are typically inaccurate.

As a result, this thesis describes our efforts in the development of a formal verification pipeline that addresses a few key challenges in traditional approaches to safety-critical system verification. The first contribution centers on difficult, reactive test synthesis. By test synthesis, we mean the construction of a (potentially difficult) environment in which we require the system under test to perform its objective, e.g. placement of parked cars around which an autonomous vehicle must park. Typically phrased as an optimization problem over the space of allowable environments, these tests are "static" insofar as they do not react to the system's choices made during the test. We posit that such reactivity could more accurately identify worst-case system behavior. As a result, we phrase reactive, maximally difficult test synthesis as a game-theoretic optimization problem, leveraging the same control theoretic tools that facilitate safety-critical controller synthesis - control barrier functions and signal temporal logic. We prove that our proposed synthesis technique is always solvable and always produces a realizable test environment. Finally, we showcase our results by synthesizing reactive tests for both single and multi-agent systems.

The second set of contributions centers on our efforts in uncertainty quantification. Due to un-modeled system and environmental aspects affecting system evolution in unpredictable ways, real-life systems need not realize the same paths every time. As such, typical analyses phrase verification as an optimization problem minimizing the expected value of a function over system trajectories with the expectation taken over this path variability, the distribution for which is assumed to be known. However, we posit that such an analysis should be risk-aware, i.e. account for this variability in a more principled fashion than an expectation-specific analysis, and should not assume apriori knowledge of the distribution corresponding to path variability, as it will be unknown in practice. To that end, we develop methods to bound a subset of risk measures for random variables whose distributions are unknown. This subset includes both Value-at-Risk and other, coherent risk measures heavily utilized in the controls and robotics communities. Simultaneously, we note that the same procedure can be applied to a wide class of non-convex optimization problems. In doing so, we develop a percentile-based optimization approach that rapidly identifies percentile solutions to optimization problems, i.e. a 90-th percentile solution is as good as 90% of solutions in the considered decision space.

The third set of contributions focuses on the application of the prior mathematical developments to facilitate both risk-aware safety-critical system verification and controller synthesis. We phrase risk-aware controller verification as a risk-measure identification problem and utilize the prior bounding results to provide an efficient, dimensionally-independent verification procedure. Then, we phrase risk-aware controller synthesis as an optimization problem maximizing the bound provided by our risk-aware verification method, and show that this problem is solvable by the percentile optimization methods mentioned prior. Finally, we lay the foundation for the utilization of the aforementioned mathematical developments in other aspects of controls and robotics and communities more broadly. We show how risk-measure bounding can augment models both offline and online to robustify safety-critical controllers, how percentile optimization can facilitate "optimal" input selection and guarantee generation for non-convex finite-time optimal controllers, and how multiple applications of the percentile approach can also bound the optimality gap of reported percentile solutions. We showcase all these results on hardware for multiple systems and highlight the data efficiency of our proposed approaches.

Thesis Files