We present StochasticBarrier.jl, an open-source Julia-based toolbox for generating Stochastic Barrier Functions (SBFs) for safety verification of discrete-time stochastic systems with additive Gaussian noise. StochasticBarrier.jl certifies linear, polynomial, and piecewise affine (PWA) systems. The latter enables verification for a wide range of system dynamics, including general nonlinear types. The toolbox implements a Sum-of-Squares (SOS) optimization approach, as well as methods based on piecewise constant (PWC) functions. For SOS-based SBFs, StochasticBarrier.jl leverages semi-definite programming solvers, while for PWC SBFs, it offers three engines: two using linear programming (LP) and one based on gradient descent (GD). Benchmarking StochasticBarrier.jl against the state-of-the-art shows that the tool outperforms existing tools in computation time, safety probability bounds, and scalability across over 30 case studies. Compared to its closest competitor, StochasticBarrier.jl is up to four orders of magnitude faster, achieves significant safety probability improvements, and supports higher-dimensional systems.

In this paper, we present a novel data-driven approach to quantify safety for non-linear, discrete-time stochastic systems with unknown noise distribution. We define safety as the probability that the system remains in a given region of the state space for a given time horizon and, to quantify it, we present an approach based on Stochastic Barrier Functions (SBFs). In particular, we introduce an inner approximation of the stochastic program to design an SBF in terms of a chance-constrained optimisation problem, which allows us to leverage the scenario approach theory to design an SBF from samples of the system with Probably Approximately Correct (PAC) guarantees. Our approach leads to tractable, robust linear programs, which enable us to assert safety for nonlinear models with a confidence that was otherwise deemed infeasible with existing methods. To further mitigate the computational complexity of our approach, we exploit the structure of the system dynamics and rely on spatial data structures to accelerate the construction and solution of the underlying optimisation problem. We show the efficacy and validity of our framework in several benchmarks, showing that our approach can obtain tighter certificates compared to state-of-the-art with a confidence that is several orders of magnitude higher.

The partitioning problem is of central relevance for designing and implementing non-centralized Model Predictive Control (MPC) strategies for large-scale systems. These control approaches include decentralized MPC, distributed MPC, hierarchical MPC, and coalitional MPC. Partitioning a system for the application of non-centralized MPC consists of finding the best definition of the subsystems, and their allocation into groups for the definition of local controllers, to maximize the relevant performance indicators. The present survey proposes a novel systematization of the partitioning approaches in the literature in five main classes: optimization-based, algorithmic, community-detection-based, game-theoretic-oriented, and heuristic approaches. A unified graph-theoretical formalism, a mathematical re-formulation of the problem in terms of mixed-integer programming, the novel concepts of predictive partitioning and multi-topological representations, and a methodological formulation of quality metrics are developed to support the classification and further developments of the field. We analyze the different classes of partitioning techniques, and we present an overview of their strengths and limitations, which include a technical discussion about the different approaches. Representative case studies are discussed to illustrate the application of partitioning techniques for non-centralized MPC in various sectors, including power systems, water networks, wind farms, chemical processes, transportation systems, communication networks, industrial automation, smart buildings, and cyber–physical systems. An outlook of future challenges completes the survey.

Neural networks hold great potential to act as approximate models of nonlinear dynamical systems, with the resulting neural approximations enabling verification and control of such systems. However, in safety-critical contexts, the use of neural approximations requires formal bounds on their closeness to the underlying system. To address this fundamental challenge, we propose a novel, adaptive, and parallelizable verification method based on certified first-order models. Our approach provides formal error bounds on the neural approximations of dynamical systems, allowing them to be safely employed as surrogates by interpreting the error bound as bounded disturbances acting on the approximated dynamics. We demonstrate the effectiveness and scalability of our method on a range of established benchmarks from the literature, showing that it significantly outperforms the state of the art. Furthermore, we show that our framework can successfully address additional scenarios previously intractable for existing methods – neural network compression and an autoencoder-based deep learning architecture for training Koopman operators for the purpose of trajectory prediction.

Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems. Recently, CBFs represented as neural networks have shown great promise due to their expressiveness and applicability to a broad class of dynamics and safety constraints. However, verifying that a trained neural network is indeed a valid CBF is a computational bottleneck that limits the size of the networks that can be used. To overcome this limitation, we present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF. Our approach is rooted in linear bound propagation (LBP) for neural networks, which we extend to compute bounds on the gradients of the network. Combined with McCormick relaxation, we derive linear upper and lower bounds on the CBF conditions, thereby eliminating the need for computationally expensive verification procedures. Our approach applies to arbitrary control-affine systems and a broad range of nonlinear activation functions. To reduce conservatism, we develop a parallelizable refinement strategy that adaptively refines the regions over which these bounds are computed. Our approach scales to larger neural networks than state-of-the-art verification procedures for CBFs, as demonstrated by our numerical experiments.

