Showing 1–6 of 6 results for author: Mathiesen, F B

Data-Driven Permissible Safe Control with Barrier Certificates

Authors: Rayan Mazouz, John Skovbekk, Frederik Baymler Mathiesen, Eric Frew, Luca Laurenti, Morteza Lahijanian

Abstract: 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… ▽ More 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 learning-enabled 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 the system grows the permissible strategy set. △ Less

Submitted 4 May, 2024; v1 submitted 30 April, 2024; originally announced May 2024.

IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes

Authors: Frederik Baymler Mathiesen, Morteza Lahijanian, Luca Laurenti

Abstract: 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 o… ▽ More 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. △ Less

Submitted 29 April, 2024; v1 submitted 8 January, 2024; originally announced January 2024.

Simultaneous Synthesis and Verification of Neural Control Barrier Functions through Branch-and-Bound Verification-in-the-loop Training

Authors: Xinyu Wang, Luzia Knoedler, Frederik Baymler Mathiesen, Javier Alonso-Mora

Abstract: Control Barrier Functions (CBFs) that provide formal safety guarantees have been widely used for safety-critical systems. However, it is non-trivial to design a CBF. Utilizing neural networks as CBFs has shown great success, but it necessitates their certification as CBFs. In this work, we leverage bound propagation techniques and the Branch-and-Bound scheme to efficiently verify that a neural net… ▽ More Control Barrier Functions (CBFs) that provide formal safety guarantees have been widely used for safety-critical systems. However, it is non-trivial to design a CBF. Utilizing neural networks as CBFs has shown great success, but it necessitates their certification as CBFs. In this work, we leverage bound propagation techniques and the Branch-and-Bound scheme to efficiently verify that a neural network satisfies the conditions to be a CBF over the continuous state space. To accelerate training, we further present a framework that embeds the verification scheme into the training loop to synthesize and verify a neural CBF simultaneously. In particular, we employ the verification scheme to identify partitions of the state space that are not guaranteed to satisfy the CBF conditions and expand the training dataset by incorporating additional data from these partitions. The neural network is then optimized using the augmented dataset to meet the CBF conditions. We show that for a non-linear control-affine system, our framework can efficiently certify a neural network as a CBF and render a larger safe set than state-of-the-art neural CBF works. We further employ our learned neural CBF to derive a safe controller to illustrate the practical use of our framework. △ Less

Submitted 17 November, 2023; originally announced November 2023.

Comments: 8 pages, 6 figures, under review for ECC 2024

Inner approximations of stochastic programs for data-driven stochastic barrier function design

Authors: Frederik Baymler Mathiesen, Licio Romao, Simeon C. Calvert, Alessandro Abate, Luca Laurenti

Abstract: 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… ▽ More 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. △ Less

Submitted 10 September, 2023; v1 submitted 10 April, 2023; originally announced April 2023.

Safety Certification for Stochastic Systems via Neural Barrier Functions

Authors: Frederik Baymler Mathiesen, Simeon Calvert, Luca Laurenti

Abstract: Providing non-trivial certificates of safety for non-linear stochastic systems is an important open problem that limits the wider adoption of autonomous systems in safety-critical applications. One promising solution to address this problem is barrier functions. The composition of a barrier function with a stochastic system forms a supermartingale, thus enabling the computation of the probability… ▽ More Providing non-trivial certificates of safety for non-linear stochastic systems is an important open problem that limits the wider adoption of autonomous systems in safety-critical applications. One promising solution to address this problem is barrier functions. The composition of a barrier function with a stochastic system forms a supermartingale, thus enabling the computation of the probability that the system stays in a safe set over a finite time horizon via martingale inequalities. However, existing approaches to find barrier functions for stochastic systems generally rely on convex optimization programs that restrict the search of a barrier to a small class of functions such as low degree SoS polynomials and can be computationally expensive. In this paper, we parameterize a barrier function as a neural network and show that techniques for robust training of neural networks can be successfully employed to find neural barrier functions. Specifically, we leverage bound propagation techniques to certify that a neural network satisfies the conditions to be a barrier function via linear programming and then employ the resulting bounds at training time to enforce the satisfaction of these conditions. We also present a branch-and-bound scheme that makes the certification framework scalable. We show that our approach outperforms existing methods in several case studies and often returns certificates of safety that are orders of magnitude larger. △ Less

Submitted 3 June, 2022; originally announced June 2022.

A Flow-Efficient and Legal-by-Construction Real-Time Traffic Signal Control Platform

Authors: Frederik Baymler Mathiesen, Garey Fleeman

Abstract: Inefficiencies in traffic flow through an intersection lead to stop** vehicles, unnecessary congestion, and increased accident risk. In this paper, we propose a traffic signal controller platform demonstrating the ability to increase traffic flow for arbitrary intersection topologies. This model uses Model Predictive Control on a Mixed Logical Dynamical system to control the state of independent… ▽ More Inefficiencies in traffic flow through an intersection lead to stop** vehicles, unnecessary congestion, and increased accident risk. In this paper, we propose a traffic signal controller platform demonstrating the ability to increase traffic flow for arbitrary intersection topologies. This model uses Model Predictive Control on a Mixed Logical Dynamical system to control the state of independently controlled traffic signals in a single intersection, removing constraints forcing the selection of signals from a set of phases. Further, we use constraints to impose a guarantee on the output of the system to be in the set of permissible actions under constraints including precise yellow timing, minimum inter-lane green transition timing, and selection of signal states with non-conflicting dependencies. We evaluate our model on a simulated 4-way intersection and an intersection in Denmark with true traffic data and a currently implemented timing schedule as a baseline. Our model shows at least 22\% reduction in time loss compared to baseline light schedules, and timing shows that this system can feasibly run online predictions at a frequency faster than 2s/prediction optimizing over a prediction horizon of 25s. △ Less

Submitted 1 November, 2020; originally announced November 2020.