Safe and Robust Domains of Attraction for Discrete-Time Systems: A Set-Based Characterization and Certifiable Neural Network Estimation

This paper proposes a novel framework that characterizes safe and robust domains of attraction for discrete-time nonlinear uncertain systems using value functions on compact set metric spaces and leverages physics-informed neural networks with formal verification to provide certifiable estimates.

The Gist

Imagine you are driving a car on a winding mountain road. You want to know: "If I start driving from this specific spot, will I definitely reach the destination safely, even if the road is slippery, the wind is gusting, or I make a tiny mistake?"

In the world of engineering and robotics, this question is about finding the Domain of Attraction (DOA). It's the map of all the starting points where a system (like a drone, a power grid, or a self-driving car) is guaranteed to stay safe and eventually settle down, despite unexpected bumps and uncertainties.

This paper proposes a new, smarter way to draw that safety map for complex, unpredictable systems. Here is how they did it, broken down into simple concepts:

1. The Problem: The "Perfect World" Trap

Traditionally, engineers tried to draw these safety maps using rigid, pre-made shapes (like perfect circles or ellipses) or by assuming the world is "perfect" (no wind, no friction).

• The Flaw: Real life isn't perfect. If you design a safety map assuming no wind, but then a gust hits your drone, your "safe" map might actually lead you off a cliff.
• The Old Math: The math used to calculate these maps was either too slow (taking forever to compute) or too simple (ignoring the messy reality of uncertainty).

2. The New Idea: A "Smart GPS" for Safety

The authors created a new framework that acts like a Smart GPS. Instead of guessing the shape of the safe zone, they let a computer "learn" the shape by understanding the rules of the road.

They used three main ingredients:

A. The "Scorekeeper" (Value Functions)

Imagine a game where your goal is to reach a safe harbor (the destination).

• The authors invented a special Scorekeeper (called a Value Function).
• This Scorekeeper doesn't just look at where you are now; it looks at your entire future path.
• The Rule: If you are in a safe spot, your score is low. If you are in a dangerous spot or on a path that might lead to a crash, your score goes up.
• The Magic: They proved that if you can find a Scorekeeper that always goes down as you get closer to the harbor, you have found a safe zone.

B. The "Physics-Informed" Neural Network (The Learner)

Usually, AI (Neural Networks) learns by looking at millions of examples. But in safety-critical systems, you can't afford to make mistakes while learning.

• The Innovation: Instead of just feeding the AI data, they taught the AI the laws of physics directly.
• Think of it like teaching a student not just by showing them test answers, but by making them memorize the formulas that generate the answers.
• The AI is forced to follow the "Scorekeeper" rules (the Bellman equations) while it learns. This ensures the AI doesn't just guess; it understands the underlying logic of safety.

C. The "Safety Inspector" (Formal Verification)

Even a smart AI can make a tiny mistake. In engineering, "pretty sure" isn't good enough; you need "100% sure."

• After the AI learns the safety map, the authors use a Safety Inspector (a formal verification tool).
• This Inspector is like a super-rigid auditor. It checks every single point on the AI's map and mathematically proves: "Yes, if you start here, you will never crash, no matter what the wind does."
• If the AI claims a spot is safe but the Inspector finds a loophole, the map is shrunk until it is 100% certified.

3. The Analogy: The "Flooded Basement"

Imagine your house is in a valley, and you want to know which rooms will stay dry if a flood comes (the uncertainty).

• Old Way: You draw a circle around the living room and say, "If the water stays inside this circle, we are safe." But if the water flows in a weird shape, your circle is useless.
• This Paper's Way:
  1. You build a Smart Water Sensor (the Neural Network) that learns how water flows in your specific house.
  2. You force the sensor to obey the Laws of Water Flow (the Physics equations) so it doesn't hallucinate.
  3. You hire a Certified Engineer (the Verification Tool) to walk through every room the sensor marked as "dry" and mathematically prove that no water can ever get in, even if the flood is chaotic.

4. Why This Matters

The authors tested this on four different complex systems (like a power grid and a robotic arm).

• Result: Their method found larger safe zones than previous methods. This means we can drive faster, fly higher, or use more energy, knowing we are still safe.
• Robustness: It works even when the system is "wobbly" or the environment is unpredictable.
• Efficiency: It's fast enough to be useful, unlike older methods that would take days to compute.

Summary

This paper gives us a new toolkit to build safer, more reliable machines. It combines the flexibility of AI (to handle complex shapes) with the rigor of math (to guarantee safety) and the power of formal checking (to prove it works). It's like upgrading from a paper map that might be wrong, to a GPS that not only knows the road but has a lawyer on board to guarantee you won't get a ticket.

Technical Summary

1. Problem Statement

The paper addresses the challenge of estimating the Safe Robust Domain of Attraction (DOA) for discrete-time nonlinear uncertain systems.

• System Model: $x_{k+1} = f(x_k, w_k)$, where $x_k$ is the state, $w_k$ is a disturbance from a compact set $W$, and $f$ is continuous.
• Objective: Identify the set of initial states from which all trajectories are guaranteed to:
  1. Converge to a prescribed Robust Invariant Set (RIS), denoted as $A$.
  2. Satisfy state constraints (remain within an open safe set $X$) for all time steps and all admissible disturbance sequences.
• Challenges:
  • Existing methods often rely on fixed-form Lyapunov functions (e.g., quadratic), leading to conservative estimates.
  • Traditional grid-based solutions to Bellman equations are computationally expensive and suffer from the "curse of dimensionality."
  • Sum-of-Squares (SOS) methods are limited to polynomial systems.
  • Standard Neural Network (NN) approaches often lack formal guarantees regarding safety and robustness due to approximation errors and the difficulty of verifying set-valued dynamics.

