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

Cyber-physical systems integrate digital control and physical processes and often operate in complex, uncertain environments. The consequence of operational failures in such systems can be catastrophic and may include loss of life, environmental damage, irreparable system damage, and economic disruption. Therefore, safety is a critical concern and traditional engineering approaches that only rely on extensive testing and conservative design margins are insufficient to guarantee safety in the face of uncertainty. The issue is that testing only assesses the performance on a limited number of scenarios or samples, while in practice the collection of possible scenarios is uncountable due to the physical process and uncertainties therein. Formal methods provide a powerful alternative, offering mathematically rigorous verification that accounts for all possible behaviours subject to ranges of disturbances and uncertainties. A key challenge in applying formal methods to stochastic dynamical systems is a fundamental tension between computational tractability and conservatism. Existing approaches either scale poorly with the system dimension and complexity or produce loose bounds on safety probabilities that limit their practical applicability. This creates a critical gap between theory and practice: while formal verification methods exist, their practical applicability to real-world systems remains severely limited. Therefore, the core research question driving this work is: How to efficiently compute tight bounds on the satisfaction probabilities for safety, reachability, and reach-avoid specifications of stochastic systems?

To answer this question and address the gap, the present dissertation develops several complementary approaches for efficiently verifying properties of stochastic systems. The focus is on discrete-time, continuous-space stochastic systems and simple specifications over given sets. The approaches represent points along the spectrum of the scalability-conservatism trade-off and rely on different system assumptions. The methods developed belong to two families: stochastic barrier functions and finite-state abstractions.

Stochastic barrier functions are Lyapunov-like functions that provide certificates of safety by imposing conditions on the expected value of the barrier function along system trajectories. The core idea is that if the composition of the barrier function with the dynamics of the system forms a c-martingale, then the probability of safety can be bounded using martingale inequalities. The main challenge is to construct a barrier that is optimal with respect to the martingale inequalities. Hand-crafting such functions is difficult and time-consuming, and existing synthesis methods are often limited to low-dimensional and simple systems for non-trivial results. To enable efficient synthesis of stochastic barrier functions, we develop multiple synthesis techniques, including a neural network-based method that offers flexibility but requires post hoc verification to confirm correctness. More significantly, we introduce piecewise-constant stochastic barrier function theory and synthesis methods that are guaranteed to asymptotically approach optimality. The synthesis methods include a dual linear programming formulation, a counterexample-guided inductive synthesis with linear programming solvers, and gradient descent optimization; their trade-off is between scalability and required parameter tuning. The theoretical analysis of piece-wise constant barriers reveals deep insights into the relationship between barrier functions and system dynamics, illuminates fundamental sources of conservatism inherent to the approach, and establishes clear connections to Interval Markov Decision Process (IMDP)-based finite-state abstractions. Additionally, we develop a data-driven scenario-theoretic approach for systems with partially unknown dynamics, leveraging scenario theory to handle uncertainty in system models.

Finite-state abstractions, on the other hand, reduce the original continuous-space system to a finite-state model that can be analysed using probabilistic model checking techniques. While abstraction-based methods are exceedingly flexible -- they have been successfully applied to a wide range of systems, including partially-unknown systems, and specifications -- they often suffer from high computational complexity of using probabilistic model checking and scalability issues due to the pervasive state-space explosion problem.  To address the first issue, we develop hardware-aware algorithmic innovations for faster model checking of IMDPs via dynamic programming. Dynamic programming over IMDPs relies for efficiency on an algorithm named O-maximization, or order-maximization, which by theoretical analysis is revealed to be composed of two phases: a sorting phase and a cumulative summation phase. We introduce parallel algorithms to both phases, which allows us to exploit modern highly parallel computing architectures to achieve significant speedups in verifying IMDPs. To address the second issue, we introduce a novel finite-state model called factored Interval Markov Decision Processes (fIMDPs) that exploits structural properties of the system dynamics to significantly reduce memory requirements while maintaining formal guarantees. Factored models encode data-dependencies more fine-grained than flat models, which is the key driver for the reduction in memory. Moreover, factored models have been successfully used in the context of abstraction to Markov Decision Processes (MDPs), but have not been applied until now to IMDPs. An insight of abstracting to factored models is that the structural exploitation inadvertently tightens the ambiguity sets that characterize IMDPs conservatism, thereby reducing the pessimism of the bounds.

The methods developed in this dissertation represent significant algorithmic and theoretical advances to address the scalability-conservatism trade-off and enable more efficient computation of tighter safety probability bounds, advancing formal verification of stochastic dynamical systems. By advancing stochastic barrier function synthesis and IMDP-based finite-state abstractions, this work pushes the frontier of formal verification for stochastic systems, providing new tools and insights to bridge the gap between theory and practice.  The findings suggest that future progress in scalable safety verification for stochastic systems depends critically on designing algorithms that respect and exploit inherent problem structure, offering a promising, albeit challenging path toward making formal methods practical for real-world stochastic cyber-physical systems. ... Read more

