PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Jordan Peper, James Mathias Gast, Vignesh Nanduri, Tanmayee Maram, Ethan Howes, Ivan Ruchkin

arXiv:2608.15920v1eess.SYcs.LG

TL;DR

Designing sound finite abstractions that are not overly conservative is difficult because simulation metrics are costly and nondifferentiable. This paper introduces S^3, a smooth surrogate for gradient-based abstraction optimization, and finds strong correlation with the reverse simulation metric and effective conservatism reduction.

  • Problem

    Sound finite abstractions can be overly conservative, and distributing limited abstract states to reduce this conservatism remains a longstanding design question.

  • Method

    S^3 combines a smooth finite-horizon simulation surrogate with Taylor model-based, sound-by-construction transitions for gradient-based abstraction optimization.

  • Results

    Across case studies, S^3 strongly correlates with the finite-horizon reverse simulation metric and improves abstraction-wide discrepancy measures during optimization.

  • Takeaways & Limitations

    S^3 provides an effective, computationally efficient objective for reducing abstraction conservatism while preserving soundness by construction.

  • Takeaways & Limitations

    The certified containment condition is inconvenient during optimization, so the method uses a practical half-average-cell-width compromise for its error parameter.

Abstract

from arXiv · show

Intelligent systems are increasingly deployed in safety-critical settings with black-box controllers, including neural networks. The properties and behaviors of these end-to-end systems can be studied with abstraction-based methods that replace them with simpler finite models. Constructing such abstractions requires balancing the soundness of over-approximating the dynamical system against conservatism, which manifests as spurious or excessive nondeterministic behaviors. Bi-simulation theory provides principled metrics for characterizing these relationships, but does not prescribe how to construct sound abstractions with minimal conservatism. We fill this gap with a smooth simulation surrogate ($S^3$) --- a differentiable objective that approximates the reverse simulation metric used to quantify conservatism. Combined with Taylor model-based reachability, $S^3$ enables gradient-based optimization of abstraction parameters while preserving soundness by construction. We evaluate this optimization pipeline on three case studies. Our results show that $S^3$ is strongly correlated with the reverse simulation metric, is computationally faster, and serves as an effective objective for reducing abstraction conservatism.

Introduction

The introduction frames sound abstraction as essential but costly, then presents S^3 as a smooth, efficient surrogate enabling gradient-based reduction of conservatism while preserving soundness.

  • Motivation: Abstraction methods replace potentially infinite-state dynamical systems with finite models by partitioning continuous states and constructing behavior-capturing transitions.These abstractions support indirect analysis of complex dynamical systems.
  • Motivation: Soundness requires abstract models to over-approximate the dynamics, but this can create excessive nondeterminism, spurious transitions, and pessimistic certification results.Finer state partitions can reduce conservatism, but enlarge the abstract model and increase computational cost.
  • Problem and framework: Simulation metrics formally quantify abstraction soundness through forward simulation and over-conservatism through reverse simulation.The paper uses bi-simulation theory as its framework for characterizing these relationships.
  • Proposed approach: S^3 addresses simulation metrics’ computational expense, non-differentiability, and worst-case focus by providing a computationally efficient, smooth surrogate for over-conservatism.The surrogate is derived from the Bellman equation associated with the reverse simulation metric.
  • Contributions: The paper contributes a differentiable proxy, a gradient-based pipeline for minimizing abstraction conservatism, and case studies testing correlation with and utility for improving the real simulation metric.The pipeline is evaluated on three case studies and compared with two baseline strategies for reducing conservatism.

Preliminaries and Problem

