With the increasing ubiquity of safety-critical autonomous systems operating in uncertain environments, there is a need for mathematical methods for formal verification of stochastic models. Towards formally verifying properties of stochastic systems, methods based on discrete, finite Markov approximations - abstractions - thereof have surged in recent years. These are found in contexts where: either a) one only has partial, discrete observations of the underlying continuous stochastic process, or b) the original system is too complex to analyze, so one partitions the continuous state-space of the original system to construct a handleable, finite-state model thereof. In both cases, the abstraction is an approximation of the discrete stochastic process that arises precisely from the discretization of the underlying continuous process. The fact that the abstraction is Markov and the discrete process is not (even though the original one is) leads to approximation errors. Towards accounting for non-Markovianity, we introduce memory-dependent abstractions for stochastic systems, capturing dynamics with memory effects. Our contribution is twofold. First, we provide a formalism for memory-dependent abstractions based on transfer operators. Second, we quantify the approximation error by upper bounding the total variation distance between the true continuous state distribution and its discrete approximation.

Understanding atomic hydrogen (H) diffusion in multi-principal element alloys (MPEAs) is crucial for enhancing hydrogen transport and storage technologies. However, the vast compositional space and complex chemical environments of MPEAs pose significant challenges. We develop highly accurate machine learning force field and neural network-driven kinetic Monte Carlo simulations to investigate H diffusion in body-centered cubic (BCC) MoNbTaW MPEAs. H diffusion exhibits super-Arrhenius behavior in MPEAs, dominated by the low percentile of the H solution energy spectrum. Robust analytical models are derived via machine learning symbolic regression to predict H diffusivity across general BCC MPEAs. Additionally, it is revealed that chemical short-range order (SRO) generally does not impact H diffusion in MoNbTaW MPEAs, except it enhances diffusion when H-favoring elements are present in low concentrations. These insights not only deepen our understanding of H diffusion dynamics in MPEAs but also guide the strategic development of advanced MPEAs for hydrogen-related applications by manipulating element type, composition, and SRO.

Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties and black-box components that influence the system dynamics. In this work, we develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements against temporal logic specifications from an input-output dataset. The verification framework employs Gaussian process (GP) regression to learn the unknown dynamics from the dataset and abstracts the continuous-space system as a finite-state, uncertain Markov decision process (MDP). This abstraction relies on space discretization and transition probability intervals that capture the uncertainty due to the error in GP regression by using reproducible kernel Hilbert space analysis as well as the uncertainty induced by discretization. The framework utilizes existing model checking tools for verification of the uncertain MDP abstraction against a given temporal logic specification. We establish the correctness of extending the verification results on the abstraction created from noisy measurements to the underlying system. We show that the computational complexity of the framework is polynomial in the size of the dataset and discrete abstraction. The complexity analysis illustrates a trade-off between the quality of the verification results and the computational burden to handle larger datasets and finer abstractions. Finally, we demonstrate the efficacy of our learning and verification framework on several case studies with linear, nonlinear, and switched dynamical systems.

Uncertainty propagation in non-linear dynamical systems has become a key problem in various fields including control theory and machine learning. In this work, we focus on discrete-time non-linear stochastic dynamical systems. We present a novel approach to approximate the distribution of the system over a given finite time horizon with a mixture of distributions. The key novelty of our approach is that it not only provides tractable approximations for the distribution of a nonlinear stochastic system but also comes with formal guarantees of correctness. In particular, we consider the Total Variation (TV) distance to quantify the distance between two distributions and derive an upper bound on the TV between the distribution of the original system and the approximating mixture distribution derived from our framework. We show that in various cases of interest, including in the case of Gaussian noise, the resulting bound can be efficiently computed in closed form. This allows us to quantify the correctness of the approximation and to optimize the parameters of the resulting mixture distribution to minimize such distance. The effectiveness of our approach is illustrated on several benchmarks from the control community.

