Reachability Analysis of Linear Hybrid Systems with Scalable Time-Step Adjustment
Authors
Hansen, Daniel Hilo ; Melchiors, Grace ; Bjørn, Mikkel Daniel
Term
4. term
Education
Publication year
2026
Submitted on
2026-06-04
Abstract
Reachability analysis is a method used to check whether a system can enter unsafe or undesirable states within a given time period. In earlier work, we developed a method for linear continuous systems, where the system’s state changes smoothly over time. This method uses an adaptive time step size that automatically adjusts based on a specified safety property, making the analysis both efficient and accurate. In this thesis, we extend the method to linear hybrid systems, which combine continuous evolution with sudden discrete jumps in the system state. For these systems, we let the time step size depend not only on the safety property, but also on the guard set (conditions that trigger state changes) and the invariant set (states in which the system must remain). The improved reachability algorithm chooses, at each point in time, the largest possible time step that still ensures the computed over-approximation does not violate any safety properties. Larger time steps mean fewer computation steps and thus shorter runtime, while we can still decrease the time step size when needed to achieve the same precision as with a fixed time step size. We demonstrate that this property-driven time step adaptation reaches state-of-the-art performance on four challenging benchmark problems.
Rækkeviddeanalyse er et værktøj, der bruges til at kontrollere, om et system kan komme i farlige eller uønskede tilstande inden for en given tidsperiode. I tidligere arbejde har vi udviklet en metode til lineære kontinuerte systemer, hvor systemets tilstand udvikler sig jævnt over tid. Metoden bruger en variabel tidsstørrelse, der automatisk tilpasses ud fra en given sikkerhedsegenskab, så analysen bliver både effektiv og præcis. I denne afhandling udvider vi metoden til også at omfatte lineære hybride systemer, hvor der både kan ske kontinuerlige ændringer og pludselige spring i systemets tilstand. Her lader vi tidsstørrelsen afhænge ikke blot af sikkerhedsegenskaben, men også af systemets "guard set" (betingelser for at skifte tilstand) og "invariant set" (tilstande som systemet skal blive i). Den forbedrede algoritme vælger ved hvert tidspunkt det størst mulige tidsinterval, som stadig sikrer, at den beregnede over-approksimation ikke bryder nogen sikkerhedsegenskaber. Større tidsintervaller betyder færre beregningstrin, hvilket reducerer den samlede køretid, mens vi stadig kan reducere tidsstørrelsen, når det er nødvendigt, for at opnå samme præcision som ved en fast tidsstørrelse. Vi viser, at denne egenskabsstyrede tilpasning af tidsstørrelsen giver resultater på niveau med de bedste eksisterende metoder på fire krævende testeksempler.
[This abstract has been rewritten with the help of AI based on the project's original abstract]
Keywords