The paper models concrete dynamics as deterministic infinite-state systems and their abstractions as nondeterministic finite-state systems induced by parameterized state quantization. It formulates abstraction design as minimizing reverse simulation conservatism subject to exact simulation, while addressing the expense and nondifferentiability of direct metric optimization.

  • System Models: A concrete system is an infinite-state tuple s = (X, X0, f) with deterministic, known, twice-differentiable dynamics f.X is the state space and X0 contains initial states; f maps X to X.
  • System Models: An abstract system is a finite-state tuple ˆs = (ˆX, ˆX0, ˆf), where nondeterministic transitions map each abstract state to a set of successors.Abstract states are indexed over Nn, and ˆf maps ˆX to its powerset.
  • Abstraction: Parameterized quantization ψθ maps concrete states to abstract states, whose preimage cells define the regions represented by each abstract state.The parameter θ belongs to a parameter space Θ, and transitions are constructed over the resulting finite abstract state set.
  • Abstraction: Soundness requires the abstract model to contain all concrete states, initial states, and one-step transitions under the quantization.These conditions provide conservative abstract representatives and preserve every concrete one-step transition.
  • Problem Formulation: The central problem minimizes the reverse simulation metric over θ subject to exact simulation, but direct evaluation is expensive and generally non-differentiable in Θ.Metric evaluation requires compiling the concrete system and quantizer into the abstraction plus a sub-optimization loop, motivating differentiable proxies and sound-by-construction pipelines.

Exact Forward Simulation by Construction

The section constructs exact forward-simulating abstractions by combining a rectilinear quantization parameterization with Taylor model-based reachable-set over-approximation. The resulting abstract transition system simulates the concrete dynamical system exactly by construction.

  • Quantization parameterization: The method parameterizes rectilinear grids with per-dimension resolutions and unconstrained gap weights transformed by Softplus into positive, normalized interval widths.This converts ordered boundary placement into an unconstrained optimization problem over Θ = R^(sum_i m_i).
  • Reachability-based transitions: First-order Taylor models over-approximate each abstract cell’s one-step image using linearized dynamics plus componentwise Taylor remainder bounds.The construction applies to any axis-aligned bounding box and explicitly determines the linear part at the cell centroid.
  • Reachability-based transitions: The reachable-set operator is sound because the worst-case remainder occurs at a corner, guaranteeing f(A) ⊆ Reach(A).The remainder is evaluated at either corner, e = e(u) = e(ℓ), to obtain the over-approximation.
  • Exact forward simulation: Proposition 1 proves that the abstract system defined from the quantization and reachable-set successors simulates the concrete system exactly: s ≲ ŝθ.The result holds for any parameter vector θ and rectilinear state quantization function ψθ when successors satisfy Equation 9.

Smooth Simulation Surrogate

This section derives the smooth simulation surrogate (S^3) as a computable proxy for the reverse simulation metric and uses it to optimize quantization parameters. It introduces finite-horizon simulation functions that measure over-conservatism while avoiding difficult infinite-horizon evaluation.

  • Smooth Simulation Surrogate: The smooth simulation surrogate (S^3) is derived as a proxy for the reverse simulation metric and used to optimize quantization parameters.The construction proceeds through Bellman-like simulation functions, finite-horizon analogues, an abstract value function, and an upper bound on the simulation metric.
  • Smooth Simulation Surrogate: Evaluating the simulation function over an infinite horizon is difficult, particularly when constructing Lyapunov-like bounds for nonlinear systems.Such bounds can be conservative while their construction may be challenging.
  • Smooth Simulation Surrogate: Finite-horizon simulation functions measure abstraction over-conservatism for discrepancies occurring within a temporal window, including finite-time co-safety specifications.Co-safety satisfaction can be determined from a finite trajectory prefix, allowing finite-horizon evaluation instead of full infinite-horizon analysis.
  • Smooth Simulation Surrogate: V_H(x, ˆx) is nondecreasing in H because admissible rollout prefixes expand monotonically, and it converges to V(x, ˆx) as H approaches infinity.The corresponding reverse simulation metric also converges to its infinite-horizon value.

Smooth simulation surrogate (S3)

