TTT: A Temporal Refinement Heuristic for Tenuously Tractable Discrete Time Reachability Problems

TL;DR

This paper tackles the challenge of computing formally correct reachability sets for nonlinear control systems with neural-network controllers, where exact methods are intractable. It introduces temporal refinement, an automated approach that selects when along the time horizon to perform symbolic queries of depth $b_{ ext{steps}}$ under a budget $b$, balancing tightness and computational cost. The method is instantiated for forward reachability in Neural Feedback Loops (NFLs) using MILP-based overapproximation and a hybrid symbolic-concrete query strategy, building on prior symbolic-reachability work. Empirically, the approach achieves 20–70% faster computation than hand-tuned baselines while delivering comparable or tighter error bounds, demonstrating practical scalability for complex control systems.

Abstract

Reachable set computation is an important tool for analyzing control systems. Simulating a control system can show general trends, but a formal tool like reachability analysis can provide guarantees of correctness. Reachability analysis for complex control systems, e.g., with nonlinear dynamics and/or a neural network controller, is often either slow or overly conservative. To address these challenges, much literature has focused on spatial refinement, i.e., tuning the discretization of the input sets and intermediate reachable sets. This paper introduces the idea of temporal refinement: automatically choosing when along the horizon of the reachability problem to execute slow symbolic queries which incur less approximation error versus fast concrete queries which incur more approximation error. Temporal refinement can be combined with other refinement approaches as an additional tool to trade off tractability and tightness in approximate reachable set computation. We introduce a temporal refinement algorithm and demonstrate its effectiveness at computing approximate reachable sets for nonlinear systems with neural network controllers. We calculate reachable sets with varying computational budget and show that our algorithm can generate approximate reachable sets with a similar amount of error to the baseline in 20-70% less time.

Figures (6)

• Figure 1: An illustration of overapproximate forward reachability. A symbolic query uses multiple copies of the dynamical system update function $f(x)$ within a single computation to produce tighter final sets. This concept is central to the refinement algorithm.
• Figure 2: An illustration of Alg. \ref{['alg:overall']}. In this example $b_{\text{steps}}=4$.
• Figure 3: Approximate reachable sets of various fidelity are produced depending on allotted time and are competitive with hand-tuned baseline sidrane2022overt indicated with dashed lines.
• Figure 4: Reachable sets for pendulum problem S1 with two layer, 25 neuron-per-layer neural network controller show less error than the naive baseline and greater speed than the hand-tuned baseline for less error.
• Figure 5: Dimensions 1 and 2 of the reachable sets for TORA problem T1 with three layer, 25 neuron-per-layer neural network controller which has less error than the naive baseline and greater speed than the hand-tuned baseline for similar error.