The European Economic Area Electricity Network Benchmark (EEA-ENB) is a multi-area power system representing the European network of transmission systems for electricity to facilitate the application of distributed control techniques. In the EEA-ENB, we consider the Load Frequency Control (LFC) problem in the presence of Renewable Energy Sources (RESs), and Energy Storage Systems (ESSs). RESs are known to cause instability in power networks due to their inertialess and intermittent characteristics, while ESSs are introduced as a resource to mitigate the problem. In the EEA-ENB, particular attention is dedicated to Distributed Model Predictive Control (DMPC), whose application is often limited to small and homogeneous test cases due to the lack of standardized large-scale scenarios for testing, and due to the large computation time required to obtain a centralized MPC action for performance comparison with DMPC strategies under consideration. The second problem is exacerbated when the scale of the system grows. To address these challenges and to provide a real-world-based and control-independent benchmark, the EEA-ENB has been developed. The benchmark includes a centralized MPC strategy providing performance and computation time metrics to compare distributed control within a repeatable and realistic simulation environment.

In this study, we explore the mechanisms underlying the exceptional intrinsic strength of face-centered cubic (FCC) Multi-Principal Element Alloys (MPEAs) using a multifaceted approach. Our methods integrate atomistic simulations, informed by both embedded-atom model and neural network potentials, with first-principles calculations, stochastic Peierls-Nabarro (PN) modeling, and symbolic machine learning. We identify a consistent, robust linear correlation between the strength of MPEAs and the standard deviation of the maximum stacking-fault restoring force (τ_max,sd) across various potentials. This finding is substantiated by comparing the experimental strengths of Cantor alloys’ subsystems and Ni_62.5V_37.5 against τ_max,sd values from high-throughput first-principle calculations. Our theoretical insights are derived from integrating the stochastic Peierls-Nabarro model with a shearable precipitation hardening framework, demonstrating that lattice distortion alone does not directly enhance intrinsic strength. Instead, τ_max,sd emerges as a critical determinant, capable of boosting the strength of MPEAs by up to tenfold. Our analysis reveals the critical role of the exponential form of the PN model in achieving substantial strength improvement by transforming the Gaussian-like distribution of τ_max into an exponential-like distribution of local Peierls stress. Additionally, using an advanced symbolic machine learning technique, the sure independence screening and sparsifying operator (SISSO) method, we derive interpretable relationships between MPEA strength, elastic properties, and τ_max statistics, offering new insights into the design and optimization of advanced MPEAs. These findings highlight that the nonlinear physics and atomic fluctuations characterizing MPEAs not only underpin their unconventional intrinsic strength but also contribute to other complex properties such as sluggish diffusion and cocktail effect.

Stochastic differential equations are commonly used to describe the evolution of stochastic processes. The state uncertainty of such processes is best represented by the probability density function (PDF), whose evolution is governed by the Fokker-Planck partial differential equation (FPPDE). However, it is generally infeasible to solve the FP-PDE in closed form. In this work, we show that physics-informed neural networks (PINNs) can be trained to approximate the solution PDF. Our main contribution is the analysis of PINN approximation error: we develop a theoretical framework to construct tight error bounds using PINNs. In addition, we derive a practical error bound that can be efficiently constructed with standard training methods. We discuss that this error-bound framework generalizes to approximate solutions of other linear PDEs. Empirical results on nonlinear, high-dimensional, and chaotic systems validate the correctness of our error bounds while demonstrating the scalability of PINNs and their significant computational speedup in obtaining accurate PDF solutions compared to the Monte Carlo approach.

This paper introduces a method of identifying a maximal set of safe strategies from data for stochastic systems with unknown dynamics using barrier certificates. The first step is learning the dynamics of the system via Gaussian Process (GP) regression and obtaining probabilistic errors for this estimate. Then, we develop an algorithm for constructing piecewise stochastic barrier functions to find a maximal permissible strategy set using the learned GP model, which is based on sequentially pruning the worst controls until a maximal set is identified. The permissible strategies are guaranteed to maintain probabilistic safety for the true system. This is especially important for learned systems, because a rich strategy space enables additional data collection and complex behaviors while remaining safe. Case studies on linear and nonlinear systems demonstrate that increasing the size of the dataset for learning grows the permissible strategy set.