The evolution of communication and computing technologies of the recent decades has enabled the rapid development and scaling of networks of systems. Consequently, modern networks of systems present complexities and geographical extents for which traditional monitoring, planning, and control paradigms based on centralized, or even human-driven, operation are not sufficient anymore to guarantee efficient and safe operation. For such systems, more sophisticated control strategies are required for nominal functioning and further extension. While the availability of information, given by real-time communication, and the computing power, generally accessible for large applications, are no longer a fundamentally limiting factor in modern networks, the same cannot be stated for the control technologies behind their operation. The achievement of complete non-centralization of control decisions and actions, as well as the satisfaction of complex requirements for safe network operations, preservation, and restoration, are among the main drivers of the future development of networks. Pursuing the achievement of these advanced specifications, of profound societal relevance, and the necessity of improving performance and efficiency are at the basis of current research in the field of systems and control of networks. This thesis approaches some of these topics and consists of two main parts.... ... Read more

The formal verification of multi-agent systems in safety-critical domains is challenged by the need to certify population-level behaviours, such as formation control, under environmental uncertainty. Traditional state-based verification techniques are often inadequate for expressing these system-wide objectives and face scalability limitations. This thesis addresses this gap by developing a distributional reachability framework that models the evolution of the system directly over the space of probability distributions, using Interval Markov Decision Processes (IMDPs) to capture model uncertainty. We introduce two complementary analysis algorithms to compute guaranteed bounds on the set of all reachable distributions: a forward method using occupation measures and McCormick relaxations, and a robust backward algorithm based on value iteration over a discretised distribution space. Case studies in swarm deployment demonstrate the efficacy of the framework in computing robust, set-based approximations of reachable distributions. Furthermore, results for the robust backward reachability algorithm are presented for a running example. This capability allows for the formal verification of complex distributional specifications and the synthesis of control policies with certified safety guarantees, establishing a computational foundation for designing certifiably safe, large-scale autonomous systems.
... Read more

Gaussian Mixture Models (GMMs) are powerful tools for representing arbitrary distributions or data sets, especially in complex non-linear systems. They are often used as approximators due to their flexibility. However, in many cases, such as for dynamical systems, these must be propagated through non-linear functions. How we can do this is still an open problem.
In this work, we propose a scalable method for quantizing GMMs with formal bounds on the approximation error using the Wasserstein distance. This ensures the method is suitable for safety-critical applications such as autonomous vehicles and UAVs, where formal guarantees are essential. Our approach, called the multi-grids method, constructs local grids at locations of high density, which are identified using clustering techniques. Around each cluster, a hyperrectangular grid is formed, and the locations are placed ensuring minimal error in terms of the Wasserstein distance. This design allows the method to scale efficiently to GMMs of large sizes in terms of both the dimension and the number of components, a known limitation of existing methods.
We validate our method against the state of the art, across various settings, demonstrating significantly lower approximation errors in terms of the Wasserstein distance. Even at higher dimensions of 60 it can still find efficient quantizations with little computational costs. Additionally, we apply the multi-grids method to the uncertainty propagation problem in dynamical systems, including the benchmark Dubins Car, highlighting its practical effectiveness in real-time systems. ... Read more

The demand for autonomous systems in safety-critical domains has increased in recent years. As real-world systems grow in complexity, a key challenge is ensuring robust performance under uncertainty, which requires the synthesis of controllers that not only operate reliably in stochastic environments but also support post-hoc validation and certification of safety. To this end, Stochastic Model Predictive Control (SMPC) is a control framework suitable for systems subjected to stochastic disturbances and model uncertainties. However, its practical application is limited by the intractability of exact uncertainty propagation of the state distribution (i.e. the prediction step), particularly for nonlinear dynamics, incentivising research to focus on approximation methods such as linearisation or Monte Carlo sampling. In this literature, however, the approximations do not provide guarantees of correctness. This work addresses this particular limitation by leveraging quantisation-based uncertainty propagation, where both the state and disturbance distributions are discretised with formal guarantees in the Wasserstein distance. We formulate a quantised SMPC algorithm for discrete-time nonlinear systems with Gaussian additive noise, subject to individual chance constraints. For safety certification of the obtained controller, we introduce a validation scheme based on Wasserstein ambiguity sets that estimate worst-case constraint violation probabilities. The proposed approach is evaluated in simulation on benchmark tasks under both open and closed-loop policies. ... Read more

