PaperlayerView exact revision on arXiv

Source-linked AI summary

Real-Time Synthesis of Robust Controlled Invariant Sets for Monotone Systems

Yasin Sonmez, Mahmoud Khaled, Majid Zamani, Murat Arcak

arXiv:2609.14115v1eess.SYcs.AIcs.ROcs.SY

TL;DR

Safety-critical control needs invariant safety certificates that can be recomputed as conditions change, but synthesis can be costly and lazy basis methods retain membership and redundancy-check bottlenecks. The paper reformulates the iteration using threshold functions, reporting large speedups and real-time-scale synthesis while requiring monotone dynamics and lower-closed safety.

  • Problem

    Controlled invariant sets certify regions whose trajectories can be kept safe indefinitely, while synthesis costs grow with state dimension and lazy basis methods retain costly membership and sequential redundancy checks.

    Source: §I · p. 1

  • Method

    The paper represents lower-closed sets by threshold functions and uses parallel column updates instead of tracking and updating antichain bases.

    Source: §I · p. 1

  • Results

    The threshold iteration is reported to be orders of magnitude faster than lazy fixed-point iteration and to reach grids exceeding 10^9 cells around 100 ms.

    Source: §V · p. 6

  • Takeaways & Limitations

    The threshold table supplies O(1) membership queries that can be used in an optimizer for safety-informed closed-loop control.

    Source: B. Real-time controller: unprotected… · p. 6

    The method requires monotonicity under an orthant order and a lower-closed safety set, and its grid resolution is bounded by GPU memory.

    Source: §V · p. 6

Abstract

from arXiv · show

Safety-critical control of autonomous systems requires formal safety certificates, such as controlled invariant sets, that must be computed online as conditions change. Although standard synthesis algorithms scale poorly with state dimension, monotone dynamical systems with lower-closed safety specifications allow for accelerated computation of controlled invariant sets. In particular, lazy fixed-point algorithms exploit monotonicity and track only the antichain basis of the set. However, membership tests and redundancy checks against an evolving basis remain major bottlenecks. We introduce a threshold-function reformulation in which a lower-closed set on a d-dimensional grid is represented by its column heights along a designated axis. This reformulates the greatest-fixed-point iteration as independent one-dimensional binary searches, one per grid column, yielding an embarrassingly parallel iteration with asymptotically lower computational complexity than the lazy fixed-point algorithm. Experiments synthesize invariant sets on 3D grids with 10^9 cells in under 50 ms and 10^14 cells in under two minutes. We further demonstrate online re-synthesis in a safety-informed model predictive controller example.

I. INTRODUCTION

The paper replaces evolving antichain bases with threshold functions to accelerate invariant-set synthesis for monotone systems with lower-closed safety sets. It motivates this design by the cost of basis membership and neighbor checks, while framing lower sets as compactly represented by their maximal elements.

I. INTRODUCTION

  • Lazy fixed-point methods exploit monotonicity by tracking an antichain basis, but membership scans cost O(N^(2(d−1))) per iteration and neighbor redundancy checks limit parallelism.The basis has O(N^(d−1)) elements on an N d grid.Source: §I · p. 1
  • Threshold functions store lower-set boundaries along a designated axis, enabling O(1) membership queries and parallel column updates with O(N^(d−1) log N) work per iteration.This representation avoids basis enumeration and sequential neighbor checks.Source: §I · p. 1
  • The method is experimentally reported to yield speedups on the order of thousands over basis-based lazy synthesis.The introduction also reports a 1014-cell scaling benchmark completed in under two minutes.Source: §I · p. 1

A. Monotone systems and lower sets

  • A lower set contains every state below each of its members, and its maximal elements form a basis that determines the set.On the stated grid, the basis is bounded by O(N^(d−1)), compared with O(N^d) grid states.Source: A. Monotone systems and lower sets · p. 2

B. Monotone dynamics and the robust controlled pre-operator

The robust controlled predecessor retains states that remain safe after one step under some control for every adversarial mode. Under state monotonicity and lower-closed safety, iterating this operator yields the maximal robust controlled invariant subset in finitely many steps.

