ReLU Barrier Functions for Nonlinear Systems with Constrained Control: A Union of Invariant Sets Approach

1. Problem Statement

The paper addresses the challenge of certifying safety for nonlinear control-affine systems subject to polytopic input constraints (e.g., actuator saturation).

• Core Difficulty: Designing Control Barrier Functions (CBFs) for such systems is computationally intractable because the synthesis problem becomes nonconvex when input constraints are present.
• Limitations of Existing Methods:
  • Linear $\alpha(\cdot)$: Standard approaches often use a linear extended class-$\mathcal{K}$ function $\alpha(\cdot)$ to maintain convexity. However, this introduces significant conservatism, resulting in smaller certified safe sets.
  • Neural CBFs: While neural networks can approximate complex dynamics, training them typically involves nonconvex optimization with expensive verification, and they often lack systematic mechanisms to enlarge invariant sets under saturation.
  • Prior Work: The authors' previous work [12] handled Piecewise Affine (PWA) systems with saturation but was restricted to linear $\alpha(\cdot)$ and PWA dynamics only.

Goal: Synthesize a CBF for nonlinear systems under input constraints that reduces conservatism (enlarges the safe set) while preserving convex synthesis and ensuring rigorous safety guarantees.

---

2. Methodology

The authors propose an Approximation–Verification Pipeline that bridges convex optimization on surrogate models with rigorous verification on the original nonlinear system. The process consists of five key steps:

A. Surrogate Modeling (Approximation)

Instead of synthesizing directly on the nonlinear system, the closed-loop dynamics are approximated by a Piecewise Affine (PWA) surrogate model. This is achieved using a ReLU neural network, leveraging the mathematical equivalence between ReLU networks and continuous PWA functions.

B. Leaky ReLU Surrogate for $\alpha(\cdot)$

To reduce conservatism without sacrificing convexity, the paper introduces a two-slope Leaky ReLU function as a surrogate for the extended class-$\mathcal{K}$ function $\alpha(\cdot)$:
$$\alpha(s) = \begin{cases} \alpha_m s & s \ge 0 \\ \alpha_1 s & s < 0 \end{cases}$$

• Theoretical Basis: Theorem 1 proves that any invariant set certifiable by a general $\alpha \in \mathcal{K}_\infty$ can also be certified by this two-slope Leaky ReLU.
• Benefit: This avoids the bilinear nonconvexity of arbitrary nonlinear $\alpha$ while allowing for steeper slopes (less conservatism) compared to a single linear slope.

C. Union of Invariant Sets (UIS)

To further enlarge the certified region, the authors introduce the Union of Invariant Sets (UIS) approach:

1. Multiple Syntheses: The optimization problem is solved multiple times using different linear slopes ($\alpha_i x$) from a grid.
2. Max-Composition: Instead of selecting the single largest set, the method constructs a new barrier function $h(x)$ as the maximum of the individual barrier functions:
   $$h(x) = \max_i \{ h^{(i)}(x) \}$$
3. Result: The union of the individual invariant sets is certified as forward-invariant. This yields a safe region that is never smaller than the best single linear choice and often significantly larger, without requiring additional optimization solves beyond the initial grid search.

D. Facet-wise Verification

Since the PWA surrogate is an approximation, the synthesized barrier must be verified against the original nonlinear dynamics.

• Strategy: The zero-level set of the max-composed barrier function is decomposed into a finite number of facet patches (linear regions).
• Verification: Using Farkas' Lemma, the CBF condition is checked locally on each facet patch. This eliminates the control input $u$ analytically, transforming the verification into a small, tractable nonlinear optimization problem for each patch.
• Efficiency: This approach avoids checking the entire domain, focusing only on the boundary where safety is critical.

E. Local Uncertainty Updates

If verification fails on a specific facet (a counterexample is found):

1. The deviation between the true dynamics and the surrogate is calculated at the counterexample point.
2. A local uncertainty set ($\Delta_j$) is added only to the specific cell containing the counterexample.
3. The convex program is re-solved with this localized robustification. This avoids the excessive conservatism of applying global uncertainty bounds to the entire system.

---

3. Key Contributions

1. Leaky ReLU Surrogate for $\alpha(\cdot)$: A novel two-slope design that reduces conservatism relative to linear $\alpha$ while maintaining the convexity of the synthesis problem.
2. Union of Invariant Sets (UIS): A method to combine multiple LP-based invariant sets via max-composition. It guarantees a certified region at least as large as the best single-$\alpha$ certificate, with no extra optimization cost.
3. Approximation–Verification Pipeline: A complete framework that performs convex synthesis on PWA surrogates and rigorously certifies the original nonlinear system through facet-wise verification and local uncertainty updates.
4. Scalability: The method supports parallelization (both UIS solves and facet verifications are independent), making it suitable for higher-dimensional systems.

---

4. Results and Simulations

The method was validated on three benchmarks with input saturation:

• Example 1: Inverted Pendulum

  • Setup: Nonlinear pendulum with saturated control.
  • Result: The UIS method produced a strictly larger invariant set than any single linear $\alpha$ design.
  • Time: Total certification time was 46 seconds (34s synthesis + 12s verification).

• Example 2: Nonlinear System (from literature)

  • Setup: A 2D nonlinear system where the goal is to avoid an unsafe set.
  • Comparison: Compared against a deep neural network approach (315+ seconds) and Sum-of-Squares (SOS) methods.
  • Result: The proposed method used a compact single-layer ReLU (20 neurons) and achieved a provably safe set strictly larger than single-$\alpha$ solutions and comparable to SyntheBC, but with significantly lower computation time (80 seconds).

• Example 3: Cart-Pole System

  • Setup: 4D nonlinear dynamics with input saturation.
  • Result: Successfully certified a large invariant set using the UIS approach with two slopes.
  • Time: Total time was 1466 seconds (1349s synthesis + 117s verification), demonstrating scalability to 4D systems.

Table I Summary: The paper demonstrates that while synthesis time scales with dimension, the UIS approach consistently yields larger safe sets than linear designs, and the verification step remains computationally manageable.

---

5. Significance

This paper makes a significant contribution to safe autonomous control by solving the trade-off between tractability (convexity) and conservatism (size of the safe set).

• Bridging Gaps: It effectively bridges the gap between the efficiency of convex optimization (typically limited to linear or PWA systems) and the complexity of nonlinear dynamics with constraints.
• Practicality: By using local uncertainty updates rather than global bounds, the method avoids the "curse of conservatism" that often renders safety certificates useless in practice.
• Future Impact: The framework provides a systematic way to enlarge certified regions without resorting to nonconvex training, making it highly applicable to robotics and autonomous driving where safety guarantees are paramount.