$S^3$: A Smooth Simulation Surrogate for Optimizing Discrete Abstractions of Dynamical Systems

What the math gives to ML

The paper provides a constructive mechanism for reducing conservatism in finite abstractions of nonlinear dynamical systems: parameterize abstract cells and transitions, use a differentiable surrogate for the reverse simulation metric, and optimize these parameters while Taylor-model reachability preserves soundness. The transferable asset is a differentiable mismatch objective whose minimization reduces spurious abstract behaviors without relaxing safety over-approximation. A promising neural-network transfer is to jointly train a controller or latent dynamics model and a differentiable finite abstraction, using the surrogate as a regularizer while enforcing reachability containment as a hard constraint. The key falsifiable prediction is that the smooth surrogate should track the nonsmooth reverse simulation metric and that optimized abstractions should reduce abstract branching and reachable-set volume without losing concrete trajectories.