The partitioning problem is a key problem for distributed control techniques. The problem consists in the definition of the subnetworks of a dynamical system that can be considered as individual control agents in the distributed control approach. Despite its relevance and the different approaches proposed in the literature, no generalized technique to perform the partitioning of a network of dynamical systems is present yet. In this article, we introduce a general approach to partitioning for distributed control. This approach is composed by an algorithmic part selecting elementary subnetworks, and by an integer program, which aggregates the elementary components according to a global index. We empirically evaluated our approach on a distributed predictive control problem in the context of power systems, obtaining promising performances in terms of reduction of computation speed and resource cost, while retaining a good level of performance.

We study the problem of certifying the robustness of Bayesian neural networks (BNNs) to adversarial input perturbations. Specifically, we define two notions of robustness for BNNs in an adversarial setting: probabilistic robustness and decision robustness. The former deals with the probabilistic behaviour of the network, that is, it ensures robustness across different stochastic realisations of the network, while the latter provides guarantees for the overall (output) decision of the BNN. Although these robustness properties cannot be computed analytically, we present a unified computational framework for efficiently and formally bounding them. Our approach is based on weight interval sampling, integration and bound propagation techniques, and can be applied to BNNs with a large number of parameters independently of the (approximate) inference method employed to train the BNN. We evaluate the effectiveness of our method on tasks including airborne collision avoidance, medical imaging and autonomous driving, demonstrating that it can compute non-trivial guarantees on medium size images (i.e., over 16 thousand input parameters).

Extended defects such as dislocation networks and general grain boundaries are ubiquitous in metals, and accurate modeling these extensive defects is crucial to elucidate their deformation mechanisms. However, existing machine learning interatomic potentials (MLIPs) often fall short in adequately describing these defects, as their large characteristic scales exceed the computational limits of first-principles calculations. To address this challenge, we present a computational framework combining a defect genome constructed via empirical interatomic potential-guided sampling, with an automated reconstruction technique that enables accurate first-principles modeling of general defects by converting atomic clusters into periodic configurations. The effectiveness of this approach was validated through simulations of nanoindentation, tensile deformation, and fracture in BCC tungsten. This framework enhances the modeling accuracy of extended defects in crystalline materials and provides a robust foundation for advancing MLIP development by leveraging defect genomes strategically.

Gaussian Process Regression (GPR) is a powerful and elegant method for learning complex functions from noisy data with a wide range of applications, including in safety-critical domains. Such applications have two key features: (i) they require rigorous error quantification, and (ii) the noise is often bounded and non-Gaussian due to, e.g., physical constraints. While error bounds for applying GPR in the presence of non-Gaussian noise exist, they tend to be overly restrictive and conservative in practice. In this paper, we provide novel error bounds for GPR under bounded support noise. Specifically, by relying on concentration inequalities and assuming that the latent function has low complexity in the reproducing kernel Hilbert space (RKHS) corresponding to the GP kernel, we derive both probabilistic and deterministic bounds on the error of the GPR. We show that these errors are substantially tighter than existing state-of-the-art bounds and are particularly well-suited for GPR with neural network kernels, i.e., Deep Kernel Learning (DKL). Furthermore, motivated by applications in safety-critical domains, we illustrate how these bounds can be combined with stochastic barrier functions to successfully quantify the safety probability of an unknown dynamical system from finite data. We validate the efficacy of our approach through several benchmarks and comparisons against existing bounds. The results show that our bounds are consistently smaller, and that DKLs can produce error bounds tighter than sample noise, significantly improving the safety probability of control systems.