B. Monotone dynamics and the robust controlled pre-operator

  • The predecessor keeps states in A for which some admissible control sends every adversarial successor into B.A controlled invariant set is a fixed point of this operator.Source: B. Monotone dynamics and the robust… · p. 2
  • When stronger control- or disturbance-monotonicity variants hold, predecessor checks can be restricted to minimal controls, maximal adversarial modes, or both.The correctness results require only state monotonicity; these reductions apply under the stronger variants.Source: B. Monotone dynamics and the robust… · p. 2
  • Under state monotonicity and lower-closed safety, the predecessor of any lower set is itself a lower set.This preserves the lower-set structure through the iteration.Source: B. Monotone dynamics and the robust… · p. 2
  • Repeated predecessor application from the safe set descends in finitely many steps to its maximal robust controlled invariant subset.The sequence consists of lower sets and terminates because the abstract state space is finite.Source: B. Monotone dynamics and the robust… · p. 2

C. Lazy fixed-point iteration

The lazy fixed-point method stores the evolving antichain basis rather than the full grid, but scan-based checks and sequential updates drive its cost.

C. Lazy fixed-point iteration

  • O(Rlazy C N^2(d−1)) safety-check work and O(Rlazy N^2(d−1)) neighbor-generation work arise under scan-based basis membership.Rlazy is the number of complete outer basis passes; the basis has size O(N^(d−1)).Source: C. Lazy fixed-point iteration · p. 3
  • After each basis removal, candidate neighbors require redundancy checks against the evolving basis, making updates sequential.The algorithm stores and updates the current antichain basis rather than the full grid.Source: C. Lazy fixed-point iteration · p. 3

III. THRESHOLD-FUNCTION ITERATION

The section introduces the threshold-function approach, its parallel binary-search reformulation of one GFP step, and its equivalence and complexity analysis.

III. THRESHOLD-FUNCTION ITERATION

  • The section presents the threshold representation, parallel per-column binary searches for one GFP step, then equivalence with Algorithm 1 and complexity analysis.Source: §III · p. 3

A. The threshold-function representation

A lower set is represented by threshold heights over a projection onto all but one designated axis, making membership a comparison against the height for that column.

A. The threshold-function representation

B. The threshold iteration

The GFP update preserves a prefix in each grid column, so its threshold can be found by binary search and updated independently across columns.

B. The threshold iteration

  • Monotonicity ensures that if a state in a column can maintain K, every lower state in that column can also maintain K.Thus the maintainable states form a contiguous prefix with height f(k).Source: B. The threshold iteration · pp. 3–4
  • A binary search over {1, ..., τ(k)} finds each column's prefix height f(k) in O(log N) probes.The search predicate is monotone nonincreasing in v.Source: B. The threshold iteration · p. 4
  • Because each column's threshold update is independent, all columns can be processed in parallel.Algorithm 2 repeats the updates until τ is unchanged, then returns the lower set represented by τ.Source: B. The threshold iteration · p. 4

C. Correctness, convergence, and complexity

The threshold iteration preserves the predecessor fixed-point semantics: its iterates remain lower, descend finitely to K*, and match the lazy basis result. Its boundary updates are parallelized, with a dense-storage tradeoff.

C. Correctness, convergence, and complexity

  • Starting from the safe set, threshold iteration produces lower sets that descend finitely to the maximal robust controlled invariant subset K*.Each iterate is obtained as the predecessor of the previous set.Source: C. Correctness, convergence, and… · p. 4
  • The lazy basis and threshold algorithms return the same maximal robust controlled invariant set K* from the same safe set.The threshold sequence converges to K*, and the lazy algorithm returns that same set.Source: C. Correctness, convergence, and… · p. 4
  • Independent column updates replace quadratic lazy boundary work with a parallel threshold stage.Each column's threshold update is independent of the others.Source: C. Correctness, convergence, and… · p. 4
  • Threshold storage uses one value per column even when a sparse basis could use less memory; choosing the axis with maximal N_d* minimizes that storage.The threshold representation is attractive for dense or irregular frontiers and workloads dominated by membership queries.Source: C. Correctness, convergence, and… · p. 4

IV. EXPERIMENTS

The experiments cover adaptive cruise control in 3D and 5D and two unprotected-turn benchmarks. Their setups use monotone-system structure and lower-closed safety specifications.

