Projects and Associated Publications

Research Series

LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems

By Oliver Schön, Ernesto Casablanca, Paolo Zuliani, Sadegh Soudjani

Ensuring the safety of AI-enabled systems, particularly in high-stakes domains such as autonomous driving and healthcare, has become increasingly critical. Traditional formal verification tools fall short when faced with systems that embed both opaque, black-box AI components and complex stochastic dynamics. To address these challenges, we introduce LUCID (Learning-enabled Uncertainty-aware Certification of stochastIc Dynamical systems), a verification engine for certifying safety of black-box stochastic dynamical systems from a finite dataset of random state transitions. As such, LUCID is the first known tool capable of establishing quantified safety guarantees for such systems.

Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings
We show how to solve the resulting program for unknown polynomial dynamics efficiently using sum-of-squares optimization. 2024 IEEE American Control Conference (ACC).
Full Paper

Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification

Oliver Schön, Shammakh Naseer, Ben Wooding, Sadegh Soudjani

8th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2024).

 

Formal verification of stochastic systems using Binary-Tree Gaussian Processes (BTGPs) for efficient abstraction. BTGPs naturally partition the state space, simplifying error quantification. This yields formal models that are amenable to model checking.

Research Series

SySCoRe: Synthesis via Stochastic Coupling Relations

By Oliver Schön, Birgit van Huijgevoort, Sofie Haesaert, Sadegh Soudjani

This research line develops a powerful method for synthesizing correct-by-design controllers for uncertain stochastic systems via stochastic simulation relations. The abstraction-based approach handles infinite-horizon LTLf specifications and non-Gaussian stochasticity. By leveraging tensor representations of Markov decision processes, the framework achieves superior scalability compared to traditional methods. Recent advancements address epistemic uncertainty, compositionality, and integrate Bayesian techniques to enable data-driven control synthesis. This combination of abstraction, uncertainty handling, and data-driven methods provides a robust solution for designing controllers in safety-critical environments.

Open challenges are extension to LTL specifications and furthering scalability.

Also see my video on sub-simulation relations.

Correct-by-Design Control of Parametric Stochastic Systems
Establishing formal guarantees while allowing for epistemic uncertainty is still a great challenge. We investigate ways of relating parametric stochastic systems to their nominal model. IEEE 61st Conference on Decision and Control (CDC 2022).
Full Paper
ARCH-COMP22 Category Report: Stochastic Models
A friendly competition for formal verification and policy synthesis of stochastic models showcasing the performance and limits of state-of-the-art solution approaches. 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22).
Full Paper
SySCoRe: Synthesis via Stochastic Coupling Relations
Developed MATLAB toolbox for synthesizing robust controllers for stochastic continuous-state systems to satisfy temporal logic specifications and quantifying the associated formal robustness guarantees. 26th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2023).
Full Paper
Poster Abstract: Data-Driven Correct-by-Design Control of Parametric Stochastic Systems
We propose a two-stage approach for data-driven controller synthesis for safety-critical systems, combining Bayesian regression for robust parameter estimation with formal methods to handle stochastic and parametric uncertainties using simulation relations based on sub-probability measures. 26th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2023).
View Poster
Verifying the Unknown: Correct-by-Design Control Synthesis for Networks of Stochastic Uncertain Systems
We extend sub-simulation relations to compositional systems and provide results for stochastic systems with arbitrary additive noise distributions. 2023 62nd IEEE Conference on Decision and Control (CDC).
Full Paper
ARCH-COMP23 Category Report: Stochastic Models
A friendly competition for formal verification and policy synthesis of stochastic models showcasing the performance and limits of state-of-the-art solution approaches. 10th International Workshop on Applied Verication of Continuous and Hybrid Systems (ARCH23).
Full Paper
Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relations
We present a data-driven approach for correct-by-design control synthesis via stochastic simulation relations and Bayesian linear regression. IEEE Transactions on Automatic Control.
Full Paper
Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates
We propose an adversarial framework that significantly enhances the scalability and practical applicability of probabilstic simulation relations by eliminating the need to compute error bounds directly. International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (QEST 2025)
Full Paper
Previous
Next

Multi-Objective Physics-Guided Recurrent Neural Networks for Identifying Non-Autonomous Dynamical Systems

Oliver Schön, Ricarda Samantha-Götte, Julia Timmermann

14th IFAC Workshop on Adaptive and Learning Control Systems (ALCOS 2022).

 

Learning dynamics models from data whilst utilizing physics-based knowledge for efficient convergence and physically plausible models. Combining a multi-objective approach, an approximate dynamics model, and a recurrent neural network.

Theses

Since their introduction, Physics-guided Neural Networks (PGNN), a novel class of hybrid models, have already been successfully implemented in several domains of application. As a result, both synergetic effects as well as physically sound models were obtained. Within the context of this thesis, for the first time, the potential of PGNNs for the identification of dynamic systems is investigated from a control engineering point of view. Various approaches are identified and first investigations are performed. By combining a recurrent neural network with a physical dynamics model, a Physics-guided Recurrent Neural Network (PGRNN) is constructed. It is demonstrated that the PGRNN generally outperforms a purely data-driven approach by a substantial margin. Further investigations indicate that the quality of the introduced dynamics model is merely of minor importance to the resulting performance benefits. Consecutively, the PGRNN is augmented by a physics-based constraint, inciting energy conserving solutions as well as a function library of nonlinear terms. The latter resulted in the full compensation of prediction error deficiencies due to inaccurate dynamic models.

 

