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

Yasin Sonmez; Mahmoud Khaled; Majid Zamani; Murat Arcak

eess.SYSep 12, 2026

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

Authors: Yasin Sonmez, Mahmoud Khaled, Majid Zamani, Murat Arcak

Organizations: University of California, Berkeley, USA · Ludwig-Maximilian University, Germany · University of Colorado Boulder, USA

Abstract

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.

Figures & tables

Panel of Figure 1 — Fig. 1: Threshold representation and update. (a) A lower set $K$ is stored by the column height $\tau_{K}(k)$ , so membership is the $O(1)$ test $(k,v)\in K\iff v\leq\tau_{K}(k)$ . (b) For each column, $\Phi(K)$ is a prefix whose height $f(k)$ is found by binary search; all columns are updated independently.

	Lazy [ 2 ]	Threshold (ours)
Predecessor tests	$O(CN^{2(d-1)})$	$O(CN^{d-1}\log N)$
	sequential over evolving $B$	parallel over columns
Basis update	$O(N^{2(d-1)})$	—
	sequential	—

TABLE I: Per-iteration complexity comparison.

Case	$\|X\|$	$t_{\rm pre}$	Lazy			Threshold
			$R_{\rm lazy}$	$t_{\rm lazy}$	$t_{\rm lazy+\tau}$	$R_{\rm thr}$	$t_{\rm thr}$	Speedup
ACC	$10^{6}$	$.569\,\mathrm{ms}$	182	$63.1\,\mathrm{s}$	$106\,\mathrm{ms}$	26	$3.18\,\mathrm{ms}$	$33.4\times$
ACC	$10^{9}$	$439\,\mathrm{ms}$	1595	Timeout	$126\,\mathrm{s}$	24	$16.9\,\mathrm{ms}$	$7{,}458\times$
ACC	$10^{10}$	Timeout				24	$318\,\mathrm{ms}$	-
ACC	$10^{12}$	Timeout				24	$750\,\mathrm{ms}$	-
ACC	$10^{14}$	Timeout				24	$7.94\,\mathrm{s}$	-

TABLE II: Lazy vs. Threshold Comparison.

t_{\rm pre}

is the successor-table generation time used in Lazy methods and is excluded from the reported speedups, which equal

t_{\rm lazy+\tau}/t_{\rm thr}

; R = iterations; timeout = 20 minutes.

Panel of Figure 4 — Fig. 2: Real-time controller for an unprotected left turn. An MPPI controller samples rollouts and queries the threshold table once per rollout step to evaluate the set-membership penalty. The resulting optimized control input is applied. When oncoming velocities change, the invariant set is resynthesized.

Quantity	Value
Grid cells $\|X\|$	$10^{10}=10^{4}\times 10^{2}\times 10^{4}$
Sampling period $T_{s}$	$0.1$ s
Prediction and control horizon $H_{p},H_{c}$	$20$ steps
MPPI iterations / step $N_{\mathrm{it}}$	$10$
Rollouts / iteration $N_{r}$	$512$
Perturbation standard deviation $\sigma_{u}$	$1000$ Nm

TABLE III: Real-time unprotected left turn: configuration and timings.

Explore similar work

Minimal Information Control Invariance via Vector Quantization
Apr 3, 2026Ege Yuceel, Teodor Tchalakov, Sayan MitraSafety-Critical Control Vector Quantization
Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign, Urbana, IL 61801, USA.
SMC-ES: Automated synthesis of formally verified control policies
Jul 16, 2026Riccardo Curcio, Toni Mancini, Enrico TronciFormal Verification Safe RL
Department of Computer Science, Sapienza University of Rome, via Salaria 113, 00198 Rome, Italy
Finite-Step Invariant Sets for Hybrid Systems with Probabilistic Guarantees
Apr 6, 2026Varun Madabushi, Elizabeth Dietrich, Hanna Krasowski +1Dynamical Systems
Georgia Institute of Technology · University of California, Berkeley

Apr 3, 2026J/K move · Enter open · S save

Minimal Information Control Invariance via Vector Quantization

Ege Yuceel, Teodor Tchalakov, Sayan Mitra

Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign, Urbana, IL 61801, USA.

Safety-Critical Control Vector Quantization

Open paper AskPDF arXiv

Safety-critical autonomous systems must satisfy hard state constraints under tight computational and sensing budgets, yet learning-based controllers are often far more complex than safe operation requires. To formalize this gap, we study how many distinct control signals are needed to render a compact set forward invariant under sampled-data control, connecting the question to the information-theoretic notion of invariance entropy. We propose a vector-quantized autoencoder that jointly learns a state-space partition and a finite control codebook, and develop an iterative forward certification algorithm that uses Lipschitz-based reachable-set enclosures and sum-of-squares programming. On a 12-dimensional nonlinear quadrotor model, the learned controller achieves a

157\times

reduction in codebook size over a uniform grid baseline while preserving invariance, and we empirically characterize the minimum sensing resolution compatible with safe operation.

Abstract

Explore similar work

Minimal Information Control Invariance via Vector Quantization

SMC-ES: Automated synthesis of formally verified control policies

Finite-Step Invariant Sets for Hybrid Systems with Probabilistic Guarantees