IV. EXPERIMENTS

  • The 3D ACC state is headway and ego and lead speeds, with ego torque control and an adversarial mode for lead braking and parameter uncertainty.Its safe set requires headway to exceed the worst-case braking-distance map, and is lower-closed when that map is nondecreasing.Source: §IV · pp. 4–5
  • ACC-5D adds ego and lead actuator states, whose dynamics follow first-order response equations.The actuator states replace direct torque arguments in the acceleration models.Source: §IV · p. 4
  • Both unprotected-turn benchmarks use ego position and speed plus oncoming-car position, with no exogenous disturbance channel.Turn-Oncoming models ego waiting while the oncoming car passes; Turn-Ego models ego passing first.Source: §IV · p. 5
  • Turn safety sets forbid simultaneous conflict-zone occupation while enforcing ego or oncoming priority under the corresponding orthant order.The priority constraints are lower-closed, with monotonicity following from the dynamics' sign structure.Source: §IV · p. 5

A. Lazy vs. threshold comparison

Threshold iteration substantially outperforms the lazy approaches in the reported scaling tests and completes at grid sizes where the basis method exceeds time or memory limits. The comparison distinguishes representation changes from changes to the Lazy traversal schedule.

A. Lazy vs. threshold comparison

  • Lazy+τ retains Lazy's traversal and immediate-deletion schedule while changing representation and boundary maintenance; its basis is materialized after each pass.Both Lazy methods use the same pass, immediate-deletion schedule, and precomputed successor cache.Source: A. Lazy vs. threshold comparison · p. 5
  • The threshold implementation uses inline dynamics because a full successor table would require O(C|X|) memory and becomes a bottleneck on larger grids.Experiments used C++/pFaces with OpenCL kernels on an NVIDIA RTX 5090 GPU and AMD Ryzen 9 9950X3D CPU.Source: A. Lazy vs. threshold comparison · p. 5
  • At |X| = 10^9, threshold iteration is thousands of times faster; at |X| ≥ 10^10, it completes while the basis method exceeds the time or memory budget.The threshold method uses an O(N^(d−1)) table and eliminates antichain maintenance.Source: A. Lazy vs. threshold comparison · p. 5

B. Real-time controller: unprotected left turn

The controller models the left turn as two 3D robust-safety phases and resynthesizes their invariant sets when sensed oncoming speed changes. It uses the synthesized set in MPPI rollouts, but does not provide a formal closed-loop safety guarantee.

B. Real-time controller: unprotected left turn

  • The two-phase controller waits for the first oncoming vehicle to clear, then turns before the second closes the gap, resynthesizing sets when sensed speed changes sufficiently.Each phase is a 3D robust-safety problem in (se, ve, sonc).Source: B. Real-time controller: unprotected… · p. 5
  • MPPI queries the threshold table once per rollout step and applies its optimized input; it suits the nonsmooth penalty without requiring threshold-representation gradients.The invariant-set algorithm returns K*, not an explicit policy; first-order MPC methods would need to smooth the discontinuous membership test.Source: Figure 2 · p. 6, B. Real-time controller: unprotected… · p. 6
  • The lifted set K2 intersects the two phase constraints for rollout membership queries, but is not claimed to be a 4D controlled-invariant set.A formal 4D invariance claim would require a common witness input, which need not exist because the wait and go constructions impose opposite orthant orders on (se, ve).Source: B. Real-time controller: unprotected… · p. 6
  • The controller uses set membership as a penalty rather than a hard constraint, so it provides no formal closed-loop safety guarantee.Such a guarantee would require a hard one-step invariant constraint or an invariant-preserving backup policy; lookup and MPPI computation times are negligible relative to resynthesis.Source: B. Real-time controller: unprotected… · p. 6

V. CONCLUSION

The conclusion presents threshold-function synthesis as a parallel reformulation that greatly accelerates invariant-set computation for monotone systems, while noting its assumptions, policy, and memory limits.

V. CONCLUSION

  • Threshold-function reformulation makes greatest-fixed-point invariant-set synthesis embarrassingly parallel, with benchmark speedups on the order of thousands over lazy iteration.The threshold iteration reaches grids exceeding 10^9 cells around 100 ms and enables real-time re-synthesis for closed-loop control.Source: §V · p. 6
  • The method requires monotonicity under some orthant order and a lower-closed safety set, and the threshold table stores the set rather than a specific control policy.Source: §V · p. 6
  • Grid resolution is bounded by GPU memory because the threshold table requires O(N^(d−1)) integers.Source: §V · p. 6
Loading 2609.14115v1…