The use of machine learning (ML), especially neural networks, in modeling control systems has shown promise, particularly for systems with complex physics. However, applying these models in safety-critical areas requires reliable verification and control synthesis methods due to their inherent complexity. Formal methods, using stochastic finite state models like interval Markov decision processes (IMDPs), provide a way to analyze and verify these systems against detailed safety and performance specifications defined using linear temporal logic over finite traces (LTLf). Abstraction of ML models into such IMDPs, allows the deriving of formal guarantees on the IMDP that carryover to the underlying ML model.

This thesis focuses on designing a switched controller for a cart-pendulum system using neural network dynamic models (NNDM) by formal control synthesis, validating it through formal verification methods. The methodology includes modeling the system behavior under different controllers, abstracting these models into IMDPs, applying the respective formal methods, and validating the approach through experiments. The aim is to demonstrate the framework's utility in a practical context, comparing different neural network architectures and researching the applicability of formal guarantees to both the models and the actual system.

The main contributions are a practical application of the framework to a specific system, a comparison of neural network architectures for dynamic modeling, and an experiment-based validation of the framework's effectiveness. It confirms that the formal guarantees for abstracted models are relevant to the actual system, providing insights into the framework's potential for real-world applications. The findings suggest areas for further research, particularly in making such frameworks more accessible for practical deployment in safety-critical systems. ... Read more

Noise's impact on biochemical systems has long been a focal point of investigation, given its potential to compromise signal accuracy and disrupt system functionality. This paper conducts a comprehensive exploration into the noise characteristics within a set of signal differentiators recognized for their high precision. Noteworthy for their modularity, swift computation, and ease of implementation, these differentiators play a pivotal role in computing concentration changes and bear the potential to regulate the dynamics of biological systems.

This study establishes a comprehensive simulation framework to examine the noise characteristics of these differentiators across diverse input signal scenarios. Furthermore, we also apply noise suppression techniques such as noise filters to mitigate excessive noise and enhance noise performance.

Our findings reveal that these differentiators significantly amplify the system noise level, surpassing both the Poisson level and the original system noise level. Moreover, while noise filters demonstrate notable success in noise reduction, achieving Poisson-level noise without compromising signal integrity remains a challenge.

This investigation yields invaluable insights into the noise properties of biochemical differentiators, shedding light on their inherent limitations. Additionally, it presents a viable pathway to enhance noise behaviour, thereby extending the scope of applications for these differentiators. ... Read more

In the field of Systems and Control, optimal control problem-solving for complex systems is a core task. The development of accurate mathematical models to represent these systems’ dynamics is often difficult. This complexity comes from potential uncertainties, complex non-linearities, or unknown factors that might affect the system. Because of these challenges, there is a need for methods that can understand the dynamics using available data and control strategies that can work with such models without relying too much on expert knowledge or task-specific insights. These methods are essential for creating efficient and reliable solutions in a wide variety of applications within the discipline. The need for models that do not require expert knowledge has spurred the interest in applying machine learning methods to control problems. Probabilistic Inference for Learning COntrol (PILCO) is a model-based Reinforcement Learning (RL) algorithm known for its probabilistic approach to model-based RL. By employing Gaussian Process (GP) dynamics models, PILCO integrates uncertainties into its learning process, allowing it to derive control policies from limited data. PILCO’s use of the Squared Exponential (SE) kernel in its GP can restrict the learning capacity. Especially in higher-dimensional spaces, due to the SE kernel’s inherent smoothness assumption that might not capture complex or non-smooth dynamics effectively. The algorithm’s reliance on moment matching for approximating posterior distributions introduces another weakness, which can lead to inaccuracies in non-Gaussian or multi-modal contexts. These shortcomings may limit PILCO’s efficiency and scalability in more complex, higher-dimensional tasks or in situations where the underlying dynamics are not well-captured by the chosen kernel and approximation methods. This thesis introduces Deep Kernel PILCO (DKL PILCO), a novel framework that uses Deep Kernel Learning (DKL) for learning the dynamics, and the Unscented Transform (UT) to propagate the uncertainty. The effectiveness of this approach is demonstrated across various tasks, highlighting the potential of DKL and UT to enhance the scalability and efficiency of model-based RL methods such as PILCO, making it a promising candidate for real-world control applications. ... Read more