Providing safety guarantees for stochastic dynamical systems is a central problem in various fields, including control theory, machine learning, and robotics. Existing methods either employ stochastic barrier functions (SBFs) or rely on numerical approaches based on finite abstractions. SBFs, analogous to Lyapunov functions, are used to establish (probabilistic) set invariance, whereas abstraction-based approaches approximate the stochastic system with a finite model to compute safety probability bounds. This article presents a unifying perspective on these seemingly different approaches. Specifically, we show that both methods can be interpreted as approximations of a stochastic dynamic programming problem. This perspective allows us to formally establish the correctness of both techniques, characterize their convergence and optimality properties, and analyze their respective assumptions, advantages, and limitations. Our analysis reveals that, unlike SBFs-based methods, abstraction-based approaches can provide asymptotically optimal safety certificates, albeit at the cost of increased computational effort.

Stochastic barrier functions (SBFs) are Lyapunov-like functions that enable safety analysis of stochastic systems. Finding a valid SBF, however, is challenging, as it requires solving a complex functional optimization problem. Existing convex approaches are often limited to low-dimensional systems with simple (polynomial) dynamics, while non-convex approaches lack completeness guarantees. To address these challenges, this paper presents a novel SBF synthesis framework based on piecewise (PW) functions We first outline a general formulation of PW-SBFs. Then, we focus on PW-Constant (PWC) SBFs and show how their simplicity yields computational advantages for general stochastic systems. Specifically, we prove that synthesis of PWC-SBFs reduces to a minimax optimization problem. We then introduce three efficient algorithms to solve this problem, each offering distinct trade-offs, all with completeness guarantees. The first algorithm is based on dual linear programming (LP), which provides an exact solution to the minimax optimization problem. The second is a more scalable algorithm based on counter-example guided inductive synthesis, which involves solving two smaller LPs. The third algorithm solves the minimax problem using gradient descent, which admits even better scalability. We provide an extensive evaluation of these methods on various case studies, including neural network dynamic models, nonlinear switched systems, and high-dimensional linear systems. Our benchmarks demonstrate that PWC-SBFs outperform state-of-the-art methods, namely sum-of-squares and neural barrier functions, and can scale to eight dimensional systems.

Infinitely wide or deep neural networks (NNs) with independent and identically distributed (i.i.d.) parameters have been shown to be equivalent to Gaussian processes. Because of the favorable properties of Gaussian processes, this equivalence is commonly employed to analyze neural networks and has led to various breakthroughs over the years. However, neural networks and Gaussian processes are equivalent only in the limit; in the finite case there are currently no methods available to approximate a trained neural network with a Gaussian model with bounds on the approximation error. In this work, we present an algorithmic framework to approximate a neural network of finite width and depth, and with not necessarily i.i.d. parameters, with a mixture of Gaussian processes with bounds on the approximation error. In particular, we consider the Wasserstein distance to quantify the closeness between probabilistic models and, by relying on tools from optimal transport and Gaussian processes, we iteratively approximate the output distribution of each layer of the neural network as a mixture of Gaussian processes. Crucially, for any NN and ∊ > 0 our approach is able to return a mixture of Gaussian processes that is ∊-close to the NN at a finite set of input points. Furthermore, we rely on the differentiability of the resulting error bound to show how our approach can be employed to tune the parameters of a NN to mimic the functional behavior of a given Gaussian process, e.g., for prior selection in the context of Bayesian inference. We empirically investigate the effectiveness of our results on both regression and classification problems with various neural network architectures. Our experiments highlight how our results can represent an important step towards understanding neural network predictions and formally quantifying their uncertainty.

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.

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.

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.

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.