Vulnerability to adversarial attacks is one of the principal hurdles to the adoption of deep learning in safety-critical applications. Despite significant efforts, both practical and theoretical, training deep learning models robust to adversarial attacks is still an open problem. In this article, we analyse the geometry of adversarial attacks in the over-parameterized limit for Bayesian neural networks (BNNs). We show that, in the limit, vulnerability to gradient-based attacks arises as a result of degeneracy in the data distribution, i.e., when the data lie on a lower dimensional submanifold of the ambient space. As a direct consequence, we demonstrate that in this limit, BNN posteriors are robust to gradient-based adversarial attacks. Crucially, by relying on the convergence of infinitely-wide BNNs to Gaussian processes (GPs), we prove that, under certain relatively mild assumptions, the expected gradient of the loss with respect to the BNN posterior distribution is vanishing, even when each NN sampled from the BNN posterior does not have vanishing gradients. The experimental results on the MNIST, Fashion MNIST, and a synthetic dataset with BNNs trained with Hamiltonian Monte Carlo and variational inference support this line of arguments, empirically showing that BNNs can display both high accuracy on clean data and robustness to both gradient-based and gradient-free adversarial attacks.

This paper introduces a novel abstraction-based framework for controller synthesis of nonlinear discrete-time stochastic systems. The focus is on probabilistic reach-avoid specifications. The framework is based on abstracting a stochastic system into a new class of robust Markov models, called orthogonally decoupled Interval Markov Decision Processes (odIMDPs). Specifically, an odIMDPs is a class of robust Markov processes, where the transition probabilities between each pair of states are uncertain and have the product form. We show that such a specific form in the transition probabilities allows one to build compositional abstractions of stochastic systems that, for each state, are only required to store the marginal probability bounds of the original system. This leads to improved memory complexity for our approach compared to commonly employed abstraction-based approaches. Furthermore, we show that an optimal control strategy for a odIMDPs can be computed by solving a set of linear problems. When the resulting strategy is mapped back to the original system, it is guaranteed to lead to reduced conservatism compared to existing approaches. To test our theoretical framework, we perform an extensive empirical comparison of our methods against Interval Markov Decision Process- and Markov Decision Process-based approaches on various benchmarks including 7D systems. Our empirical analysis shows that our approach substantially outperforms state-of-the-art approaches in terms of both memory requirements and the conservatism of the results.

We introduce a framework for the control of discrete-time switched stochastic systems with uncertain distributions. In particular, we consider stochastic dynamics with additive noise whose distribution lies in an ambiguity set of distributions that are ɛ−close, in the Wasserstein distance sense, to a nominal one. We propose algorithms for the efficient synthesis of distributionally robust control strategies that maximize the satisfaction probability of reach-avoid specifications with either a given or an arbitrary (not specified) time horizon, i.e., unbounded-time reachability. The framework consists of two main steps: finite abstraction and control synthesis. First, we construct a finite abstraction of the switched stochastic system as a robust Markov decision process (robust MDP) that encompasses both the stochasticity of the system and the uncertainty in the noise distribution. Then, we synthesize a strategy that is robust to the distributional uncertainty on the resulting robust MDP. We employ techniques from optimal transport and stochastic programming to reduce the strategy synthesis problem to a set of linear programs, and propose a tailored and efficient algorithm to solve them. The resulting strategies are correctly refined into switching strategies for the original stochastic system. We illustrate the efficacy of our framework on various case studies comprising both linear and non-linear switched stochastic systems.

Model-based reinforcement learning seeks to simultaneously learn the dynamics of an unknown stochastic environment and synthesise an optimal policy for acting in it. Ensuring the safety and robustness of sequential decisions made through a policy in such an environment is a key challenge for policies intended for safety-critical scenarios. In this work, we investigate two complementary problems: first, computing reach-avoid probabilities for iterative predictions made with dynamical models, with dynamics described by Bayesian neural network (BNN); second, synthesising control policies that are optimal with respect to a given reach-avoid specification (reaching a “target” state, while avoiding a set of “unsafe” states) and a learned BNN model. Our solution leverages interval propagation and backward recursion techniques to compute lower bounds for the probability that a policy's sequence of actions leads to satisfying the reach-avoid specification. Such computed lower bounds provide safety certification for the given policy and BNN model. We then introduce control synthesis algorithms to derive policies maximizing said lower bounds on the safety probability. We demonstrate the effectiveness of our method on a series of control benchmarks characterized by learned BNN dynamics models. On our most challenging benchmark, compared to purely data-driven policies the optimal synthesis algorithm is able to provide more than a four-fold increase in the number of certifiable states and more than a three-fold increase in the average guaranteed reach-avoid probability.

