Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation
Abstract
We study safety verification for linear time-invariant systems with bounded inputs in continuous time. The standard approach reduces to a reachability analysis in two steps: first discretize time and then apply a forward analysis in the discretized system. Existing algorithms use either a fixed time step or an adaptive time step that changes based on the approximation error compared to the underlying continuous system. In this paper, we present an efficient reachability algorithm that adapts the time step based on a given safety property. Essentially, our algorithm makes the largest possible time step such that it can still prove safety. For this approach to be scalable in practice, we discuss several optimizations such as avoiding the repeated expensive calculation of the matrix exponential during discretization and a careful balance how we tame the approximation error stemming from the states and the inputs. This allows our algorithm to yield a moderate approximation error even when using a large time step, thus requiring much fewer steps than prior algorithms. We demonstrate the effectiveness and scalability on the large-scale SLICOT benchmark suite, where our algorithm consistently outperforms other state-of-the-art approaches.
Versions
Related
- Reachability and exact controllability of linear Stieltjes differential systems
- Vanishing Events and Regularity-Conditioned Reachability in Linear Stieltjes Systems
- Discrete-time polynomial systems with inputs and outputs: structure, reachability, observability, and minimal realizations
- Deep ReLU Networks Can Fail the Best Approximation Property for Continuous Target Functions
- The ball fixed point property for continuous functions on locally compact spaces
BibTeX
@misc{bjorn2026scalable,
title = {{Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation}},
author = {Mikkel Bjørn and Daniel H. Hansen and Grace Melchiors and Kim Guldstrand Larsen and Christian Schilling},
howpublished = {arXiv},
year = {2026},
month = aug,
doi = {10.48550/arxiv.2606.26352},
eprint = {2606.26352},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2606.26352},
}
RIS
TY - UNPB
TI - Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation
AU - Mikkel Bjørn
AU - Daniel H. Hansen
AU - Grace Melchiors
AU - Kim Guldstrand Larsen
AU - Christian Schilling
PY - 2026
DA - 2026/08/12
PB - arXiv
DO - 10.48550/arxiv.2606.26352
UR - https://arxiv.org/abs/2606.26352
AB - We study safety verification for linear time-invariant systems with bounded inputs in continuous time. The standard approach reduces to a reachability analysis in two steps: first discretize time and then apply a forward analysis in the discretized system. Existing algorithms use either a fixed time step or an adaptive time step that changes based on the approximation error compared to the underlying continuous system. In this paper, we present an efficient reachability algorithm that adapts the time step based on a given safety property. Essentially, our algorithm makes the largest possible time step such that it can still prove safety. For this approach to be scalable in practice, we discuss several optimizations such as avoiding the repeated expensive calculation of the matrix exponential during discretization and a careful balance how we tame the approximation error stemming from the states and the inputs. This allows our algorithm to yield a moderate approximation error even when using a large time step, thus requiring much fewer steps than prior algorithms. We demonstrate the effectiveness and scalability on the large-scale SLICOT benchmark suite, where our algorithm consistently outperforms other state-of-the-art approaches.
ER -