2. Methodology

The authors propose a novel framework integrating set-based value functions, physics-informed neural networks, and formal verification.

A. Theoretical Foundation: Set-Based Value Functions

Instead of defining value functions on the state space $\mathbb{R}^n$, the authors define them on the metric space of compact sets $K(\mathbb{R}^n)$ equipped with the Hausdorff distance.

• Assumptions: The RIS $A$ is assumed to be uniformly locally $\ell_p$-stable. This is a general condition encompassing exponential and polynomial stability.
• Value Functions: Two functions are introduced:
  1. $V(X) = \sum_{k=0}^{\infty} \Psi(R(X, k))$, where $R(X, k)$ is the reachable set at time $k$, and $\Psi$ is a cost functional involving distance to $A$ and a barrier function for the safe set $X$.
  2. $W(X) = 1 - \exp(-V(X))$.
• Characterization: The safe robust DOA is exactly characterized as the sublevel set $\{x \mid W(\{x\}) < 1\}$.
• Bellman-Type Equations: The authors derive functional equations (Zubov-type) satisfied by these value functions:
  • $V(X) = \Psi(X) + V(F(X))$
  • $W(X) - W(F(X)) = \xi(X)(1 - W(F(X)))$
    These equations hold for set-valued arguments, where $F(X)$ represents the image of set $X$ under the uncertain dynamics.

B. Physics-Informed Neural Network (PINN) Framework

To approximate these value functions in high-dimensional spaces, the authors employ a neural network learning strategy:

• Embedding: Since the Bellman equation involves set-valued terms ($F(\{x\})$), an injective embedding $T$ is used to map singleton sets $\{x\}$ and reachable sets $F(\{x\})$ into a finite-dimensional vector space $\mathbb{R}^L$.
• Loss Function: The training minimizes a composite loss:
  • Data-Driven Loss: Minimizes the error between the NN output and a finite-horizon approximation of the ground-truth value function (computed via trajectory sampling).
  • Physics-Informed Loss: Minimizes the residual of the derived Bellman-type equation directly within the training loop. This enforces the structural properties of the value function without requiring labeled data for every point.
• Approximation: The reachable sets are approximated using a finite number of sampled disturbance trajectories.

C. Certifiable Verification

Since NN approximations introduce errors, a formal verification step is required to guarantee safety:

• Initial ROA: An initial safe region is established (e.g., via a quadratic Lyapunov function).
• Enlargement: The framework verifies conditions to expand this region. It checks if the learned NN function $\omega_{nn}$ satisfies:
  1. Safety: Trajectories starting in the estimated region remain within the safe set $X$.
  2. Convergence: The value function decreases along trajectories ($\omega_{nn}(f(x,w)) - \omega_{nn}(x) \leq -\epsilon$).
• Tools: The verification utilizes state-of-the-art formal verification tools like $\alpha,\beta$-CROWN and dReal to handle the non-convexity of neural networks and the nonlinearity of the system dynamics.

3. Key Contributions

1. Set-Based Characterization: Introduction of value functions defined on metric spaces of compact sets, allowing for an exact characterization of safe robust DOAs for general nonlinear systems with uncertainties and state constraints.
2. General Stability Assumptions: Relaxation of restrictive assumptions (e.g., Lipschitz continuity, bounded safe sets) by utilizing uniform $\ell_p$-stability, which covers a broader class of decay rates (polynomial and exponential).
3. Physics-Informed Learning: A novel training scheme that embeds the set-based Bellman equations directly into the NN loss function, enabling the learning of robust Lyapunov functions without fixed templates.
4. Certifiable Estimation: A rigorous verification procedure that bridges the gap between flexible NN approximations and formal safety guarantees, compatible with modern verification tools.
5. Scalability: The method avoids grid-based discretization, making it applicable to higher-dimensional systems where traditional methods fail.

4. Results

The methodology was validated on four numerical examples, including:

• A perturbed two-machine power system.
• An uncertain nonlinear system with local polynomial stability.
• A rigid rod with gravity and saturated torque.
• A perturbed rational system.

Key Findings:

• Performance: In scenarios accounting for full uncertainty (Scenario 2), the proposed framework consistently yielded the largest certifiable DOA estimates compared to:
  • Optimized ellipsoidal ROAs (Lyapunov-based).
  • Neural networks trained on nominal (unperturbed) dynamics.
• Robustness: Nominal-trained NNs failed to produce certifiable estimates for several uncertain examples, whereas the proposed robust framework succeeded.
• Generality: The method successfully handled non-polynomial systems (rational, trigonometric) where SOS-based methods are inapplicable.
• Computational Cost: While data generation (reachable set approximation) is computationally intensive, the overall training and verification times were comparable to nominal approaches. The trade-off between trajectory sampling count and accuracy was managed effectively.

5. Significance

This paper represents a significant advancement in the control of uncertain nonlinear systems. By moving from point-wise Lyapunov analysis to set-based value functions, the authors provide a mathematically rigorous way to handle the inherent set-valued nature of robust control problems. The integration of formal verification with physics-informed learning solves a critical bottleneck in applying deep learning to safety-critical systems: the lack of guarantees.

The framework offers a practical, scalable, and theoretically sound alternative to traditional grid-based or polynomial optimization methods, enabling the design of safer and more robust controllers for complex, high-dimensional, and uncertain dynamical systems.