S3 replaces a non-differentiable abstraction-wide discrepancy objective with smooth reachable-set over-approximations and temperature-scaled log-sum-exp aggregations. Its construction preserves soundness through reachable-set containment while exposing differentiable abstraction parameters for gradient-based optimization.

  • Construction: S3 is derived by upper-bounding the finite-horizon discrepancy and smoothing both reachable sets and remaining supremum operations.The original discrepancy is non-differentiable and lacks an abstraction-wide optimization objective; S3 addresses both issues in two stages.
  • Soundness: For inflation components ˜e_i ≥ max_j η_i,j, every concretized abstract reachable set is contained in its smooth over-approximation A_k.This condition certifies Ψθ(Â_k) ⊆ A_k for any k ≥ 0, while ˜e remains an objective hyperparameter because the sufficient bound may be conservative.
  • Smooth surrogate: Nested temperature-scaled log-sum-exp aggregations replace the suprema over horizon k ∈ [0, H] and abstract states ˆx ∈ ˆX.The temperatures τ1 and τ2 control horizon and abstract-state aggregation, respectively.
  • Hyperparameters: S3 depends on four hyperparameters: horizon H, temperatures τ1 and τ2, and inflation vector ˜e.The inflation vector determines compounding reachable-set growth over the horizon, while the experimental section guides parameter selection.
  • Optimization: The gradient ∇θ˜σ←H(s, θ) exists for all θ ∈ Θ, enabling automatic differentiation and stochastic gradient descent without assuming convexity.The constraint σ→(s, ˆsθ) = 0 is satisfied by construction for any θ through the quantization scheme and Taylor model-based transition building.

Experimental Evaluation

Across three case studies, S3 closely tracks finite-horizon reverse simulation quality while being far faster to evaluate. Optimizing S3 with stochastic gradient descent produces competitive abstractions and improves abstraction-wide quality in key comparisons.

  • Proxy validity: S3 exhibits high empirical correlation with the finite-horizon reverse simulation metric and moderate correlation with mean and median state-wise discrepancies.Correlation weakens at longer horizons, while temperature trades off maximum versus mean correlation; at H = 1, mean and median statistics have near-zero variance.
  • Computational cost: 0.01–0.02 seconds per parameter vector is required to evaluate S3, versus 2.95–4.30 seconds for Spiral, 18.4–84.4 seconds for Unicycle, and 2.44–7.38 seconds for Mountain Car.The speed advantage makes S3 practical for gradient-based optimization, whereas direct simulation-metric evaluation can be prohibitive for sample-intensive gradient-free methods.
  • Method comparison: On Mountain Car with mi = 70, Weber achieves the lowest worst-case metric at 0.070 versus 0.074, while S3 obtains mean and median discrepancies of (0.032, 0.027) and recall of 0.234.The results motivate composing the methods: Weber selects dimension-wise resolution, S3 optimizes gap widths, and CEGAR performs task-specific refinement.
  • Method comparison: S3 improves abstraction-wide quality on Unicycle by reducing mean and median discrepancies relative to the compared methods.The provided comparison reports this improvement as part of the model-checking evaluation of optimized abstractions.

Proofs of Propositions

The proofs establish exact simulation, a finite-horizon bound on concrete trajectories, and containment of concretized abstract reachable sets under cell-size error bounds.

  • Proposition 1 (Exact simulation): Proposition 1 proves that the constructed abstraction simulates the concrete dynamical system exactly.The proof shows zero distance within each quantization cell and uses successor-cell reachability plus induction.
  • Proposition 2: The proof of Proposition 2 bounds the concrete finite-horizon value by the abstraction’s trajectory-center error plus reachable-set radius.Specifically, VH(c0, ˆxo) ≤ ˆWH(ˆx).
  • Proposition 3 (Containment of abstract reachable sets): Proposition 3 proves that concretized abstract reachable sets are contained in concrete reachable sets when each error component satisfies ˜ei ≥ maxj ηi,j.The induction starts from equal initial sets and propagates containment through reachability and the error expansion.

Additional System Descriptions

