Safe operation region estimation and certification

This dissertation develops a unified framework for defining, computing, and certifying safe operating regions for autonomous dynamical systems operating under deterministic, robust, and stochastic dynamics. As these systems are increasingly deployed in safety-critical environments—ranging from autonomous vehicles and air traffic management to robotics and automated decision-making—ensuring that their behaviour remains within safe bounds is of vital importance. Classical reachability methods offer strong theoretical guarantees, but they often rely on idealised models, struggle with high-dimensional systems, and cannot formally certify learned approximations. This work addresses these limitations through new safety definitions, robust generalisations of reachability theory, and a learning-verification pipeline for scalable certification.

The first contribution focuses on the notion of safe sets themselves. \Cref{ch:maneuverable} introduces the concept of the maneuverable control-invariant set—a novel refinement of traditional invariant sets. Unlike classical safe sets, which guarantee that the system can remain within a given region, maneuverable sets also ensure the system's ability to move between any two states within the set in a given time horizon. Although such maneuverability and invariance cannot always be achieved simultaneously, this definition adds a valuable dimension to safety characterisation. The set is computed using a combination of forward and backward reachable sets derived from Hamilton-Jacobi (HJ) reachability analysis. Building on this, \Cref{ch:safeset} presents an improved definition of a safe set that does guarantee both viability and full internal maneuverability simultaneously. It is obtained through a different combination of forward and backward reachable sets. While the first two chapters establish refined definitions of safe sets under idealised dynamics, real-world systems rarely operate with perfect models. To address this, the next contribution turns to the challenge of ensuring safety under model uncertainty and disturbances.

\Cref{ch:RobustBRT} addresses robustness under model uncertainty. It extends the HJ reachability framework by formulating a three-player differential game that includes unmodelled dynamics as an additional adversary alongside external disturbances. The resulting Robust Avoid Backward Reachable Tube (RABRT) generalises previous formulations by ensuring safety in the presence of both disturbances and uncertain system dynamics. The associated value function is shown to be the viscosity solution to a well-defined Hamilton-Jacobi-Isaacs (HJI) partial differential equation (PDE), and the method integrates with existing level-set tools, preserving compatibility with standard computational frameworks. While this formulation provides robustness to unmodelled dynamics, its computational demands grow quickly with system dimensionality. As classical level-set methods struggle in high-dimensional settings, recent work has turned to neural network–based approximations. The next chapter explores how such approximations can be made verifiable and trustworthy through formal certification.

To overcome the curse of dimensionality inherent in classical reachability methods, \Cref{ch:Care} introduces the Certified Approximate Reachability (CARe) framework. Instead of solving PDEs directly on grids, CARe leverages neural networks to approximate the value function and then uses formal verification tools—specifically Satisfiability Modulo Theory (SMT) solvers and Counterexample-Guided Inductive Synthesis (CEGIS)—to certify the learned approximation within a bounded error. This framework bridges the gap between deep learning and formal safety verification, offering a scalable method for high-dimensional systems while preserving correctness guarantees. While CARe provides a scalable and certifiable solution for deterministic systems, many real-world applications involve stochastic dynamics and probabilistic safety requirements. To address this, the final part of the thesis extends the reachability framework to systems governed by uncertainty and noise.

Chapters \ref{ch:StochasticABRT} and \ref{ch:stochasticsafeBRT} extend the thesis into the stochastic domain. \Cref{ch:StochasticABRT} introduces the Probabilistic Forced Backward Reachable Set, which identifies states from which the system enters an undesirable set with high probability, regardless of the control policy. The chapter develops convergent algorithms for computing this set in both discrete and continuous settings and provides error bounds under discretisation. \Cref{ch:stochasticsafeBRT} then presents the Safe Probable Backward Reachable Set (SPBRS), which guarantees not only that the system will reach a target with a given probability but also that it will remain inside a certified safe set throughout the trajectory. This is especially important in stochastic systems where intermediate safety violations can occur despite a safe terminal state. Two algorithms are developed—one computationally efficient and the other optimal—and their convergence and tractability are formally analysed.

Each chapter is supported by theoretical proofs, algorithmic implementation, and numerical validation on benchmark systems such as the Dubins car and double integrator. This dissertation offers a cohesive and extensible framework for analysing and certifying safety in both deterministic and stochastic systems. By introducing new definitions of safety, developing scalable algorithms, and integrating formal verification with deep learning, the work makes contributions that are both foundational and practical. It addresses longstanding limitations in the scalability, conservatism, and verifiability of reachability-based safety analysis. The results have direct implications for real-world autonomous systems, including autonomous vehicles, robotics, air traffic management, and safety-critical embedded systems. More broadly, the methods contribute to the growing effort to make machine learning and autonomy formally trustworthy, especially in domains where safety cannot be left to statistical performance alone. Looking ahead, this work lays the groundwork for future research in adaptive safety verification, stochastic control synthesis, and trustworthy decision-making in uncertain environments—pushing the boundaries of what is possible at the intersection of formal methods, control theory, and autonomy.