Saved in:
Bibliographic Details
Main Authors: Kötz, Lasse, Sjöberg, Jonas, Åkesson, Knut
Format: Preprint
Published: 2026
Subjects:
Online Access:https://arxiv.org/abs/2602.00031
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866917236112883712
author Kötz, Lasse
Sjöberg, Jonas
Åkesson, Knut
author_facet Kötz, Lasse
Sjöberg, Jonas
Åkesson, Knut
contents We present a falsification framework that integrates learned surrogate dynamics with optimal control to efficiently generate counterexamples for cyber-physical systems specified in signal temporal logic (STL). The unknown system dynamics are identified using neural ODEs, while known a-priori structure is embedded directly into the model, reducing data requirements. The learned neural ODE is converted into an analytical form via symbolic regression, enabling fast and interpretable trajectory optimization. Falsification is cast as minimizing STL robustness over input trajectories; negative robustness yields candidate counterexamples, which are validated on the original system. Spurious traces are iteratively used to refine the surrogate, while true counterexamples are returned as final results. Experiments on ARCH-COMP 2024 benchmarks show that this method requires orders of magnitude fewer experiments of the system under test than optimization-based approaches that do not model system dynamics.
format Preprint
id arxiv_https___arxiv_org_abs_2602_00031
institution arXiv
publishDate 2026
record_format arxiv
spellingShingle Optimal Control-Based Falsification of Learnt Dynamics via Neural ODEs and Symbolic Regression
Kötz, Lasse
Sjöberg, Jonas
Åkesson, Knut
Systems and Control
We present a falsification framework that integrates learned surrogate dynamics with optimal control to efficiently generate counterexamples for cyber-physical systems specified in signal temporal logic (STL). The unknown system dynamics are identified using neural ODEs, while known a-priori structure is embedded directly into the model, reducing data requirements. The learned neural ODE is converted into an analytical form via symbolic regression, enabling fast and interpretable trajectory optimization. Falsification is cast as minimizing STL robustness over input trajectories; negative robustness yields candidate counterexamples, which are validated on the original system. Spurious traces are iteratively used to refine the surrogate, while true counterexamples are returned as final results. Experiments on ARCH-COMP 2024 benchmarks show that this method requires orders of magnitude fewer experiments of the system under test than optimization-based approaches that do not model system dynamics.
title Optimal Control-Based Falsification of Learnt Dynamics via Neural ODEs and Symbolic Regression
topic Systems and Control
url https://arxiv.org/abs/2602.00031