In this paper, we present IntervalMDP.jl, a Julia package for probabilistic analysis of interval Markov Decision Processes (IMDPs). IntervalMDP.jl facilitates the synthesis of optimal strategies and verification of IMDPs against reachability specifications and discounted reward properties. The library supports sparse matrices and is compatible with data formats from common tools for the analysis of probabilistic models, such as PRISM. A key feature of IntervalMDP.jl is that it presents both a multi-threaded CPU and a GPU-accelerated implementation of value iteration algorithms for IMDPs. In particular, IntervalMDP.jl takes advantage of the Julia type system and the inherently parallelizable nature of value iteration to improve the efficiency of performing analysis of IMDPs. On a set of examples, we show that IntervalMDP.jl substantially outperforms existing tools for verification and strategy synthesis for IMDPs in both computation time and memory consumption.

Analyzing event-triggered control's (ETC) sampling behavior is of paramount importance, as it enables formal assessment of its sampling performance and prediction of its sampling patterns. In this work, we formally analyze the sampling behavior of stochastic linear periodic ETC (PETC) systems by computing bounds on associated metrics. Specifically, we consider functions over sequences of state measurements and intersampling times that can be expressed as average, multiplicative or cumulative rewards, and introduce their expectations as metrics on PETC's sampling behavior. We compute bounds on these expectations, by constructing Interval Markov Chains equipped with suitable reward functions, that abstract stochastic PETC's sampling behavior. Our results are illustrated on a numerical example, for which we compute bounds on the expected average intersampling time and on the probability of triggering with the maximum possible intersampling time in a finite horizon.

Accurate fatigue assessment of material plagued by defects is of utmost importance to guarantee safety and service continuity in engineering components. This study shows how state-of-the-art semi-empirical models can be endowed with additional defect descriptors to probabilistically predict the occurrence of fatigue failures by exploiting advanced Bayesian Physics-guided Neural Network (B-PGNN) approaches. A B-PGNN is thereby developed to predict the fatigue failure probability of a sample containing defects, referred to a given fatigue endurance limit. In this framework, a robustly calibrated El Haddad's curve is exploited as the prior physics reinforcement of the probabilistic model, i.e., prior knowledge. Following, a likelihood function is built and the B-PGNN is trained via Bayesian Inference, thus calculating the posterior of the parameters. The arbitrariness of the choice of the related architecture is circumvented through a Bayesian model selection strategy. A case-study is analysed to prove the robustness of the proposed approach. This methodology proposes an advanced practical approach to help support the probabilistic design against fatigue failure.

This paper proposes a new framework to compute finite-horizon safety guarantees for discrete-time piece-wise affine systems with stochastic noise of unknown distributions. The approach is based on a novel approach to synthesise a stochastic barrier function (SBF) from noisy data and rely on the scenario optimization theory. In particular, we show that the stochastic program to synthesize a SBF can be relaxed into a chance-constrained optimisation problem on which scenario approach theory applies. We further show that the resulting program can be reduced to a linear programming problem, thus guaranteeing efficiency. In contrast to existing approaches, this method is data efficient as it only requires the number of data to be proportional to the logarithm in the negative inverse of the confidence level and is computationally efficient due to its reduction to linear programming. The efficacy of the method is empirically evaluated on various verification benchmarks. Experiments show a significant improvement with respect to state-of-the-art, obtaining tighter certificates with a confidence that is several orders of magnitude higher.