Full Text (in German)

Bayesian Optimization is a powerful tool for providing solutions to complex optimization problems, e.g. as part of setup processes. It enables the automated setting of basic tuning parameters, especially when the collection of data is very time- and cost-intensive. The optimization of both processes and devices usually takes place without any understanding of the regarding systems in the form of a black box optimization. In the context of technical systems, however, prior knowledge is typically available in the form of a physical dynamics model, which could potentially result in greater efficiency of the optimization process. In order of investigating this connection in more detail, the effect of a priori knowledge in the context of the optimization process is examined on the basis of an exemplary application. It can be shown that the utilization of sufficiently accurate prior knowledge results in a significant increase in the efficiency of the Bayesian optimizer. In addition to the conditioning of the optimization problem, the dimension of the problem also plays a particularly important role. In general, however, the use of a priori knowledge should not be neglected, since the number of required iterations can already be reduced by specifying rough baselines and performance losses only occur in special cases due to the introduction of misleading information.


Full Text (in German)

All Publications on Google Scholar

Title Citations Year
Kernel-Based Learning of Safety Barriers

O Schön, Z Zhong, S Soudjani

arXiv preprint arXiv:2601.12002, 2026

1 2026
LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems

E Casablanca, O Schön, P Zuliani, S Soudjani

arXiv preprint arXiv:2512.11750, 2025

1 2025
Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates

O Schön, S Haesaert, S Soudjani

International Conference on Quantitative Evaluation of Systems and Formal …, 2025

1 2025
Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)

O Schön, S Haesaert, S Soudjani

arXiv preprint arXiv:2506.16971, 2025

2025
Bayesian formal synthesis of unknown systems via robust simulation relations

O Schön, B van Huijgevoort, S Haesaert, S Soudjani

IEEE Transactions on Automatic Control, 2024

13* 2024
Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings

O Schön, Z Zhong, S Soudjani

2024 American Control Conference (ACC), pp. 3417-3423, 2024

12 2024
Lyapunov-based policy synthesis for multi-objective interval mdps

N Monir, O Schön, S Soudjani

IFAC-PapersOnLine 58 (11), 99-106, 2024

3 2024
Data-driven abstractions via binary-tree Gaussian processes for formal verification

O Schön, S Naseer, B Wooding, S Soudjani

IFAC-PapersOnLine 58 (11), 115-122, 2024

5 2024
Verifying the unknown: Correct-by-design control synthesis for networks of stochastic uncertain systems

O Schön, B van Huijgevoort, S Haesaert, S Soudjani

2023 62nd IEEE Conference on Decision and Control (CDC), 7035-7042, 2023

7 2023
ARCH-COMP23 category report: stochastic models

A Abate, H Blom, N Cauchi, J Delicaris, S Haesaert, B van Huijgevoort, ...

10th International Workshop on Applied Verification of Continuous and Hybrid …, 2023

7 2023
Data-Driven Correct-by-Design Control of Parametric Stochastic Systems✱

O Schön, B Van Huijgevoort, S Haesaert, S Soudjani

Proceedings of the 26th ACM International Conference on Hybrid Systems …, 2023

2023
SySCoRe: Synthesis via stochastic coupling relations

B Van Huijgevoort, O Schön, S Soudjani, S Haesaert

Proceedings of the 26th ACM international conference on hybrid systems …, 2023

26 2023
SySCoRe Repeatability Package (ARCH 2023)

O Schön, S Soudjani, S Haesaert, B van Huijgevoort

https://doi.org/10.24433/co.8616869.v1, 2023

2023
Correct-by-Design Control of Parametric Stochastic Systems

O Schön, B van Huijgevoort, S Haesaert, S Soudjani

2022 IEEE 61st Conference on Decision and Control (CDC), 5580-5587, 2022

9 2022
SySCoRe: Synthesis via Stochastic Coupling Relations (Code)

B van Huijgevoort, O Schön, S Soudjani, S Haesaert

https://doi.org/10.24433/co.3825821.v1, 2022

2022
SySCoRe Repeatability Package (ARCH 2022)

O Schön, B van Huijgevoort, S Soudjani, S Haesaert

https://doi.org/10.24433/co.2213659.v1, 2022

2022
ARCH-COMP22 Stochastic Models

A Abate, H Blom, J Delicaris, S Haesaert, A Hartmanns, ...

EPiC Series in Computing, 2022

17 2022
Multi-Objective Physics-Guided Recurrent Neural Networks for Identifying Non-Autonomous Dynamical Systems

O Schön, RS Götte, J Timmermann

14th IFAC Workshop on Adaptive and Learning Control Systems ALCOS 2022, 19-24, 2022

13 2022
Physics-Guided Neural Networks for Identifying Dynamical System

O Schön

Master's Thesis, Universität Paderborn, 2021

1* 2021
Efficient Bayesian Optimization using A-Priori Knowledge of a Physical Dynamics Model

O Schön

Project Thesis, Universität Paderborn, 2019

1* 2019

Meet My Collaborators

http://oliverschon.com/wp-content/uploads/2022/12/021222-NUHeadshots-40-scaled-e1672141173377.jpg

Dr. Sadegh Soudjani

Max Planck Institute SWS, Germany

Dr. Sofie Haesaert

TU Eindhoven, The Netherlands

Dr. Birgit van Huijgevoort

TU Eindhoven, The Netherlands

Dr. Ben Wooding

Newcastle University, UK

Dr. Zhengang Zhong

University of Warwick, UK