Paper deep dive
Real-Time Synthesis of Robust Controlled Invariant Sets for Monotone Systems
Yasin Sonmez, Mahmoud Khaled, Majid Zamani, Murat Arcak
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 96%
Last extracted: 9/20/2026, 4:19:30 AM
Summary
This paper introduces a threshold-function reformulation for computing robust controlled invariant sets in monotone systems. By representing lower-closed sets as column heights on a grid, the method transforms the greatest-fixed-point iteration into independent one-dimensional binary searches. This approach eliminates the sequential bottlenecks of traditional lazy fixed-point algorithms, enabling embarrassingly parallel computation with significantly lower asymptotic complexity. Experiments demonstrate synthesis of invariant sets on grids with up to 10^14 cells in under two minutes.
Entities (10)
Relation Signals (9)
Mahmoud Khaled → affiliatedwith → Ludwig-Maximilian University
confidence 99% · M. Khaled is with the Ludwig-Maximilian University, Germany
Yasin Sonmez → affiliatedwith → University of California, Berkeley
confidence 99% · Y. Sonmez and M. Arcak are with the University of California, Berkeley, USA
Murat Arcak → affiliatedwith → University of California, Berkeley
confidence 99% · Y. Sonmez and M. Arcak are with the University of California, Berkeley, USA
Majid Zamani → affiliatedwith → University of Colorado Boulder
confidence 99% · M. Zamani is with the University of Colorado Boulder, USA
Threshold-Function Iteration → computes → Controlled Invariant Set
confidence 98% · We introduce a threshold-function reformulation... This reformulates the greatest-fixed-point iteration... Experiments synthesize invariant sets...
Threshold-Function Iteration → appliesto → Monotone Systems
confidence 97% · monotone dynamical systems with lower-closed safety specifications allow for accelerated computation of controlled invariant sets.
Threshold-Function Iteration → improvesupon → Lazy Fixed-Point Algorithm
confidence 95% · yielding an embarrassingly parallel iteration with asymptotically lower computational complexity than the lazy fixed-point algorithm.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2609.14115v1
- Canonical: https://arxiv.org/abs/2609.14115v1
Trouble viewing inline? Open PDF directly →
Full Text
38,514 characters extracted from source content.
Expand or collapse full text
Real-Time Synthesis of Robust Controlled Invariant Sets for Monotone SystemsThanks: Y. Sonmez and M. Arcak are with the University of California, Berkeley, USA (yasin_sonmez,arcak@berkeley.edu); M. Zamani is with the University of Colorado Boulder, USA (majid.zamani@colorado.edu); M. Khaled is with the Ludwig-Maximilian University, Germany (m.mahmoud@lmu.de). This work is supported in part by the NSF grant CNS-2111688. Yasin Sonmez, Mahmoud Khaled, Majid Zamani, Murat Arcak Affiliation: 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 10910^9 cells in under 50 ms and 101410^14 cells in under two minutes. We further demonstrate online re-synthesis in a safety-informed model predictive controller example. I Introduction Controlled invariant sets characterize safe regions in which trajectories can be kept for all future time through appropriate control actions. Symbolic abstractions [1] locate controlled invariant sets through finite-state fixed-point computations, but their cost grows sharply with state dimension. One approach to overcome the scalability barrier is to exploit monotone dynamics: When the dynamics are monotone with respect to a partial order and the safe set is lower-closed with respect to the same order, the maximal robust controlled invariant set is also lower-closed and is uniquely determined by its antichain basis [2]. On an NdN^d grid, the basis size is O(Nd−1)O(N^d-1), one order of magnitude smaller than the underlying grid. The lazy fixed-point algorithms of [2, 3, 4] track only the basis and update the antichain boundary between iterations. Two bottlenecks remain despite this reduction: 1. Quadratic per-iteration cost. Each iteration performs O(Nd−1)O(N^d-1) safety checks, and each check scans the basis to test membership in its lower closure, giving O(N2(d−1))O(N^2(d-1)) work per iteration. 2. Sequential neighbor generation. After unsafe elements are removed, new candidate neighbors must be added to the basis, each requiring a redundancy check—an inherently sequential step that limits parallelism. Instead of representing the boundary of the lower-closed set with basis points, which must be iteratively updated and searched, in this paper we store this surface as a threshold function along a designated axis. We then reformulate the greatest-fixed-point (GFP) iteration to operate solely on this threshold function, eliminating basis tracking and sequential neighbor generation. The contributions are: • We encode lower-closed sets by a threshold function with O(Nd−1)O(N^d-1) storage and O(1)O(1) membership queries. Parallel column updates yield per-iteration work O(Nd−1logN)O(N^d-1 N) without basis enumeration or neighbor checks. • We prove one-step equivalence with the predecessor operator and equivalence with the lazy basis formulation. • We show experimentally that the threshold iteration yields speedups on the order of thousands over basis-based lazy synthesis. The 101410^14-cell scaling benchmarks complete in under two minutes, while the separate 101010^10-cell closed-loop experiment completes in approximately 62–77 ms. Existing synthesis methods that leverage structural properties include sparse and compositional constructions for monotone systems and directed specifications [5], flexible abstraction-based pipelines [6], lazy exploration of exposed boundaries using antichain representations [4], and ordered reductions for robust controlled invariance [7]. Height encodings of staircase sets and discrete Pareto frontiers are well-established. Our contribution lies not in the height encoding, but in its use as the sole representation in robust invariant-set GFP iteration, together with the column-prefix result, binary-search update, equivalence proof, and parallel implementation. I Preliminaries I-A Monotone systems and lower sets We study continuous-time systems of the form ξ˙=f(ξ,u,ϑ), ξ=f(ξ,u, ), (1) where ξ∈ℝdξ ^d is the continuous state, u∈ℝmu ^m is the control input, and ϑ collects exogenous effects such as disturbances and uncertain parameters. We obtain a finite model from (1) using sampled-data symbolic abstraction [1, 8, 9]. Given a sampling period, state grid, and finite input alphabet, we overestimate one-step reachable sets under all admissible exogenous signals and obtain a finite transition system, x+=F(x,u,δ).x^+=F(x,u,δ). (2) Here, x belongs to a finite grid X, u belongs to a finite admissible control set U, and δ belongs to a finite adversarial set Δ . This set is finite at the abstraction level and conservatively indexes all abstract successor cells induced by every admissible continuous exogenous signal ϑ , uncertain parameter, and discretization over-approximation over one sampling interval. It is not an arbitrary finite sample of a continuous disturbance set. Replacing a continuous disturbance set by finitely many extremal modes is sound only under an additional dominance property, such as disturbance-state monotonicity. Definition 1 (Componentwise order). We equip the state grid with the componentwise order: x⪯yx y if and only if xj≤yjx_j≤ y_j for all j∈1,…,dj∈\1,…,d\. When partial orders on U and Δ are used, they are denoted by ⪯ _U and ⪯Δ _ . Assumption 1 (Finite grid abstraction). The abstract state space is the finite partially ordered set X=1,…,N1×⋯×1,…,Nd,X=\1,…,N_1\×·s×\1,…,N_d\, with the componentwise order of Definition 1. We write N:=maxjNjN:= _jN_j and |X|=∏jNj|X|= _jN_j. Definition 2 (Lower set and antichain basis). For S⊆XS X, define its downward closure by ↓S:=q∈X:∃s∈S such that q⪯s. S:=\q∈ X:∃\,s∈ S such that q s\. A set K⊆XK X is a lower set if q∈Kq∈ K and q′⪯q q imply q′∈Kq ∈ K. Its antichain basis is the set of its maximal elements: Bas(K)≔q∈K:∄q′∈K∖q,q⪯q′. (K) \q∈ K: \,q ∈ K \q\,\;q q \. A lower set K is fully determined by its basis: K=↓Bas(K)K= (K). Remark 1 (Antichain bound). On the grid of Assumption 1, the maximal antichain size is bounded by O(Nd−1)O(N^d-1); every lower set therefore admits a basis of size at most O(Nd−1)O(N^d-1), one order of magnitude smaller than |X|=O(Nd)|X|=O(N^d). I-B Monotone dynamics and the robust controlled pre-operator Definition 3 (Restricted robust controlled predecessor). For A,B⊆XA,B X and V⊆V , define Pre(A,V,B):=q∈A:∃u∈V∀δ∈Δ,F(q,u,δ)∈B. [rgb]0,0,0 (A,V,B):=\q∈ A:∃ u∈ V\ ∀δ∈ ,\,F(q,u,δ)∈ B\. (3) For the safety iteration, define Φ(K):=Pre(K,,K), (K):= (K,U,K), which extracts from K those states that can be kept in K for one step despite the disturbances. Definition 4 (Controlled invariant set). A subset K⊆XSK X_S is controlled invariant (with respect to system (2) and safe set XSX_S) if for every x∈Kx∈ K, there exists u∈u such that F(x,u,δ)∈KF(x,u,δ)∈ K for all δ∈Δδ∈ . Equivalently, K=Φ(K)K= (K). Assumption 2 (Lower-closed safety). The safe state set XS⊆X_S X is a lower set under ⪯ . Definition 5 (State-monotonicity (SM)). The abstract transition map (2) is state-monotone if x1⪯x2⟹F(x1,u,δ)⪯F(x2,u,δ)x_1 x_2 F(x_1,u,δ) F(x_2,u,δ) for all u∈u and all δ∈Δδ∈ . Remark 2 (Stronger monotonicity variants). Reference [7] also equips the control set U and/or the disturbance set Δ with partial orders to define control-state monotone (CSM), disturbance-state monotone (DSM), and control-disturbance-state monotone (CDSM) systems. The correctness results below require only state monotonicity (SM). When the stronger variants hold, they allow the predecessor check to be restricted to minimal controls, maximal adversarial modes, or both. Proposition 1 (Lower-closed predecessor). [4, § 4.1, Lemma 2] Suppose Assumptions 1 and 2 hold and F is state-monotone (Definition 5). Then Φ(K) (K) is a lower set for every lower set K⊆XK X. Proof. Let x∈Φ(K)x∈ (K) and y⪯xy x. Since x∈Kx∈ K and K is lower, y∈Ky∈ K. Choose u∈u such that F(x,u,δ)∈KF(x,u,δ)∈ K for all δ∈Δδ∈ . By state monotonicity, F(y,u,δ)⪯F(x,u,δ)∈K∀δ∈Δ.F(y,u,δ) F(x,u,δ)∈ K ∀\,δ∈ . Lower-closedness of K then gives F(y,u,δ)∈KF(y,u,δ)∈ K for all δ, hence y∈Φ(K)y∈ (K). ∎ Corollary 1 (Ordered reductions). [7, § 5, Thm. 1 and Prop. 2] Let K⊆XK X be a lower set and let x∈Kx∈ K. If the stronger CSM variant of Remark 2 holds, then it is enough to test minimal controls: x∈Φ(K)⇔∃u∈Min()∀δ∈Δ:F(x,u,δ)∈K. [rgb]0,0,0x∈ (K) ∃\,u (U)\ ∀\,δ∈ :\ F(x,u,δ)∈ K. If the stronger DSM variant holds, then for every fixed u∈u it is enough to test maximal adversarial modes: x∈Φ(K)⇔∃u∈∀δ∈Max(Δ):F(x,u,δ)∈K. [rgb]0,0,0x∈ (K) ∃\,u \ ∀\,δ ( ):\ F(x,u,δ)∈ K. If the CDSM variant holds, one may therefore test only minimal controls against maximal adversarial modes. Let C denote the per-state successor-evaluation count for testing x∈Φ(K)x∈ (K). In the general state-monotone case, C=|||Δ|C=|U|\,| |. The ordered reductions [7] give CCSM=|Min()||Δ|,CDSM=|||Max(Δ)|,C_CSM=|Min(U)|\,| |, C_DSM=|U|\,|Max( )|, and CCDSM=|Min()||Max(Δ)|.C_CDSM=|Min(U)|\,|Max( )|. Theorem 1 (Descending predecessor sequence). Suppose Assumptions 1 and 2 hold and F is state monotone. Define K0:=XS,Ki+1:=Φ(Ki),i∈ℕ.K_0:=X_S, K_i+1:= [rgb]0,0,0 (K_i), i . Then each KiK_i is a lower set, the sequence is descending, and it converges in finitely many steps to a lower set K∗⊆XSK_* X_S which is the maximal robust controlled invariant subset of XSX_S. Proof. Proposition 1 gives lower-closedness of each KiK_i by induction. Since Φ(K)⊆K (K) K for every K, the sequence is descending. Because X is finite, the descending sequence converges after finitely many strict inclusions. If K⊆XSK X_S is a controlled invariant set, then K⊆K0K K_0. Assume inductively that K⊆KiK K_i. Since K⊆Φ(K)K (K) and the map Φ is monotone with respect to set inclusion, K⊆Φ(K)⊆Φ(Ki)=Ki+1.K (K) (K_i)=K_i+1. Hence K⊆KiK K_i for all i, and therefore K⊆K∗K K_*. Thus K∗K_* is the maximal robust controlled invariant subset of XSX_S. ∎ I-C Lazy fixed-point iteration Proposition 1 together with Remark 1 means that K∗K_* and every iterate KiK_i can be represented by its O(Nd−1)O(N^d-1)-size antichain basis rather than by the full O(Nd)O(N^d) grid. The lazy algorithm of [2], summarized in Algorithm 1, exploits this by storing only the current basis B and updating it. Let RlazyR_lazy denote the number of complete outer basis passes until convergence and |B|=O(Nd−1)|B|=O(N^d-1) denote the basis-size bound. If the membership query “x∈↓Bx∈ B” scans B, the safety-check phase costs O(RlazyCN2(d−1))O(R_lazyCN^2(d-1)), up to dimension factors. Neighbor generation performs dominance rather than successor queries and contributes O(RlazyN2(d−1))O(R_lazyN^2(d-1)) with the same scan-based representation. Since an unsafe basis element is removed and neighbors are inserted immediately, subsequent safety and neighbor checks use an evolving B and are sequential across basis updates. For a removed element b, the explicit update in Algorithm 1 implements Bas(↓B∖b) ( B \b\) from [2]. Algorithm 1 Lazy fixed point iteration [2] 1: Lower set XSX_S, transition F, inputs U, adversarial set Δ 2: B←Bas(XS)B← (X_S) 3: repeat 4: Bpass←B_pass← B 5: Bu←∅B_u← 6: for all b∈Bpassb∈ [rgb]0,0,0B_pass do ⊳ safety check 7: if ∄u∈ \,u s.t. ∀δ∈Δ:F(b,u,δ)∈↓B∀\,δ∈ :\ F(b,u,δ)∈ B then 8: Bu←Bu∪bB_u← B_u∪\b\ 9: B←B∖bB← B \b\ 10: for all j∈1,…,dj∈\1,…,d\ do ⊳ neighbor gen. 11: c←b−ejc← b-e_j 12: if cj≥1c_j≥ 1 and c∉↓Bc∉ B then 13: B←B∪cB← B∪\c\ 14: until Bu=∅B_u= 15: return ↓B B I Threshold-function iteration Section I-A introduces the threshold-function representation of lower sets. Section I-B reformulates one GFP step as a parallel collection of binary searches. Section I-C shows equivalence with Algorithm 1 and analyzes complexity. I-A The threshold-function representation The main idea is to project a d-dimensional lower set K⊆XK X into a (d−1)(d-1)-dimensional table using a designated axis. Definition 6 (Designated axis, projection, threshold function). Fix a designated axis d∗∈1,…,dd^*∈\1,…,d\ and set :=∏j≠d∗1,…,Nj.K\;:=\; _j≠ d^*\1,…,N_j\. For x∈Xx∈ X let π(x)∈π(x) be its projection onto the remaining d−1d-1 axes, and write xd∗x_d^* for its coordinate along d∗d^*. For a lower set K⊆XK X, the threshold function is τK(k):=maxxd∗:x∈K,π(x)=k,k∈, _K(k)\;:=\; \x_d^*:x∈ K,\ π(x)=k \, k , (4) with the convention max∅=0 =0. Each k∈k indexes a one-dimensional column of cells along the designated axis; lower-closedness forces the safe cells in that column to form a contiguous prefix 1,…,τK(k)\1,…, _K(k)\. The function τK _K therefore stores the entire set K in a single integer per column as depicted in Figure 1. Proposition 2 (Threshold characterization). Let K⊆XK X be a lower set. Then x∈K⇔xd∗≤τK(π(x)).x∈ K\; \;x_d^*≤ _K(π(x)). Moreover, τK _K is antitone: k⪯k′k k implies τK(k)≥τK(k′) _K(k)≥ _K(k ). Proof. If x∈Kx∈ K, the value xd∗x_d^* is one of the values maximized in (4) at k=π(x)k=π(x), so τK(π(x))≥xd∗ _K(π(x))≥ x_d^*. Conversely, if xd∗≤τK(π(x))x_d^*≤ _K(π(x)), pick y∈Ky∈ K with π(y)=π(x)π(y)=π(x) and yd∗=τK(π(x))y_d^*= _K(π(x)); then x⪯yx y and lower-closedness gives x∈Kx∈ K. Antitonicity follows by the same lifting: for k⪯k′k k , any x∈Kx∈ K with π(x)=k′π(x)=k and xd∗=vx_d^*=v dominates y with π(y)=k,yd∗=vπ(y)=k,\ y_d^*=v, hence y∈Ky∈ K and τK(k)≥v _K(k)≥ v. ∎ Remark 3 (Memory and query complexity). τK _K has ||=∏j≠d∗Nj=O(Nd−1)|K|= _j≠ d^*N_j=O(N^d-1) entries. Storage is O(Nd−1)O(N^d-1) and every inclusion query is O(1)O(1) (one projection and one comparison), compared to O(Nd−1)O(N^d-1) for a scan-based basis check. key kkheight vτK(k) _K(k)K(a) Threshold representation 1122334455667788τ(k)τ(k)prefixf(k)f(k)(b) Column update Fig. 1: Threshold representation and update. (a) A lower set K is stored by the column height τK(k) _K(k), so membership is the O(1)O(1) test (k,v)∈K⇔v≤τK(k)(k,v)∈ K v≤ _K(k). (b) For each column, Φ(K) (K) is a prefix whose height f(k)f(k) is found by binary search; all columns are updated independently. I-B The threshold iteration The representation of Section I-A turns one GFP step into a set of independent binary searches along the designated axis. We first state the structural property that enables this (Lemma 1), then derive the per-column update (Corollary 2). Definition 7 (Grid column). For k∈k , the column at k is Col(k):=(k,v):v∈1,…,Nd∗Col(k):=\(k,v):v∈\1,…,N_d^*\\. Lemma 1 (Column-wise predecessor prefix). If K⊆XK X is a lower set and (k,v)∈Φ(K)(k,v)∈ (K), then (k,v′)∈Φ(K)(k,v )∈ (K) for every v′∈1,…,vv ∈\1,…,v\. Proof. Let u∈u be a witness for (k,v)∈Φ(K)(k,v)∈ (K), so F((k,v),u,δ)∈KF((k,v),u,δ)∈ K for every δ∈Δδ∈ . Since (k,v′)⪯(k,v)(k,v ) (k,v), monotonicity yields F((k,v′),u,δ)⪯F((k,v),u,δ)∈KF((k,v ),u,δ) F((k,v),u,δ)∈ K, and lower-closedness of K gives F((k,v′),u,δ)∈KF((k,v ),u,δ)∈ K. Hence (k,v′)∈Φ(K)(k,v )∈ (K). ∎ Lemma 1 says that, within any column, the set of states from which K can be maintained is a contiguous prefix (k,1),…,(k,f(k))\(k,1),…,(k,f(k))\. This height is efficiently computable: Corollary 2 (Per-column threshold update). Let K⊆XK X be lower with threshold function τ=τKτ= _K. For each k∈k , define f(k):=max f(k):= \ v∈1,…,τ(k):∃u∈∀δ∈Δ, v∈\1,…,τ(k)\:\ ∃\,u \ ∀\,δ∈ , (5) F((k,v),u,δ)∈K, F((k,v),u,δ)∈ K \, with max∅:=0 :=0. Then Φ(K)∩Col(k)=(k,1),…,(k,f(k)). [rgb]0,0,0 (K) (k)=\(k,1),…,(k,f(k))\. Moreover, f(k)f(k) can be computed by binary search over 1,…,τ(k)\1,…,τ(k)\. Each probe requires one membership query in K per pair (u,δ)(u,δ), so the cost per column is O(ClogN).O\! (C\, N ). Proof. By Lemma 1, Φ(K)∩Col(k) (K) (k) is a prefix of Col(k)Col(k) of length equal to (5) and the predicate in (5) is monotone non-increasing in v, so a standard binary search over 1,…,τ(k)\1,…,τ(k)\ locates f(k)f(k) in O(logN)O( N) probes. ∎ Since the update τ(k)←f(k)τ(k)← f(k) is independent across columns, all columns can be processed in parallel as in Figure 1. The full iteration is summarized in Algorithm 2. Algorithm 2 Threshold-function iteration Lower set XSX_S, transition F, inputs U, adversarial set Δ , designated axis d∗d^* τ←τXSτ← _X_S repeat for all k∈k do ⊳ all columns are independent f(k)←BinSearch(k,τ,F,,Δ)f(k)← BinSearch(k,τ,F,U, ) ⊳ using (5) τ←fτ← f until τ unchanged return Kτ=x∈X:xd∗≤τ(π(x))K_τ=\x∈ X:x_d^*≤τ(π(x))\ I-C Correctness, convergence, and complexity We now prove that Algorithm 2 computes the same invariant set as Algorithm 1. Theorem 2 (One-step equivalence). Let K⊆XK X be a lower set with threshold τ=τKτ= _K, and let f be defined by (5). Then, Assumption 1 and state monotonicity (Definition 5) imply: Φ(K)=x∈X:xd∗≤f(π(x)),i.e.f=τΦ(K). [rgb]0,0,0 (K)\;=\; \x∈ X:x_d^*≤ f(π(x)) \,\ i.e.\ f= _ (K). Proof. By Corollary 2, Φ(K)∩Col(k)=(k,1),…,(k,f(k)) (K) (k)=\(k,1),…,(k,f(k))\ for every k∈k ; taking the union over k gives Φ(K)=x:xd∗≤f(π(x)) (K)=\x:x_d^*≤ f(π(x))\. Combining this with Proposition 2 yields f=τΦ(K)f= _ (K). ∎ Corollary 3 (Correctness and convergence of Algorithm 2). Let τ0:=τXS _0:= _X_S and, for each i∈ℕi , let τi+1 _i+1 be obtained from τi _i by the update (5). Define Ki:=x∈X:xd∗≤τi(π(x)).K_i:=\x∈ X:x_d^*≤ _i(π(x))\. Then K0=XSK_0=X_S, each KiK_i is a lower set, and Ki+1=Φ(Ki)∀i∈ℕ.K_i+1= [rgb]0,0,0 (K_i) ∀\,i . The sequence (Ki)i∈ℕ(K_i)_i is descending and converges in finitely many steps to the maximal robust controlled invariant subset K∗K_* of XSX_S. Equivalently, Algorithm 2 returns K∗K_*. Proof. The identity K0=XSK_0=X_S follows from the definition of τXS _X_S together with Proposition 2. Since XSX_S is a lower set and Theorem 2 maps the threshold of a lower set to the threshold of its predecessor, each KiK_i is a lower set and satisfies Ki+1=Φ(Ki)K_i+1= (K_i). The conclusion now follows from Theorem 1. ∎ Theorem 3 (Equivalence with the lazy basis formulation). Let KlazyK^lazy denote the set returned by Algorithm 1 and let KthrK^thr denote the set returned by Algorithm 2, both started from the same lower set XSX_S. Then Klazy=Kthr=K∗.K^lazy=K^thr=K_*. Proof. By Corollary 3, Algorithm 2 returns the maximal robust controlled invariant subset K∗K_* of XSX_S. By the completeness result for the lazy algorithm in [2], Algorithm 1 returns the same maximal invariant set. ∎ The threshold iteration replaces quadratic lazy boundary work with one embarrassingly parallel stage; see Table I. TABLE I: Per-iteration complexity comparison. Lazy [2] Threshold (ours) Predecessor tests O(CN2(d−1))O(CN^2(d-1)) O(CNd−1logN)O(CN^d-1 N) sequential over evolving B parallel over columns Basis update O(N2(d−1))O(N^2(d-1)) — sequential — Remark 4 (Dense storage and designated-axis choice). Let Md∗:=∏j≠d∗NjM_d^*:= _j≠ d^*N_j. A threshold buffer stores Md∗M_d^* values regardless of frontier complexity, whereas a sparse basis stores |B||B| maximal grid points and may require substantially less memory when |B|≪Md∗|B| M_d^*. The threshold representation is attractive for dense or irregular frontiers and workloads dominated by membership queries. Memory can be minimized by choosing an axis with maximal Nd∗N_d^*. IV Experiments We evaluate threshold iteration on three d=3d=3 benchmarks and a d=5d=5 benchmark from the monotone-synthesis literature. ACC — adaptive cruise control [2]. The 3D state is (h,ve,vℓ)(h,v_e,v_ ) (headway, ego speed, lead speed), with ego torque command u and adversarial mode δ that captures lead-vehicle braking and parameter uncertainty. The ACC dynamics are h˙=vℓ−ve,v˙e=ae(ve,u,δ),v˙ℓ=aℓ(vℓ,δ). h=v_ -v_e, v_e=a_e(v_e,u,δ), v_ =a_ (v_ ,δ). ACC-5D uses state (h,ve,vℓ,Te,Tℓ)(h,v_e,v_ ,T_e,T_ ), replaces direct torque arguments by actuator states in ae,aℓa_e,a_ , and adds T˙e=(u−Te)/τe,T˙ℓ=(δT−Tℓ)/τℓ T_e=(u-T_e)/ _e,\ T_ =( _T-T_ )/ _ . The acceleration model is a(v,T,θ)=1M(TRw−α)−βMv−γMv2,a(v,T,θ)= 1M\! ( TR_w-α )- βMv- γMv^2, (6) where θ=(M,Rw,α,β,γ)∈Θθ=(M,R_w,α,β,γ)∈ . The safe set is KACC=(h,ve,vℓ):h≥db(ve)K_ACC=\(h,v_e,v_ ):h≥ d_b(v_e)\, where dbd_b is the worst-case braking-distance map. We use the orthant order x⪯ACCy⇔hx≥hy,ve,x≤ve,y,vℓ,x≥vℓ,y,x _ACCy h_x≥ h_y,\ v_e,x≤ v_e,y,\ v_ ,x≥ v_ ,y, and, for ACC-5D, additionally Te,x≤Te,yT_e,x≤ T_e,y and Tℓ,x≥Tℓ,yT_ ,x≥ T_ ,y. KACCK_ACC is lower-closed whenever dbd_b is nondecreasing. Turn-Ego/Turn-Oncoming. Both unprotected-turn benchmarks [10] use state (se,ve,so)(s_e,v_e,s_o): ego longitudinal position and speed, plus oncoming longitudinal position along the opposing lane centerline. There is no exogenous disturbance channel, so we use a singleton adversarial set. The dynamics are s˙e=ve,v˙e=ae(ve,u),s˙o=vo. s_e=v_e, v_e=a_e(v_e,u), s_o=v_o. -2.84544pt Let Z(s):=1+s≥−10+s≥10Z(s):=1+1_\s≥-10\+1_\s≥ 10\ be the shared zone map and write Ze:=Z(se),Zo:=Z(so)Z_e:=Z(s_e),\ Z_o:=Z(s_o). Both benchmarks use the same unprotected-turn geometry for opposite maneuvers: Turn-Oncoming models the ego waiting while the oncoming car passes, Turn-Ego models the ego passing first; the orthant order is flipped between them, thus the ego-priority and oncoming-priority safe sets are Kego K_ego =x∈Xturn:¬(Ze<Zo∨(Ze=2∧Zo=2)), =\x∈ X_turn: (Z_e<Z_o (Z_e=2 Z_o=2))\, Konc K_onc =x∈Xturn:¬(Zo<Ze∨(Ze=2∧Zo=2)). =\x∈ X_turn: (Z_o<Z_e (Z_e=2 Z_o=2))\. They forbid simultaneous conflict-zone occupation while enforcing the chosen priority relation. The orthant orders are x⪯Ey⇔se,x≥se,y,ve,x≥ve,y,so,x≤so,y, x _Ey s_e,x≥ s_e,y,\ v_e,x≥ v_e,y,\ s_o,x≤ s_o,y, x⪯Oy⇔se,x≤se,y,ve,x≤ve,y,so,x≥so,y. x _Oy s_e,x≤ s_e,y,\ v_e,x≤ v_e,y,\ s_o,x≥ s_o,y. Minimal controls are maximum torque for ⪯E _E and minimum torque for ⪯O _O. Since Z is monotone, moving downward under ⪯E _E advances ego and delays the oncoming phase, while downward movement under ⪯O _O has the reverse effect; thus, priority constraints are lower-closed, and monotonicity follows from the dynamics’ sign structure [10]. IV-A Lazy vs. threshold comparison For fair comparison, we also introduce a stronger Lazy+τ baseline which preserves Algorithm 1’s traversal and immediate-deletion schedule while maintaining the exact threshold table τ↓B _ B. Deleting an uncontrolled maximal element b updates τ(π(b))←τ(π(b))−1τ(π(b))←τ(π(b))-1. A neighbor c=b−ejc=b-e_j is maximal when c∈Kτc∈ K_τ and every valid immediate successor c+eℓ∉Kτc+e_ ∉ K_τ, which is checked using threshold queries. Thus, Lazy+τ changes the representation and boundary-maintenance operations while retaining the sequential Lazy schedule; the basis is materialized after each pass. Table I compares scan-based Lazy, Lazy+τ, and threshold GFP. The two Lazy methods use the same pass, immediate-deletion schedule, and the same precomputed successor cache. The time required to construct this cache is reported as tpret_ pre. The implementation and experiment configurations are publicly available. 11 1 https://github.com/mkhaled87/pFaces-MonoSynth The threshold method uses inline dynamics: a full successor table would cost O(C|X|)O(C|X|) memory and becomes the bottleneck at larger grids, while threshold membership needs only the O(Nd−1)O(N^d-1) table and eliminates antichain maintenance. At |X|=109|X|=10^9, the threshold iteration is already thousands of times faster; at |X|≥1010|X|≥ 10^10 the basis method exceeds the time or memory budget, but the threshold iteration completes. Let RthrR_thr denote the number of threshold rounds. A threshold round computes one full Φ(K) (K) update over all columns, whereas a lazy pass incrementally mutates the exposed antichain boundary. Thus, RlazyR_lazy and RthrR_thr are algorithm-specific round counts and are not comparable. Experiments were run on an NVIDIA RTX 5090 GPU (32 GB, 170 SMs) with an AMD Ryzen 9 9950X3D CPU. We implement the method in C++/pFaces [11] with OpenCL kernels. Each key k∈k evaluates predecessor feasibility and updates τ(k)τ(k) by binary search. Memory is dominated by τ∈ℕ||τ ^|K| with ||=O(Nd−1)|K|=O(N^d-1). TABLE I: Lazy vs. Threshold Comparison. tpret_ pre is the successor-table generation time used in Lazy methods and is excluded from the reported speedups, which equal tlazy+τ/tthrt_ lazy+τ/t_ thr; R = iterations; timeout = 20 minutes. Case |X||X| tpret_ pre Lazy Threshold RlazyR_ lazy tlazyt_ lazy tlazy+τt_ lazy+τ RthrR_ thr tthrt_ thr Speedup ACC 10610^6 .569ms.569\,ms 182 63.1s63.1\,s 106ms106\,ms 26 3.18ms3.18\,ms 33.4×33.4× ACC 10910^9 439ms439\,ms 1595 Timeout 126s126\,s 24 16.9ms16.9\,ms 7,458×7,458× ACC 101010^10 Timeout 24 318ms318\,ms - ACC 101210^12 Timeout 24 750ms750\,ms - ACC 101410^14 Timeout 24 7.94s7.94\,s - ACC-5D 10610^6 .624ms.624\,ms 318 299s299\,s 457ms457\,ms 25 3.34ms3.34\,ms 137×137× ACC-5D 10910^9 470ms470\,ms 835 Timeout 410s410\,s 31 143ms143\,ms 2,870×2,870× ACC-5D 101110^11 Timeout 28 4.94s4.94\,s - T-Ego 10610^6 1.35ms1.35\,ms 278 329s329\,s 269ms269\,ms 22 10.8ms10.8\,ms 24.9×24.9× T-Ego 10910^9 1.18s1.18\,s 2691 Timeout 341s341\,s 26 41.6ms41.6\,ms 8,188×8,188× T-Ego 101010^10 Timeout 26 274ms274\,ms - T-Ego 101210^12 Timeout 26 3.18s3.18\,s - T-Ego 101410^14 Timeout 26 70.0s70.0\,s - T-Onc 10610^6 .563ms.563\,ms 273 118s118\,s 173ms173\,ms 35 4.22ms4.22\,ms 41.0×41.0× T-Onc 10910^9 458ms458\,ms 2462 Timeout 185s185\,s 35 26.4ms26.4\,ms 6,993×6,993× T-Onc 101010^10 Timeout 35 123ms123\,ms - T-Onc 101210^12 Timeout 34 960ms960\,ms - T-Onc 101410^14 Timeout 35 19.2s19.2\,s - IV-B Real-time controller: unprotected left turn To demonstrate online use of the synthesized invariant sets, we employ the threshold method inside an MPPI [12] controller for an unprotected left turn (Figure 2). The ego vehicle approaches the intersection from the west while two oncoming vehicles approach from the east. Their velocities are sensed online. The ego first waits for onc1onc_1 to clear the conflict zone, then commits to the turn before onc2onc_2 closes the available gap. Each phase is formulated as a 3D robust-safety problem in (se,ve,sonc)(s_e,v_e,s_onc), and the corresponding invariant set is re-synthesized when the sensed oncoming speed changes sufficiently. Let Kw⊆ℝ3K_w ^3 and Kg⊆ℝ3K_g ^3 be the two phase sets. The two-oncoming safety condition is represented by the intersection of these two 3D constraints in lifted coordinates: K2=(se,ve,s1,s2):(se,ve,s1)∈Kw,(se,ve,s2)∈Kg.K_2=\(s_e,v_e,s_1,s_2):\ (s_e,v_e,s_1)∈ K_w,\\ (s_e,v_e,s_2)∈ K_g\. This lifted set is used only for online rollout membership queries; we do not claim that the full 4D system is monotone or that K2K_2 is a 4D controlled-invariant set. The reduction is sound for simultaneously checking the two phase certificates under the modeled independent oncoming evolution. A formal 4D invariance claim would additionally require a common witness input for both component constraints, which need not exist because the wait and go constructions impose opposite orthant orders on (se,ve)(s_e,v_e). conflict zoneegoonc1v→onc,1 v_onc,1onc2v→onc,2 v_onc,2 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. The invariant-set algorithm returns K∗K_*, not an explicit policy. In closed loop, we use K∗K_* inside an optimizer: the threshold table gives an O(1)O(1) membership query that is easy to insert into a sampling-based MPPI cost. MPPI is a natural choice here because it handles nonlinear dynamics and nonsmooth table penalties without requiring gradients of the threshold representation; first-order MPC methods would need smoothing of the same discontinuous membership test. Let TsT_s denote the controller sampling period, HpH_p the prediction horizon, HcH_c the control horizon, NrN_r the number of rollouts per MPPI iteration, NitN_it the number of MPPI updates per control step, σu _u the standard deviation of the Gaussian input perturbations, and [umin,umax][u_ ,u_ ] the admissible torque interval. Their numerical values are reported in Table I. The stage cost is ℓ(xk,uk)=wp(se,k−g)2+wsxk∉K2+wj∥uk−uk−1∥2 (x_k,u_k)=w_p(s_e,k-g)^2+w_s1_\x_k∉ K_2\+w_j\|u_k-u_k-1\|^2. Each table is computed for the oncoming-speed parameters and interval vehicle parameters, and re-synthesis is triggered when the sensed velocity change exceeds the threshold εres _res listed in Table I. The safety-informed MPPI performs an O(1)O(1) threshold lookup per rollout step; states outside K2K_2 accumulate a penalty wsw_s, rather than being prohibited by a hard constraint, and the implemented controller provides no formal closed-loop safety guarantee. Such a guarantee would require a hard one-step invariant constraint or an invariant-preserving backup policy, which is left for future work. The threshold lookup and MPPI control computation times are negligible relative to the re-synthesis times. TABLE I: Real-time unprotected left turn: configuration and timings. Quantity Value Grid cells |X||X| 1010=104×102×10410^10=10^4× 10^2× 10^4 Sampling period TsT_s 0.10.1 s Prediction and control horizon Hp,HcH_p,H_c 2020 steps MPPI iterations / step NitN_it 1010 Rollouts / iteration NrN_r 512512 Perturbation standard deviation σu _u 10001000 Nm Cost weights (wp,ws,wj)(w_p,w_s,w_j) (1,104,10−2)(1,10^4,10^-2) Resynthesis threshold εres _res 0.20.2 m/s Wait and go synthesis twait,tgot^wait,t^go 77±15,62±7ms77± 15,62± 7\,ms Average MPPI control time 22 ms V Conclusion We introduced a threshold-function reformulation of greatest-fixed-point invariant-set synthesis for monotone systems. The algorithm is embarrassingly parallel and orders of magnitude faster than lazy fixed-point iteration. Experiments on benchmarks confirm speedups on the order of thousands over the lazy baseline. The threshold iteration reaches grids exceeding 10910^9 cells around 100 ms, enabling real-time re-synthesis for closed-loop control. However, the method requires monotonicity under some orthant order and lower-closedness of the safety set. The threshold table stores only the set and gives no specific control policy. Grid resolution is bounded by GPU memory (O(Nd−1)O(N^d-1) integers). References [1] P. Tabuada, Verification and control of hybrid systems: a symbolic approach. Springer Science & Business Media, 2009. [2] A. Saoud, E. Ivanova, and A. Girard, “Efficient synthesis for monotone transition systems and directed safety specifications,” in IEEE Conference on Decision and Control. IEEE, 2019, p. 6255–6260. [3] E. Ivanova and A. Girard, “Lazy safety controller synthesis with multi-scale adaptive-sampling abstractions of nonlinear systems,” IFAC-PapersOnLine, vol. 53, no. 2, p. 1837–1843, 2020. [4] E. Ivanova, A. Saoud, and A. Girard, “Lazy controller synthesis for monotone transition systems and directed safety specifications,” Automatica, vol. 135, p. 109993, 2022. [5] E. S. Kim, M. Arcak, and S. A. Seshia, “Symbolic control design for monotone systems with directed specifications,” Automatica, vol. 83, p. 10–19, 2017. [6] —, “Flexible computational pipelines for robust abstraction-based control synthesis,” in International Conference on Computer Aided Verification. Springer, 2019, p. 591–608. [7] A. Saoud and M. Arcak, “Characterization, verification and computation of robust controlled invariants for monotone dynamical systems,” Mathematics of Control, Signals, and Systems, vol. 36, p. 71–100, 2024. [8] M. Rungger and M. Zamani, “SCOTS: A tool for the synthesis of symbolic controllers,” in Proceedings of the 19th international conference on hybrid systems: Computation and control, 2016, p. 99–104. [9] Y. Li and J. Liu, “ROCS: A robustly complete control synthesis tool for nonlinear dynamical systems,” in 21st International Conference on Hybrid Systems: Computation and Control, 2018, p. 130–135. [10] S. W. Smith, A. Saoud, and M. Arcak, “Monotonicity-based symbolic control for safety in driving scenarios,” IEEE Control Systems Letters, vol. 6, p. 830–835, 2021. [11] M. Khaled and M. Zamani, “pFaces: An acceleration ecosystem for symbolic control,” in 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019, p. 252–257. [12] G. Williams, N. Wagener, B. Goldfain, P. Drews, J. M. Rehg, B. Boots, and E. A. Theodorou, “Information theoretic MPC for model-based reinforcement learning,” in 2017 IEEE international conference on robotics and automation (ICRA). IEEE, 2017, p. 1714–1721.