The experiments cover spiral, unicycle, and MountainCarcontinuous-v0 systems with distinct state domains, dynamics, controllers, and reachability objectives. The unicycle controller combines goal attraction with obstacle repulsion, while MountainCar uses a pretrained DDPG policy.

  • Spiral system: The spiral case study is a two-dimensional, linear, time-invariant, globally exponentially stable discrete-time system on X = [−10, 10] × [−10, 10].Verification requires reaching within 2.0 units of equilibrium x∗ while remaining inside X; X0 = X.
  • Unicycle system: The unicycle is a three-dimensional Dubins system on [0.0, 50.0] × [0.0, 50.0] × [−π, π], initialized with heading in [−π/2, π/2].Its sampling time is ∆t = 0.5 and speed is v = 5.0.
  • Unicycle system: The unicycle objective is to reach a radius-8.0 goal centered at (40.0, 20.0) while avoiding a radius-5.0 obstacle centered at (25.0, 25.0) and the domain boundary.A deterministic state controller selects heading rate from a smooth guidance law.
  • Unicycle controller: The unicycle controller forms a guidance vector by combining an attractive goal vector with a repulsive obstacle vector using gains krep and katt.The desired heading is converted to bounded control through u(x) = umax tanh(kα(αd(x) − x3)); experiments set α = 0.6, ϵ = 10−6, katt = 1.0, krep = 8.0, kα = 2.5, and umax = π/4.
  • MountainCar system: MountainCarcontinuous-v0 is a two-dimensional system on X = [−1.2, 0.6]×[−0.07, 0.07] with actions u ∈[−1, 1] and a goal of reaching x1 ≥0.45.The evaluation uses a pretrained deep deterministic policy gradient (DDPG) from Stable-Baselines3 (2022).

Algorithms to Build Abstractions

The abstraction-construction procedure combines rectilinear quantization with Taylor model-based reachability to produce a finite model satisfying forward simulation by construction. It parameterizes cell widths, computes sound reachable-set over-approximations, and assigns intersecting cells as abstract successors.

  • Finite abstraction construction: Rectilinear quantization and Taylor model-based reachability construct a finite abstraction whose transitions satisfy forward simulation by construction.Abstract transitions are assigned according to Equation 9, as established in Proposition 1.
  • Reachability computation: Precomputing symbolic Jacobian and Hessian expressions substantially reduces repeated derivative-evaluation costs across quantization cells.The implementation uses SymPy to derive, simplify, and cache the analytical expressions.
  • Finite abstraction construction: Normalized Softplus maps unconstrained gap weights to positive cell widths, whose Cartesian-product intervals define the abstract state set.Initial abstract states are cells whose concretizations intersect the concrete initial set.
  • Reachability computation: For each quantization cell, first-order Taylor images of vertices define an axis-aligned linearized-image box, augmented with componentwise Taylor-remainder bounds.The affine approximation attains coordinatewise extrema at cell vertices.
  • Successor assignment: Abstract successors are all quantization cells intersecting the inflated reachable-set approximation, and the procedure returns the abstract state set, initial set, and dynamics.Algorithm 3 applies this successor-identification procedure to every abstract state.

Additional Experiments

Additional experiments show that S3’s temperature controls a trade-off between worst-case and abstraction-wide discrepancy alignment, while its optimization effects vary by system and agree qualitatively with proxy-validation results.

  • Temperature effects: Increasing S3 temperatures modestly raises correlation with mean state-wise discrepancy δH while slightly reducing correlation with worst-case metric σ←H.This trade-off persists across Tables 1, 3, and 4.
  • Temperature effects: Higher temperatures make S3 more sensitive to discrepancy distributions across abstract states and time steps rather than the largest discrepancies.Temperature-scaled log-sum-exp therefore controls whether S3 emphasizes worst-case or abstraction-wide discrepancy.
  • Hyperparameter optimization: Alternative S3 hyperparameters have system-dependent effects: Spiral is largely insensitive, Mountain Car is most sensitive, and Unicycle shows variable behavior.For Spiral, τ = 0.1 and τ = 1.0 produce nearly identical changes in simulation metrics and verification recall.
  • Agreement with proxy validation: Mountain Car confirms the trade-off: at H ∈{3, 5}, τ = 1.0 generally yields greater median reductions but increases σ←H more and changes recall less or negatively.For Unicycle at resolution 503 and H = 5, the lower-temperature objective instead produces a considerably larger worst-case-metric reduction.
  • Grid visualizations: Optimized grids allocate granularity to system-relevant regions, especially higher Unicycle turn rates x3 near obstacle or goal boundaries.Unicycle shows the greatest gap-width variation, while Mountain Car shows milder variation and Spiral has a uniform optimum.
Loading 2608.15920v1…