Many autonomous navigation tasks require mobile robots to operate in dynamic environments involving interactions between agents. Developing interaction-aware motion planning algorithms that enable safe and intelligent interactions remains challenging. Dynamic game theory renders a powerful mathematical framework to model these interactions rigorously as coupled optimization problems. By solving the resultant coupled optimization problems to equilibrium solutions, the game-theoretic models explicitly account for the interdependence of agents’ decisions and achieve simultaneous prediction and planning. Coupled constraints between players, such as collision avoidance, can also be handled explicitly. However, most existing game-theoretic motion planning approaches rely on known objective models of all agents. This assumption presents a key obstacle to real-world ego-centric planning applications of these methods, where only local information is available. This thesis investigates solution approaches to relax this assumption and explicitly account for the ego agent’s uncertainty about other agents’ objectives while adaptively conducting game-theoretic motion planning.

The main contribution of this work is an online adaptive model-predictive game-play (MPGP) framework that jointly infers other players’ objectives and computes corresponding generalized Nash equilibrium (GNE) strategies. These strategies are then used as predictions for other players and control strategies for the ego agent. The adaptivity of the proposed approach is enabled by differentiating through a trajectory game solver whose gradient signal is used for maximum likelihood estimation (MLE) of opponents’ objectives. Compared with existing objective inference solutions in dynamic games, the proposed approach handles general inequality constraints in games and further supports direct integration with other differentiable modules, such as neural networks (NNs). Two simulation experiments indicate that the proposed approach performs closely to solving games with known objectives and outperforms the game-theoretic and model-predictive control (MPC) baselines. Two hardware experiments further demonstrate the real-time planning capability of the planner and its real-world applicability.

In addition to this main contribution, the second contribution of this work is a variational autoencoder (VAE) pipeline built upon the proposed differentiable game solver. This contribution aims at going beyond the point estimation in the first contribution and inferring potentially multi-modal beliefs about players’ objectives based on observations. The main idea is to employ variational inference (VI) to approximate Bayesian inference of players’ objectives. The variational autoencoder (VAE) framework is utilized for amortization to avoid per-sample optimization. Initial results on a single-player example show that after training, the proposed pipeline can: (i) generate a game objective distribution that resembles the underlying training data distribution and (ii) accurately predict a narrow, uni-modal posterior objective distribution when the observation is unambiguous based on seen data in the past and (iii) generate a multi-modal belief distribution of player’s objective to capture mostly likely modes in case of high uncertainty. ... Read more

The rapid advancement in autonomous driving technology underscores the importance of studying the fragility of perception systems in autonomous vehicles, particularly due to their profound impact on public transportation safety. These systems are of paramount importance due to their direct impact on the lives of passengers and pedestrians. Additionally, their reliability can be easily compromised given the complexity and unpredictability of driving environments. However, current research and existing regulations often fail to adequately address the adversarial robustness of autonomous vehicle perception systems. This thesis delves into the adversarial robustness of camera-based perception systems of autonomous vehicles. Our research concentrates on developing and implementing evasion attacks that use black-box gradient estimation, as well as physical attacks in traffic sign detection and classification systems. Our findings indicate that even minor perturbations can impact the accuracy of these systems, leading to detection and classification errors. This finding highlights a critical vulnerability in the perception system's robustness against adversarial attacks. Moreover, the study extends to assess the transferability of adversarial examples across diverse perception models. Our results also expose significant gaps in the current regulatory frameworks of autonomous vehicles, necessitating the establishment of more rigorous and comprehensive safety standards. ... Read more

There is growing interest to control cyber-physical systems under complex specifications while retaining formal performance guarantees. In this thesis we present a framework for formal control of uncertain systems under complex specifications. We consider dynamical systems with random disturbances, whose probability distribution is unknown. When it comes to the specifications, we focus on those given as syntactically co-safe linear temporal logic (scLTL) formulas. Such formulas resemble natural language, and allow us to reason over complex behaviours of the system.

We follow an abstraction-based approach: we abstract the original system to a finite-state Markov model, in which the state discretization error as well as the distributional ambiguity, are embedded as uncertainties. To do so we make use of tools from optimal transport and ambiguity sets of probability distributions. After that, we synthesize a strategy for the abstraction and obtain probabilistic guarantees that the abstraction satisfies the specifications. Finally, we correctly refine the strategy to one that the original system can follow, and prove that the guarantees we obtained for the abstraction also hold for the original system.

We propose two approaches to obtain the abstraction. First, we propose a data-driven approach to abstract the system into an interval Markov decision process (IMDP) when samples from the unknown distribution is available. Then we use already existing algorithms to synthesize a strategy for the IMDP. Secondly, we propose an approach to abstract the original system into a robust Markov decision process (robust MDP). This second approach is applicable to more general uncertainty models besides the data-driven one, and reduces conservatism of the abstraction. Furthermore, we propose an algorithm to synthesize robust strategies for robust MDPs, which also renders the guarantees that the abstraction satisfies the specifications. Finally, we demonstrate the usefulness of our proposed approaches through several case studies that involve both linear and nonlinear systems. ... Read more