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

Maintaining stability in feedback systems, from aircraft and autonomous robots to biological and physiological systems, relies on monitoring their behavior and continuously adjusting their inputs. Incremental damage can make such control fragile. This tends to go unnoticed until a small perturbation induces instability (i.e., loss of control). Traditional methods in the field of engineering rely on accurate system models to compute a safe set of operating instructions, which become invalid when the, possibly damaged, system diverges from its model. Here we demonstrate that the approach of such a feedback system toward instability can nonetheless be monitored through dynamical indicators of resilience. This holistic system safety monitor does not rely on a system model and is based on the generic phenomenon of critical slowing down, shown to occur in the climate, biology, and other complex nonlinear systems approaching criticality. Our findings for engineered devices opens up a wide range of applications involving real-time early warning systems as well as an empirical guidance of resilient system design exploration, or “tinkering.” While we demonstrate the validity using drones, the generic nature of the underlying principles suggest that these indicators could apply across a wider class of controlled systems including reactors, aircraft, and self-driving cars. ... Read more

Recent approaches to leveraging deep learning for computing reachable sets of continuous-time dynamical systems have gained popularity over traditional level-set methods, as they overcome the curse of dimensionality. However, as with level-set methods, considerable care needs to be taken in limiting approximation errors, particularly since no guarantees are provided during training on the accuracy of the learned reachable set. To address this limitation, we introduce an ϵ-approximate Hamilton-Jacobi partial differential equation (HJ-PDE), which establishes a relationship between training loss and accuracy of the true reachable set. To formally certify this approximation, we leverage Satisfiability Modulo Theories (SMT) solvers to bound the residual error of the HJ-based loss function across the domain of interest. Leveraging Counter Example Guided Inductive Synthesis (CEGIS), we close the loop around learning and verification, by fine-tuning the neural network on counterexamples found by the SMT solver, thus improving the accuracy of the learned reachable set. To the best of our knowledge, Certified Approximate Reachability (CARe) is the first approach to provide soundness guarantees on learned reachable sets of continuous dynamical systems. ... Read more

This paper presents a reachability-guided controller for nonlinear systems that synthesizes pseudo-optimal control using only local linear models. At each step, a forward reachable tube (FRT) is computed via zonotope-based set propagation; the closest point in the FRT to the target is chosen as an intermediate waypoint, around which a backward reachable tube (BRT) is solved using Hamilton–Jacobi (HJ) reachability. The resulting value function yields a locally optimal control action. This process is repeated iteratively to steer the system toward the target without requiring global nonlinear dynamics. We evaluate the method on the double integrator, inverted pendulum, and Dubins car, benchmarking against model predictive control baselines. For the double integrator, we additionally benchmark against its ground-truth time-optimal bang-bang solution. Our proposed ZonoReach controller achieves successful setpoint tracking and near time-optimal performance. Results highlight the influence of planning and control horizons, while limitations include reliance on local linear approximations and grid-based solvers for BRT computation. We conclude with directions for improving scalability toward real-world systems. ... Read more

Ensuring safety in autonomous systems is essential as they become more integrated with modern society. One way to accomplish this is to identify and maintain a safe operating space. To this end, much effort has been devoted in the field of reachability analysis to obtaining control-invariant sets which ensure that a system inside of these sets can remain in these sets, and are thus essential for guaranteeing a system's safety. However, control invariance does not imply that a system can move from any state in the control-invariant set to any other state in the control-invariant set, within a given time horizon. In this paper, we develop an algorithm to obtain a control-invariant set that allows a given system to move from any state in the set to any other state in the set within a given time horizon without having to leave the set. We call this the 'maneuver set', M. We substantiate the algorithm's efficacy through mathematical proof, affirming that the maneuver set obtained through the algorithm is indeed control-invariant. Furthermore, we prove that the system is indeed able to move from any state within this set to any other state in the set. To illustrate the use of our algorithm, we provide the numerical example of a Dubins car, utilising Hamilton-Jacobi-Bellman reachability analysis along with the proposed algorithm in order to obtain M. ... Read more

Unmanned aerial vehicles (UAVs) are becoming an integral part of both industry and society. In particular, the quadrotor is now invaluable across a plethora of fields and recent developments, such as the inclusion of aerial manipulators, only extends their versatility. As UAVs become more widespread, preventing loss-of-control (LOC) is an ever growing concern. Unfortunately, LOC is not clearly defined for quadrotors, or indeed, many other autonomous systems. Moreover, any existing definitions are often incomplete and restrictive. A novel metric, based on actuator capabilities, is introduced to detect LOC in quadrotors. The potential of this metric for LOC detection is demonstrated through both simulated and real quadrotor flight data. It is able to detect LOC induced by actuator faults without explicit knowledge of the occurrence and nature of the failure. The proposed metric is also sensitive enough to detect LOC in more nuanced cases, where the quadrotor remains undamaged but nevertheless losses control through an aggressive yawing manoeuvre. As the metric depends only on system and actuator models, it is sufficiently general to be applied to other systems. ... Read more

Quadcopters are becoming increasingly popular across diverse sectors. Since rotor damages occur frequently, it is essential to improve the attitude estimation and thus ultimately the ability to control a damaged quadcopter. This research is based on a state-of-the-art method that makes it possible to control the quadcopter despite the total failure of a single rotor, where the attitude and position of the quadcopter are provided by an external system. In the present research, a novel attitude estimator called Adaptive Fuzzy Complementary Kalman Filter (AFCKF) has been developed and validated that works independently of any external systems. It is able to estimate the attitude of a quadcopter with one fully damaged rotor while only relying on the on-board MARG (Magnetometer, Accelerometer, Rate Gyroscope) sensors. The AFCKF provides significantly better attitude estimates for flights with a damaged rotor than mainstream filters, estimating the roll and pitch of the quadcopter with an RMS error of less than 1.7 degrees and a variance of less than 2 degrees. The proposed filter also provides accurate yaw estimates despite the fast spinning motion of the damaged quadcopter, and thus outperforms existing methods at the cost of only a small increase in computation. ... Read more