5 citations · 12 across the 9 of their papers we have counts for
11 papers
LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
Zhipeng Cao, Peiyang Song, Nikolaus Vertovec +6
Lyapunov functions and barrier certificates give state-space guarantees of stability and safety, but synthesizing and verifying them---especially for nonlinear, high-dimensional sy…
Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation
Nikolaus Vertovec, Frederik Baymler Mathiesen, Thom Badings +2
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…
Certified Neural Approximations of Nonlinear Dynamics
Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano +2
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…
SPoRt -- Safe Policy Ratio: Certified Training and Deployment of Task Policies in Model-Free RL
Jacques Cloete, Nikolaus Vertovec, Alessandro Abate
To apply reinforcement learning to safety-critical applications, we ought to provide safety guarantees during both policy training and deployment. In this work, we present theoreti…
Certified Approximate Reachability (CARe): Formal Error Bounds on Deep Learning of Reachable Sets
Prashant Solanki, Nikolaus Vertovec, Yannik Schnitzer +3
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 o…
Finite sample learning of moving targets
Nikolaus Vertovec, Kostas Margellos, Maria Prandini
We consider a moving target that we seek to learn from samples. Our results extend randomized techniques developed in control and optimization for a constant target to the case whe…
State Aggregation for Distributed Value Iteration in Dynamic Programming
Nikolaus Vertovec, Kostas Margellos
We propose a distributed algorithm to solve a dynamic programming problem with multiple agents, where each agent has only partial knowledge of the state transition probabilities an…
Multi-objective low-thrust spacecraft trajectory design using reachability analysis
Nikolaus Vertovec, Sina Ober-Blöbaum, Kostas Margellos
One of the fundamental problems in spacecraft trajectory design is finding the optimal transfer trajectory that minimizes the propellant consumption and transfer time simultaneousl…
Safety-Aware Hybrid Control of Airborne Wind Energy Systems
Nikolaus Vertovec, Sina Ober-Blöbaum, Kostas Margellos
A fundamental concern in progressing Airborne Wind Energy (AWE) operations towards commercial success, is guaranteeing that safety requirements placed on the systems are met. Due t…
Verification of safety critical control policies using kernel methods
Nikolaus Vertovec, Sina Ober-Blöbaum, Kostas Margellos
Hamilton-Jacobi reachability methods for safety-critical control have been well studied, but the safety guarantees derived rely on the accuracy of the numerical computation. Thus,…
Multi-objective minimum time optimal control for low-thrust trajectory design
Nikolaus Vertovec, Sina Ober-Blöbaum, Kostas Margellos
We propose a reachability approach for infinite and finite horizon multi-objective optimization problems for low-thrust spacecraft trajectory design. The main advantage of the prop…