1. Bibliographic Information

1.1. Title

The title of the paper is Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems. This title indicates that the paper proposes a single framework to verify the safety of systems controlled by Deep Neural Networks (DNNs) from two perspectives: qualitative (is it safe or not?) and quantitative (how safe is it, probabilistically?).

1.2. Authors

The authors of the paper are:

• Dapeng Zhi (East China Normal University)
• Pei Wang (Nanyang Technological University)
• Long Li (Nanyang Technological University)
• Min Zhang (East China Normal University)
• Si Liu (ETH Zurich)

1.3. Journal/Conference

The paper is a preprint published on arXiv, indicated by the Original Source Link and PDF Link. The acknowledgment section mentions "We thank the anonymous reviewers of CAV 2024 for their valuable comments," suggesting it has been submitted to or accepted by the Computer Aided Verification (CAV) conference. CAV is a highly reputable and influential conference in the field of formal methods and verification, known for publishing cutting-edge research on verifying hardware and software systems.

1.4. Publication Year

The paper was published on 2024-04-02.

1.5. Abstract

The paper addresses the critical need for certified safety guarantees in safety-critical systems controlled by Deep Neural Networks (DNNs), especially given the advancements in deep reinforcement learning. Existing verification methods are primarily qualitative, relying on reachability analysis, which is deemed insufficient for DNN-controlled systems due to their stochastic tendencies in open and adversarial environments.

The authors propose a novel framework that unifies both qualitative and quantitative safety verification problems for DNN-controlled systems. This unification is achieved by formulating verification tasks as the synthesis of Neural Barrier Certificates (NBCs). The framework first attempts to establish almost-sure safety guarantees through qualitative verification. If this fails, a quantitative verification method is invoked to provide precise lower and upper bounds on probabilistic safety across both infinite and finite time horizons.

To facilitate the synthesis of NBCs, the paper introduces their k-inductive variants. Furthermore, it devises a simulation-guided approach for training NBCs, aiming to compute tighter certified lower and upper bounds. The proposed approach is prototyped in a tool named UniQQ and its effectiveness is demonstrated on four classic DNN-controlled systems.

1.6. Original Source Link

• Original Source Link: https://arxiv.org/abs/2404.01769v1
• PDF Link: https://arxiv.org/pdf/2404.01769v1.pdf
• Publication Status: This is a preprint, version 1, uploaded to arXiv. As noted in the acknowledgments, it has been submitted to CAV 2024.

2. Executive Summary

2.1. Background & Motivation

The core problem the paper aims to solve is the lack of certified safety guarantees for Deep Neural Network (DNN)-controlled systems, especially in safety-critical applications. The rapid advancement of deep reinforcement learning (DRL) has led to DNNs being used to oversee complex systems, but ensuring their safety is paramount.

This problem is important because DNNs operate in open and adversarial environments, leading to stochastic tendencies in their behavior due to factors like environment noises, unreliable sensors, and malicious attacks. Traditional qualitative verification methods, such as reachability analysis, which mainly answer "is it safe?" (yes/no), are often insufficient. When qualitative verification fails, it's crucial to obtain quantitative guarantees, such as probabilistic safety bounds (e.g., "it is safe with X% probability").

Prior research in quantitative verification often relies on automata-based quantitative formalisms (e.g., Markov chains, timed automata). However, applying these to DNN-controlled systems is challenging due to:

1. The difficulty in building a faithful automata-based probabilistic model for DNNs because their actions are state-dependent and continuous state spaces are hard to enumerate.

2. State exploration issues (a known problem in model checking) even if a model is constructed with abstractions, leading to high verification times.

   The paper's innovative idea is to use Neural Barrier Certificates (NBCs) as a unifying approach. Barrier Certificates (BCs) are powerful tools for establishing safety in non-linear and stochastic systems by partitioning the state space. NBCs implement BCs using neural networks, leveraging their expressiveness. The paper's entry point is to unify both qualitative and quantitative safety verification into a single framework centered around the synthesis of NBCs.

2.2. Main Contributions / Findings

The paper makes several primary contributions:

1. Unified Framework: It presents a novel framework that unifies both qualitative (almost-sure safety) and quantitative (probabilistic safety bounds) verification of DNN-controlled systems. This is achieved by reducing these distinct verification problems into the cohesive task of synthesizing appropriate Neural Barrier Certificates (NBCs).
2. Theoretical Results for NBCs: The paper establishes new theoretical foundations for NBCs, including:
   • Specific conditions that NBCs must satisfy for both qualitative and quantitative safety verification.
   • Formulas for computing certified lower and upper bounds for safety probabilities over both infinite and finite time horizons. These bounds are presented in both linear and exponential forms.
3. Enhanced NBC Synthesis:
   • k-inductive Variants: To accelerate and ease the training process, the paper introduces k-inductive variants of NBCs. These variants relax the strict conditions of traditional BCs by leveraging k-induction principles, making synthesis more manageable.
   • Simulation-Guided Training Approach: A novel simulation-guided method is proposed to train potential NBCs. This approach incorporates differences between simulation-estimated safety probabilities and NBC-derived bounds into the loss function, aiming to produce tighter certified bounds.
4. Prototype Tool and Efficacy Demonstration: The authors developed a prototype tool called UniQQ and demonstrated its efficacy on four classic DNN-controlled systems.

   • Experimental Findings: The experiments showcase the effectiveness of the unified approach in providing qualitative and quantitative safety guarantees under various noise scenarios. k-inductive variants reduced verification overhead by an average of 25%. The simulation-guided training method yielded significantly tighter safety bounds, with up to 47.5% improvement for lower bounds and 31.7% for upper bounds compared to ordinary training.

     These findings solve the problem of providing comprehensive, certified safety guarantees for DNN-controlled systems operating under uncertainty, offering both a binary safety answer and precise probabilistic bounds when absolute safety cannot be guaranteed.

3. Prerequisite Knowledge & Related Work

3.1. Foundational Concepts

To understand this paper, a reader needs to be familiar with the following core concepts:

• Deep Neural Networks (DNNs): These are artificial neural networks with multiple layers between the input and output layers. They are capable of learning complex patterns and relationships from data. In DNN-controlled systems, a DNN acts as the controller, taking system states as input and outputting actions.
• Deep Reinforcement Learning (DRL): A subfield of machine learning that combines reinforcement learning (RL) with deep neural networks. RL algorithms learn to make sequences of decisions by interacting with an environment, receiving rewards or penalties, and DRL uses DNNs to represent policies or value functions in this process.
• Safety-Critical Systems: Systems whose failure could result in loss of life, significant property damage, or severe environmental harm (e.g., autonomous vehicles, medical devices, industrial control systems). Ensuring their safety is paramount.
• Formal Methods: A set of mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. They use formal logic and mathematical proofs to ensure system correctness and safety.
• Verification: The process of ensuring that a system meets its specifications. In the context of safety, it means proving that the system will not enter an unsafe state.
• Qualitative Verification: Focuses on whether a property holds true (yes/no, safe/unsafe). For example, reachability analysis determines if an unsafe state can ever be reached.
• Quantitative Verification: Focuses on the probability or likelihood of a property holding true. For example, probabilistic safety quantifies the probability of remaining in a safe state.
• Reachability Analysis: A qualitative verification technique that determines if a system can transition from an initial set of states to a target set of states (e.g., an unsafe set).
• Stochastic Systems: Systems whose behavior is influenced by random processes or uncertainties. In DNN-controlled systems, state perturbations (noise, sensor errors) make them stochastic.
• Barrier Certificates (BCs): Mathematical functions used to prove the safety of dynamical systems. A BC partitions the state space into safe and unsafe regions, and its properties ensure that trajectories starting in the safe region cannot cross into the unsafe region.
  • A discrete-time barrier certificate $B: S \to \mathbb{R}$ for a system $M$ with an initial set $S_0$ and an unsafe set $S_u$ typically satisfies conditions like:
    1. $B(s) \leq 0$ for all $s \in S_0$ (initial states are "safe" with respect to the barrier).
    2. $B(s) > 0$ for all $s \in S_u$ (unsafe states are "unsafe" with respect to the barrier).
    3. $B(f(s, \pi(s))) - B(s) + \lambda \cdot B(s) \leq 0$ for all $s \in S$ (the barrier function does not increase across transitions, or increases at a bounded rate, ensuring trajectories stay in the safe region). Here, $f$ is the system dynamics, $\pi$ is the control policy, and $\lambda \in (0, 1]$ is a constant.
• Neural Barrier Certificates (NBCs): Barrier Certificates implemented and trained as Deep Neural Networks. This leverages the DNNs' expressiveness to find complex BCs that might be difficult to represent with simpler function classes (e.g., polynomials).
• k-Induction: A proof technique used in formal verification. Instead of proving a property holds for all $k=0$ and then that it holds for $k+1$ assuming it holds for $k$ (simple induction), k-induction proves that if a property holds for $k$ consecutive steps, then it also holds for the $(k+1)$-th step. This can simplify proofs for systems with state dependencies extending over multiple steps.
• CounterExample-Guided Inductive Synthesis (CEGIS): An iterative framework for synthesizing programs or functions. It involves a learner that proposes a candidate solution and a verifier that checks its correctness. If the verifier finds a counterexample (a case where the candidate fails), it feeds this counterexample back to the learner to refine the candidate. This cycle continues until a correct solution is found or a timeout is reached.
• Martingales and Supermartingales: Concepts from probability theory.
  • A sequence of random variables $X_0, X_1, X_2, \ldots$ is a martingale if $E[X_{t+1} | X_0, \ldots, X_t] = X_t$. Intuitively, the expected value of the next observation, given all prior observations, is equal to the current observation.
  • A supermartingale is a sequence where $E[X_{t+1} | X_0, \ldots, X_t] \leq X_t$. The expected value of the next observation is less than or equal to the current observation. This property is often used in safety proofs, as a non-increasing function can indicate that a system is moving away from an unsafe region.
  • Submartingale is the opposite: $E[X_{t+1} | X_0, \ldots, X_t] \geq X_t$.
• Lipschitz Continuity: A property of a function that limits how fast it can change. A function $f$ is Lipschitz continuous if there exists a constant $L$ (the Lipschitz constant) such that $|f(x) - f(y)| \leq L|x - y|$ for all x, y in its domain. This property is important for guaranteeing the robustness and predictability of DNNs and system dynamics.
• Interval Bound Propagation (IBP): A technique used in DNN verification to compute rigorous bounds on the output of a neural network given an input interval. It propagates interval bounds through each layer of the network, providing lower and upper bounds for the output.

3.2. Previous Works

The paper extensively cites previous works, categorizing them into:

• Barrier Certificates for Stochastic Systems:

  • Prajna et al. [40, 41, 42] introduced BCs for stochastic systems. This work builds directly on their foundational ideas.
  • Data-driven approaches [44] and k-inductive variants [4] have expanded BC applications. The current paper incorporates k-inductive variants for NBCs.
  • Related work on computing reachability probabilities in stochastic systems for infinite [20, 61, 62] and finite time horizons [60, 59] informs the quantitative aspects.
  • Probabilistic programs have used proof rules [19] and Martingale-based approaches [14, 15, 5] for reachability and termination probabilities, which were later unified by order-theoretic fixed-point approaches [52, 49, 50]. The current paper also leverages Martingale properties for its BC conditions.

• Formal Verification of DNN-controlled Systems:

  • Modeling as Markov Decision Processes (MDPs): Some approaches model DNN-controlled systems as MDPs and use probabilistic model checkers like PRISM [30] and Storm [25] for verification.
  • Bacci and Parker [7, 8] used abstract interpretation to construct interval MDPs for safety probabilities within bounded time and verified probabilistic policies for DRL.
  • Carr et al. [13] proposed probabilistic verification by constraining analysis to partially observable finite-state models.
  • Amir et al. [3] focused on scalable verification for DRL, including liveness properties.
  • Reachability Analysis: This is a pivotal qualitative approach.
    • Bacci et al. [6] introduced a linear over-approximation-based method for reachable set invariants over an infinite time horizon.
    • Other tools like Verisig [28] and Polar [27] focus on bounded time reachability analysis. These often assume deterministic actions and do not explicitly consider perturbations. The current paper explicitly addresses stochasticity and perturbations.

• Barrier Certificates for Training and Verifying DNN Controllers:

  • Recent work [1, 39, 63, 17] has investigated BC-based methods for training and verifying DNN controllers. The core idea is to learn a safe controller through interactive computation of BCs to ensure qualitative safety.
  • Existing BC-based approaches for DNN-controlled systems predominantly focus on qualitative aspects and often neglect perturbations [47, 64]. This paper's approach complements these by explicitly accommodating inherent uncertainty through stochasticity.

3.2.1. Example of a Core Formula from Previous Work: Discrete-time Barrier Certificates (Definition 1)

The paper itself provides a foundational definition from previous work on Discrete-time Barrier Certificates (BCs) in Section 2.2. This definition is crucial for understanding the extensions proposed in the current paper.

Definition 1 (Discrete-time Barrier Certificates). Given a DNN-controlled system $M = ( S , S _ { 0 } , A , f , \pi , R )$ with an unsafe set $S _ { u } \subseteq S$ such that $S _ { u } \cap S _ { 0 } = \emptyset$. A discrete-time barrier certificate is a real-valued function $B : S \to \mathbb { R }$ such that for some constant $\lambda \in ( 0 , 1 ]$, it holds that:

1. $B ( s ) \leq 0$ for all $s \in S _ { 0 }$
2. $B ( s ) > 0$ for all $s \in S _ { u }$
3. $B ( f ( s , \pi ( s ) ) ) - B ( s ) + \lambda \cdot B ( s ) \leq 0$ for all $s \in S$.

Explanation:

• $S$: The set of all possible system states.
• $S_0$: The set of initial states of the system.
• $S_u$: The set of unsafe states. The condition $S_u \cap S_0 = \emptyset$ means that the system starts in a safe configuration.
• B(s): The barrier certificate function, which maps a state $s$ to a real number.
• $\lambda$: A positive constant, usually between 0 and 1, that determines the rate at which the barrier function can decrease.
• $f(s, \pi(s))$: The next state of the system, given the current state $s$ and the action $\pi(s)$ taken by the controller. $\pi(s)$ is the policy (controller) that maps a state to an action.
• Condition 1 ($B(s) \leq 0$ for $s \in S_0$): This means that all initial states must have a barrier function value less than or equal to zero. This implicitly defines the "safe" region as $B(s) \leq 0$.
• Condition 2 ($B(s) > 0$ for $s \in S_u$): This means that all unsafe states must have a barrier function value strictly greater than zero. This defines the "unsafe" region as $B(s) > 0$.
• Condition 3 ($B(f(s, \pi(s))) - B(s) + \lambda \cdot B(s) \leq 0$): This is the crucial inductive condition. It states that for any state $s$, if the system transitions to the next state $f(s, \pi(s))$, the barrier function value for the next state, adjusted by the current barrier value multiplied by $(1-\lambda)$, must not increase (or must decrease sufficiently). More specifically, $B(f(s, \pi(s))) \leq (1-\lambda)B(s)$. If $B(s) \leq 0$, then $B(f(s, \pi(s))) \leq (1-\lambda)B(s) \leq B(s) \leq 0$. This ensures that if the system starts in a state where $B(s) \leq 0$, it will remain in states where $B(s) \leq 0$, and thus never enter the unsafe set where $B(s) > 0$.

3.3. Technological Evolution

The evolution of safety verification for dynamical systems, particularly those controlled by DNNs, has moved from purely theoretical approaches to practical, automated tools.

1. Early formal methods focused on traditional software and hardware, often using model checking and theorem proving for finite-state systems.
2. Continuous-time systems brought the challenge of infinite state spaces, leading to techniques like Lyapunov functions and Barrier Certificates (e.g., Prajna et al.). These provided mathematical proofs for stability and safety.
3. The rise of machine learning and DRL introduced DNNs into control loops, creating DNN-controlled systems. This posed new verification challenges because DNNs are opaque ("black-box"), non-linear, and operate in stochastic environments.
4. Initial approaches adapted existing verification techniques, such as abstracting DNNs into simpler models or modeling the entire system as an MDP. However, these often struggled with scalability or accuracy when dealing with DNN complexity and continuous state spaces.
5. The concept of Neural Barrier Certificates (NBCs) emerged as a way to combine the rigor of BCs with the expressiveness of DNNs. NBCs use DNNs to learn the barrier function itself, making the search for BCs more tractable for complex systems.
6. The current paper fits within this evolution by pushing NBCs further. It addresses the stochasticity often neglected in DNN verification by incorporating state perturbations. Crucially, it unifies qualitative and quantitative verification, offering a more complete safety picture than prior BC-based methods that primarily focused on qualitative safety. It also introduces k-inductive variants and simulation-guided training to improve the efficiency and tightness of NBC synthesis, representing an advancement in practical application.

3.4. Differentiation Analysis

Compared to the main methods in related work, the core differences and innovations of this paper's approach are:

• Unification of Qualitative and Quantitative Verification: Most existing BC-based verification approaches for DNN-controlled systems focus predominantly on qualitative safety (almost-sure safety, yes/no). This paper provides a single framework that can handle both qualitative and quantitative (probabilistic bounds) aspects. This is a significant step towards providing a more comprehensive safety assessment, especially when absolute safety cannot be guaranteed.
• Explicit Handling of Stochasticity and Perturbations: Many existing reachability analysis or BC-based DNN verification methods do not explicitly account for state perturbations or inherent stochasticity in DNN-controlled systems operating in noisy/adversarial environments. This paper rigorously incorporates noise distributions (e.g., $\delta \sim \mu$) into its BC conditions, making the verification more realistic for real-world DNN applications.
• Comprehensive Quantitative Bounds (Infinite and Finite Time, Linear and Exponential): The framework not only provides lower and upper bounds for probabilistic safety but also offers them for both infinite and finite time horizons. Furthermore, it presents these finite-time bounds in both linear and exponential forms, allowing for potentially tighter and more informative estimates depending on the system's dynamics. This level of detail in quantitative guarantees is novel.
• k-Inductive Variants for NBCs: The introduction of k-inductive NBCs for both qualitative and quantitative verification is an innovation. This relaxation of strict BC conditions by leveraging k-induction makes the synthesis of valid NBCs more tractable and computationally efficient, as evidenced by the 25% faster synthesis time observed in experiments.
• Simulation-Guided Training for Tighter Bounds: The simulation-guided loss term in NBC training is a practical innovation aimed at improving the tightness of the certified bounds. By incorporating statistical results from simulations into the loss function, the trained NBCs can yield more precise bounds (up to 47.5% improvement), which is crucial for practical application where loose bounds might be meaningless.
• Leveraging DNN Expressiveness for BCs: While NBCs are not new, this paper effectively adapts and extends their use to address the specific complexities of stochastic DNN-controlled systems in a unified manner, demonstrating their power beyond simple qualitative safety for deterministic systems.

4. Methodology

4.1. Principles

The core idea of the method is to unify qualitative and quantitative safety verification for DNN-controlled systems by formulating both problems as the synthesis of Neural Barrier Certificates (NBCs). The theoretical basis relies on adapting traditional Barrier Certificate (BC) principles, extending them to handle stochasticity and DNN controllers, and then implementing these BCs as neural networks. The intuition is that by finding a suitable NBC function that satisfies specific mathematical conditions, one can formally prove almost-sure safety (qualitative) or calculate probabilistic lower and upper bounds for safety (quantitative). The use of k-induction principles and simulation-guided training further refines the synthesis process, making it more efficient and yielding tighter bounds.

4.2. Core Methodology In-depth (Layer by Layer)

The framework operates in a sequential manner, first attempting qualitative verification, and then proceeding to quantitative verification if qualitative fails or is insufficient. The central mechanism is the synthesis of NBCs for each verification task.

4.2.1. System Model: DNN-controlled Systems with State Perturbations

The paper considers DNN-controlled systems $M = ( S , S _ { 0 } , A , \pi , f , R )$ where:

• $S \subseteq \mathbb { R } ^ { n }$: The state space (possibly continuous and infinite).

• $S_0 \subseteq S$: The set of initial states.

• $A$: The set of actions.

• $\pi : S \to A$: The trained policy implemented by a neural network. This is the DNN controller.

• $f : S \times A \to S$: The system dynamics, describing how the state evolves.

• $R : S \times A \times S \to \mathbb { R }$: The reward function.

  Crucially, the paper accounts for state perturbations due to sensor errors, noise, or attacks. An observed state at time $t$ is $\hat{s}_t := s_t + \delta_t$, where $\delta_t \sim \mu$ is a random noise from a probability distribution $\mu$ over $\mathbb{R}^n$. The support of $\mu$ is denoted by $W := \mathsf{supp}(\mu)$. The action is taken based on the perturbed state: $\hat{a}_t := \pi(\hat{s}_t)$. The actual successor state is $s_{t+1} := f(s_t, \hat{a}_t)$. The system model explicitly incorporating this noise distribution is denoted as $M_{\mu} = ( S , S _ { 0 } , A , \pi , f , R , \mu )$. The state space $S$ is assumed to be compact in Euclidean topology, and $f$ and $\pi$ are Lipschitz continuous. The noise distribution $\mu$ either has bounded support or is a product of independent univariate distributions.

4.2.2. Problem Statement

The paper defines three safety verification problems for a given DNN-controlled system $M_{\mu}$ and an unsafe set $S_u$ (with $S_0 \cap S_u = \emptyset$):

1. Qualitative Verification (QV): Is $M_{\mu}$ almost-surely (a.s.) safe?
   • Almost-sure safety: $\forall s_0 \in S_0 . \omega \in \Omega_{s_0} \implies \omega_t \notin S_u \forall t \in \mathbb{N}$. (No trajectories starting from $s_0$ enter $S_u$ with probability 1).
2. Quantitative Verification over Infinite Time Horizons (QVITH): Compute certified lower and upper bounds $[l_{\mathrm{inf}}, u_{\mathrm{inf}}]$ on the probabilistic safety over infinite time horizons.
   • Probabilistic safety (infinite): $\forall s_0 \in S_0 . \mathbb{P}_{s_0} \left[ \left\{ \omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \in \mathbb{N} \right\} \right] \in \left[ l_{\mathrm{inf}} , u_{\mathrm{inf}} \right]$.
3. Quantitative Verification over Finite Time Horizons (QVFTH): Compute certified lower and upper bounds $[l_{\mathrm{fin}}, u_{\mathrm{fin}}]$ on the probabilistic safety over a finite time horizon $T$.
   • Probabilistic safety (finite): $\forall s_0 \in S_0 . \mathbb{P}_{s_0} \left[ \left\{ \omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \leq T \right\} \right] \in \left[ l_{\mathrm{fin}} , u_{\mathrm{fin}} \right]$.

4.2.3. Unified Verification Framework Overview

The verification process follows a three-step flow, as depicted in Figure 1.

The following figure (Figure 1 from the original paper) shows the system architecture:

Step 1: Qualitative Verification (QV)

• The framework first attempts to synthesize an NBC satisfying the conditions of Theorem 1.
• If successful, the system $M_{\mu}$ is concluded to be almost-surely safe, and verification stops.
• Alternative: If a Theorem 1 NBC cannot be synthesized, it tries to synthesize a k-inductive NBC based on Theorem 8. k-inductive NBCs have weaker conditions and are easier to synthesize.
• If QV fails (no NBC found within timeout), the framework proceeds to quantitative verification.

Step 2: Quantitative Verification over Infinite Time Horizons (QVITH)

• The framework attempts to synthesize two NBCs: one for lower bounds (based on Theorem 2) and one for upper bounds (based on Theorem 3).
• If synthesis fails (timeout), the process terminates.
• Otherwise, it obtains $l_{\mathrm{inf}}$ and $u_{\mathrm{inf}}$.
• Alternative: It can try to synthesize k-inductive variants of NBCs using Theorems 9 and 10.
• If $l_{\mathrm{inf}}$ is greater than or equal to a predefined safety threshold $\delta \in (0, 1)$, verification terminates. This prevents returning a trivially low (e.g., zero) lower bound.
• If $l_{\mathrm{inf}}$ is less than $\delta$, it proceeds to quantitative verification over finite time horizons.

Step 3: Quantitative Verification over Finite Time Horizons (QVFTH)

• The framework attempts to synthesize two NBCs for linear bounds (based on Theorem 4 for lower bounds and Theorem 6 for upper bounds).
• If synthesis fails (timeout), the process terminates.
• Otherwise, it computes linear lower and upper bounds for probabilistic safety over a finite time horizon $T$.
• Alternative: It can also synthesize two NBCs for exponential bounds (based on Theorem 5 for lower bounds and Theorem 7 for upper bounds), which might be tighter.

4.2.4. Detailed Conditions for Barrier Certificates

4.2.4.1. Qualitative Safety Verification (Almost-Sure Safety)

Theorem 1 (Almost-Sure Safety). Given an $M_{\mu}$ with an initial set $S_0$ and an unsafe set $S_u$, if there exists a barrier certificate $B: S \to \mathbb{R}$ such that for some constant $\lambda \in (0, 1]$, the following conditions hold:

1. $B(s) \leq 0$ for all $s \in S_0$,
2. $B(s) > 0$ for all $s \in S_u$,
3. $B(f(s, \pi(s + \delta))) - B(s) + \lambda \cdot B(s) \leq 0$ for all $(s, \delta) \in S \times W$.

Explanation:

• This theorem is an extension of Definition 1 to stochastic systems.
• $W$: The support of the noise distribution $\mu$.
• Condition 1: Initial states must be in the "safe" region ($B(s) \leq 0$).
• Condition 2: Unsafe states must be in the "unsafe" region ($B(s) > 0$).
• Condition 3: This is the inductive condition adapted for stochasticity. It states that for any state $s$ and any possible noise perturbation $\delta$ from $W$, the barrier function value for the next state $f(s, \pi(s+\delta))$ must not increase (or must decrease sufficiently) relative to the current state B(s). The key difference from Definition 1 is $f(s, \pi(s+\delta))$, explicitly considering the perturbed state $s+\delta$ for action selection and the transition over all possible $\delta$ in $W$. If these conditions hold, it implies that the system's trajectories will almost-surely not enter $S_u$.

4.2.4.2. Quantitative Safety Verification over Infinite Time Horizon

Theorem 2 (Lower Bounds on Infinite-time Safety). Given an $M_{\mu}$ with an initial set $S_0$ and an unsafe set $S_u$, if there exists a barrier certificate $B: S \to \mathbb{R}$ such that for some constant $\epsilon \in [0, 1]$, the following conditions hold:

1. $B(s) \geq 0$ for all $s \in S$,

2. $B(s) \leq \epsilon$ for all $s \in S_0$,

3. $B(s) \geq 1$ for all $s \in S_u$,

4. $\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \leq 0$ for all $s \in S \setminus S_u$,

   then the safety probability over infinite time horizons is bounded from below by: $ \forall s_0 \in S_0 . \mathbb{P}{s_0} \left[ \left{ \omega \in \Omega{s_0} \bigm \vert \omega_t \notin S_u \text{ for all } t \in \mathbb{N} \right} \right] \geq 1 - B(s_0) . $

Explanation:

• $\mathbb{E}_{\delta \sim \mu} [\dots \mid s]$: The expected value of the expression given that $\delta$ is drawn from noise distribution $\mu$, and the current state is $s$. This accounts for the probabilistic nature of transitions.
• $S \setminus S_u$: All states that are not in the unsafe set.
• Condition 1: The barrier function must be non-negative everywhere.
• Condition 2: The barrier function value for initial states must be less than or equal to $\epsilon$. This helps define the starting "level" for the lower bound.
• Condition 3: The barrier function value for unsafe states must be at least 1. This acts as a threshold for unsafety.
• Condition 4: This is a supermartingale property. It states that the expected value of the barrier function in the next state (considering noise) must be less than or equal to its current value, for all states outside the unsafe set. This means the barrier function is expected to be non-increasing in the safe region.
• Bound: $1 - B(s_0)$ provides a lower bound on the probability of never entering the unsafe set. If $B(s_0)$ is small (e.g., close to 0), the lower bound is close to 1.

Theorem 3 (Upper Bounds on Infinite-time Safety). Given an $M_{\mu}$ with an initial set $S_0$ and an unsafe set $S_u$, if there exists a barrier certificate $B: S \to \mathbb{R}$ such that for some constants $\gamma \in (0, 1)$, $0 \leq \epsilon' < \epsilon \leq 1$, the following conditions hold:

1. $0 \leq B(s) \leq 1$ for all $s \in S$,

2. $B(s) \geq \epsilon$ for all $s \in S_0$,

3. $B(s) \leq \epsilon'$ for all $s \in S_u$,

4. $B(s) - \gamma \cdot \mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] \leq 0$ for all $s \in S \setminus S_u$,

   then the safety probability over infinite time horizons is bounded from above by: $ \forall s_0 \in S_0 . \mathbb{P}{s_0} \left[ \left{ \omega \in \Omega{s_0} \mid \omega_t \notin S_u \text{ for all } t \in \mathbb{N} \right} \right] \leq 1 - B(s_0) . $

Explanation:

• $\gamma \in (0, 1)$: A discount factor.
• $0 \leq \epsilon' < \epsilon \leq 1$: Constants defining thresholds.
• Condition 1: The barrier function values are bounded between 0 and 1.
• Condition 2: Initial states have a barrier value of at least $\epsilon$. This helps define the starting "level" for the upper bound.
• Condition 3: Unsafe states have a barrier value of at most $\epsilon'$.
• Condition 4: This is a \gamma`-scaled submartingale property`. It implies that $B(s) \leq \gamma \cdot \mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ]$, which means the `expected value` of the `barrier function` is expected to increase by a factor of $1/\gamma$ in the safe region. * **Bound:** $1 - B(s_0)$ provides an `upper bound` on the probability of never entering the `unsafe set`. If $B(s_0)$ is large (e.g., close to 1), the `upper bound` is small. #### 4.2.4.3. Quantitative Safety Verification over Finite Time Horizon **Theorem 4 (Linear Lower Bounds on Finite-time Safety).** Given an $M_{\mu}$ with an initial set $S_0$ and an unsafe set $S_u$, if there exists a `barrier certificate` $B: S \to \mathbb{R}$ such that for some constants $\lambda > \epsilon \geq 0$ and $c \geq 0$, the following conditions hold: 1. $B(s) \geq 0$ for all $s \in S$, 2. $B(s) \leq \epsilon$ for all $s \in S_0$, 3. $B(s) \geq \lambda$ for all $s \in S_u$, 4. $\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \leq c$ for all $s \in S \setminus S_u$, then the `safety probability` over a `finite time horizon` $T$ is bounded from below by: $ \forall s_0 \in S_0 . \mathbb{P}_{s_0} \left[ \left\{ \omega \in \Omega_{s_0} \middle \vert \omega_t \notin S_u \text{ for all } t \leq T \right\} \right] \geq 1 - ( B(s_0) + c T ) / \lambda . $ **Explanation:** * $\lambda > \epsilon \geq 0$: Constants defining thresholds. * $c \geq 0$: A constant representing the maximum allowed increase in the `barrier function` expectation. * **Condition 1-3:** Similar to `Theorem 2`, defining non-negativity and thresholds for initial/unsafe states. * **Condition 4:** This is a `c-martingale property`. It implies that the `expected value` of the `barrier function` is allowed to increase by at most $c$ at each time step. This is less strict than a `supermartingale` (where $c=0$), allowing for some drift in the `barrier function`, but in exchange, it provides `finite-time guarantees`. * **Bound:** The `lower bound` is $1 - (B(s_0) + cT)/\lambda$. This is a `linear decrease` with time $T$. As $T$ increases, the probability of safety decreases linearly. **Theorem 5 (Exponential Lower Bounds on Finite-time Safety).** Given an $M_{\mu}$, if there exists a function $B: S \to \mathbb{R}$ such that for some constants $\alpha > 0$, $\beta \in \mathbb{R}$, and $\gamma \in [0, 1)$, the following conditions hold: 1. $B(s) \geq 0$ for all $s \in S$, 2. $B(s) \leq \gamma$ for all $s \in S_0$, 3. $B(s) \geq 1$ for all $s \in S_u$, 4. $\alpha \mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \leq \alpha \beta$ for all $s \in S \setminus S_u$. then the `safety probability` over a `finite time horizon` $T$ is bounded from below by: $ \forall s_0 \in S_0 . \mathbb{P}_{s_0} \left[ \left\{ \omega \in \Omega_{s_0} \mid \omega_t \notin S_u \text{ for all } t \right\} \right] \geq 1 - \frac { \alpha \beta } { \alpha - 1 } + \left( \frac { \alpha \beta } { \alpha - 1 } - B(s_0) \right) \cdot \alpha^{-T} . $ **Explanation:** * $\alpha > 0, \beta \in \mathbb{R}, \gamma \in [0, 1)$: Constants. * **Condition 1-3:** Similar to previous `lower bound` theorems. * **Condition 4:** This condition implies that $B(s) \geq \alpha (\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - \beta)$. The \alpha-scaled expectation of $B$ can increase by at most $\alpha \beta$ at each step. This leads to an exponential bound.
• Bound: The lower bound involves $\alpha^{-T}$, indicating an exponential decrease with time $T$. This form can be tighter than the linear bound for certain systems.

Theorem 6 (Linear Upper Bounds on Finite-time Safety). Given an $M_{\mu}$ with an initial set $S_0$ and an unsafe set $S_u$, if there exists a barrier function $B: S \to \mathbb{R}$ such that for some constants $\beta \in (0, 1)$, $\beta < \alpha < 1 + \beta$, $c \geq 0$, the following conditions hold:

1. $B(s) \geq 0$ for all $s \in S$,

2. $B(s) \leq \beta$ for all $s \in S \setminus S_u$,

3. $\alpha \leq B(s) \leq 1 + \beta$ for all $s \in S_u$,

4. $\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \geq c$ for all $s \in S \setminus S_u$.

   then the safety probability over a finite time horizon $T$ is bounded from above by: $ \forall s_0 \in S_0 . \mathbb{P}{s_0} \left[ \left{ \omega \in \Omega{s_0} \mid \omega_t \notin S_u \text{ for all } t \leq T \right} \right] \leq 1 - B(s_0) - \frac{1}{2} c \cdot T + \beta . $

Explanation:

• $\beta \in (0, 1), \beta < \alpha < 1 + \beta, c \geq 0$: Constants.
• Condition 1: Non-negativity of B(s).
• Condition 2: States outside the unsafe set have a barrier value at most $\beta$.
• Condition 3: Unsafe states have barrier values between $\alpha$ and $1+\beta$.
• Condition 4: This is an "inverse" c-martingale property. It states that the expected value of $B$ must increase by at least $c$ at each time step for states outside $S_u$. This implies a tendency to "escape" the safe region.
• Bound: The upper bound shows a linear decrease in safety probability with $T$.

Theorem 7 (Exponential Upper Bounds on Finite-Time Safety). Given an $M_{\mu}$ with an initial set $S_0$ and an unsafe set $S_u$, if there exists a barrier function $B: S \to \mathbb{R}$ such that for some constants $K' \leq K < 0$, $\epsilon > 0$ and a non-empty interval [a, b], the following conditions hold:

1. $B(s) \geq 0$ for all $s \in S \setminus S_u$,

2. $K' \leq B(s) \leq K$ for all $s \in S_u$,

3. $\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \leq - \epsilon$ for all $s \in S \setminus S_u$,

4. $a \leq B(f(s, \pi(s+\delta))) - B(s) \leq b$ for all $s \in S \setminus S_u$ and $\delta \in W$.

   then the safety probability over a finite time horizon $T$ is bounded from above by: $ \forall s_0 \in S_0 . \mathbb{P}{s_0} \left[ \left{ \omega \in \Omega{s_0} \mid \omega_t \notin S_u \text{ for all } t \leq T \right} \right] \leq \exp \left( - \frac{2 (\epsilon \cdot T - B(s_0))^2}{T \cdot (b - a)^2} \right) . $

Explanation:

• $K' \leq K < 0, \epsilon > 0, [a, b]$: Constants and interval. Note B(s) is negative in $S_u$.
• Condition 1: Non-negativity of B(s) outside $S_u$.
• Condition 2: Unsafe states have barrier values bounded between $K'$ and $K$, both negative. This is a subtle difference where the barrier function is negative in the unsafe region, which could imply a different scaling or interpretation compared to previous positive-valued barriers.
• Condition 3: This is a supermartingale difference condition. The expected value of $B$ must decrease by at least $\epsilon$ at each time step for states outside $S_u$. This means the barrier function is expected to decrease, pushing away from unsafe states.
• Condition 4: This ensures that the change in B(s) between steps, $B(f(s, \pi(s+\delta))) - B(s)$, is bounded within an interval [a, b]. This boundedness is crucial for applying Hoeffding's Inequality.
• Bound: The upper bound involves an exponential decay with $T$. This is derived using Hoeffding's Inequality on Supermartingales.

4.2.5. Relaxed k-Inductive Barrier Certificates

To make NBC synthesis more manageable, especially for qualitative verification where Theorem 1 might be too strict, the paper introduces k-inductive variants.

4.2.5.1. k-Inductive Update Functions

First, the concept of a k-step update function $g_{\pi,f}^k$ is defined. $ g_{\pi, f}^k (s_t, \Delta_t^k) = \begin{cases} g_{\pi, f} (g_{\pi, f}^{k-1} (s_t, \Delta_t^{k-1}), \delta_{t+k-1}) & \text{if } k > 1 \ f(s_t, \pi(s_t + \delta_t)) & \text{if } k = 1 \ s_t & \text{if } k = 0 \end{cases} $ where $\Delta_t^k = [\delta_t, \delta_{t+1}, \ldots, \delta_{t+k-1}]$ is a noise vector of length $k$ (each $\delta_i \sim \mu$), and $g_{\pi,f}(s_t, \delta_t) := f(s_t, \pi(s_t + \delta_t))$.

• This function effectively computes the state after $k$ steps, considering a sequence of $k$ noise values. $\mu^k$ denotes the product measure on $W^k$.

4.2.5.2. k-Inductive Barrier Certificates for Qualitative Safety

Theorem 8 (k-inductive Variant of Almost-Sure Safety). Given an $M_{\mu}$ with an initial set $S_0$ and an unsafe set $S_u$, if there exists a k-inductive barrier certificate $B: S \to \mathbb{R}$ such that the following conditions hold:

1. $\bigwedge_{0 \leq i < k} B(g_{\pi, f}^i (s, \Delta^i)) \leq 0$ for all $(s, \Delta^i) \in S_0 \times W^i$,

2. $B(s) > 0$ for all $s \in S_u$,

3. $\bigwedge_{0 \leq i < k} (B(g_{\pi, f}^i (s, \Delta^i)) \leq 0) \implies B(g_{\pi, f}^k (s, \Delta^k)) \leq 0$ for all $(s, \Delta^i) \in S \times W^i$,

   then the system $M_{\mu}$ is almost-surely safe.

Explanation:

• Condition 1: This is the base case for k-induction. It requires that for any initial state $s \in S_0$, and for any noise sequence $\Delta^i$ of length $i < k$, the barrier function value must remain non-positive for the first $k$ steps.
• Condition 2: Unsafe states still have $B(s) > 0$.
• Condition 3: This is the inductive step. It states that if the system has remained safe (i.e., $B(s') \leq 0$) for $k$ consecutive steps (given by the conjunction $\bigwedge_{0 \leq i < k} (B(g_{\pi, f}^i (s, \Delta^i)) \leq 0)$), then it will also be safe at the $(k+1)$-th step (i.e., $B(g_{\pi, f}^k (s, \Delta^k)) \leq 0$).
• Practical Condition: To compute k-inductive BCs, Condition 3 (implication) is often replaced by a sufficient condition: $
  • B(g_{\pi, f}^k (s, \Delta^k)) - \sum_{0 \leq i < k} \tau_i \cdot (- B(g_{\pi, f}^i (s, \Delta^i))) \geq 0 , \ \forall (s, \Delta^i) \in S \times W^i . $ If there exist non-negative coefficients $\tau_0, \ldots, \tau_{k-1} \geq 0$ satisfying this linear combination condition, then Condition 3 is satisfied. This transformation makes the condition amenable to optimization-based synthesis.

4.2.5.3. k-Inductive Barrier Certificates for Quantitative Safety

Theorem 9 (k-inductive Lower Bounds on Infinite-time Safety). Given an $M_{\mu}$, if there exists a k-inductive barrier certificate $B: S \to \mathbb{R}$ such that for some constants $k \in \mathbb{N}_{\geq 1}$, $\epsilon \in [0, 1]$ and $c \geq 0$, the following conditions hold:

1. $B(s) \geq 0$ for all $s \in S$,

2. $B(s) \leq \epsilon$ for all $s \in S_0$,

3. $B(s) \geq 1$ for all $s \in S_u$,

4. $\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \leq c$ for all $s \in S \setminus S_u$,

5. $\mathbb{E}_{\Delta^k \sim \mu^k} [ B(g_{\pi, f}^k (s, \Delta^k)) \mid s ] - B(s) \leq 0$ for all $s \in S \setminus S_u$,

   then the safety probability over infinite time horizons is bounded from below by: $ \forall s_0 \in S_0 . \mathbb{P}{s_0} \left[ \left{ \omega_0 \in \Omega{s_0} \mid \omega_t \notin S_u \text{ for all } t \in \mathbb{N} \right} \right] \geq 1 - k B(s_0) - \frac{k(k-1)c}{2} . $

Explanation:

• This theorem combines elements from Theorem 2 (for infinite-time lower bounds) and the k-induction concept.
• Conditions 1-3: Standard conditions for lower bounds.
• Condition 4: Requires $B$ to be a c-martingale at every single time step.
• Condition 5: Requires $B$ to be a supermartingale when sampled after every $k$-th step, i.e., $k$ steps are considered together.
• Bound: The lower bound is modified by factors of $k$ and $c$, reflecting the relaxation provided by k-induction and the c-martingale property.

Theorem 10 (k-inductive Upper Bounds on Infinite-time Safety). Given an $M_{\mu}$, if there exists a barrier certificate $B: S \to \mathbb{R}$ such that for some constant $\gamma \in (0, 1)$, $0 \leq \epsilon' < \epsilon \leq 1$, $c \leq 0$, the following conditions hold:

1. $0 \leq B(s) \leq 1$ for all $s \in S$,

2. $B(s) \geq \epsilon$ for all $s \in S_0$,

3. $B(s) \leq \epsilon'$ for all $s \in S_u$,

4. $\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \geq c$ for all $s \in S$,

5. $B(s) - \gamma^k \cdot \mathbb{E}_{\Delta^k \sim \mu^k} [ B(g_{\pi, f}^k (s, \Delta^k)) \mid s ] \leq 0$ for all $s \in S \setminus S_u$,

   then the safety probability over infinite time horizons is bounded from above by: $ \forall s_0 \in S_0 . \mathbb{P}{s_0} \left[ \left{ \omega \in \Omega{s_0} \mid \omega_t \notin S_u \text{ for all } t \in \mathbb{N} \right} \right] \leq 1 - k B(s_0) - \frac{k(k-1)c}{2} . $

Explanation:

• This theorem is for k-inductive upper bounds on infinite-time safety.
• Conditions 1-3: Standard conditions for upper bounds.
• Condition 4: This is an "inverse" c-martingale property (expected value increases by at least $c$, where $c$ is non-positive).
• Condition 5: Requires $B$ to be a \gamma^k`-scaled submartingale` when sampled after every $k$-th step. * **Bound:** The `upper bound` is similarly modified by factors of $k$ and $c$. * **Remark on $k$ for `k-inductive variants`:** For the probabilistic bounds in `Theorem 9` and `Theorem 10` to be non-trivial (i.e., meaningful, not just $P \geq 0$), the value of $k$ must be bounded by: $ 1 \leq k \leq \frac { ( c - 2 B ( s _ { 0 } ) ) + \sqrt { 4 B ( s _ { 0 } ) ^ { 2 } + c ^ { 2 } - 4 c ( B ( s _ { 0 } ) - 2 ) } } { 2 c } . $ ### 4.2.6. Synthesis of Neural Barrier Certificates (NBCs) The `BCs` defined above are synthesized as `Neural Barrier Certificates (NBCs)` using a `CEGIS (CounterExample-Guided Inductive Synthesis)` approach. This iterative process is shown in Figure 2. The following figure (Figure 2 from the original paper) shows the system architecture: ![Fig. 2. CEGIS-based NBC synthesis \[2\]](/files/papers/693134495b4290fa4ffbe7b5/images/2.jpg) **Workflow of CEGIS-based NBC Synthesis:** 1. **Initialize Candidate NBC:** A `neural network` $h_{\theta}$ (with parameters $\theta$) is initialized to act as the candidate `BC`. 2. **Training Phase:** * **Training Data Discretization:** Since the state space $S$ is continuous, a finite set of states $\tilde{S} \subseteq S$ is used for training. $\tilde{S}$ is generated by discretizing $S$ (e.g., a grid with granularity $\tau$). Finite subsets $\tilde{S}_0 = \tilde{S} \cap S_0$ and $\tilde{S}_u = \tilde{S} \cap S_u$ are derived. * **Loss Function Construction:** $h_{\theta}$ is trained by minimizing a `loss function` $\mathcal{L}(\theta)$ which is a weighted sum of several terms. Each term corresponds to a condition from the relevant `BC theorem`. For `Theorem 2` (lower bound on infinite-time safety), the loss is: $ \mathcal{L} ( \boldsymbol { \theta } ) := k _ { 1 } \cdot \mathcal { L } _ { 1 } ( \boldsymbol { \theta } ) + k _ { 2 } \cdot \mathcal { L } _ { 2 } ( \boldsymbol { \theta } ) + k _ { 3 } \cdot \mathcal { L } _ { 3 } ( \boldsymbol { \theta } ) + k _ { 4 } \cdot \mathcal { L } _ { 4 } ( \boldsymbol { \theta } ) + k _ { 5 } \cdot \mathcal { L } _ { 5 } ( \boldsymbol { \theta } ) $ where $k_i \in \mathbb{R}$ are `algorithmic parameters`. * $\mathcal{L}_1(\theta)$: Corresponds to `Condition 1` ($B(s) \geq 0$) of `Theorem 2`. $ \mathcal { L } _ { 1 } ( \theta ) = \frac { 1 } { \vert \tilde { S } \vert } \sum _ { s \in \tilde { S } } \left( \operatorname* { m a x } \{ 0 - h _ { \theta } ( s ) , 0 \} \right) $ A loss is incurred if $h_{\theta}(s) < 0$. * $\mathcal{L}_2(\theta)$: Corresponds to `Condition 2` ($B(s) \leq \epsilon$) of `Theorem 2`. $ \mathcal { L } _ { 2 } ( \theta ) = \displaystyle \frac { 1 } { | \tilde { S } _ { 0 } | } \sum _ { s \in \tilde { S } _ { 0 } } \left( \operatorname* { m a x } \{ h _ { \theta } ( s ) - \epsilon , 0 \} \right) $ A loss is incurred if $h_{\theta}(s) > \epsilon$ for initial states. * $\mathcal{L}_3(\theta)$: Corresponds to `Condition 3` ($B(s) \geq 1$) of `Theorem 2`. $ \mathcal { L } _ { 3 } ( \theta ) = \frac { 1 } { | \tilde { S } _ { u } | } \sum _ { s \in \tilde { S } _ { u } } \left( \operatorname* { m a x } \{ 1 - h _ { \theta } ( s ) , 0 \} \right) . $ A loss is incurred if $h_{\theta}(s) < 1$ for unsafe states. * $\mathcal{L}_4(\theta)$: Corresponds to `Condition 4` ($\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \leq 0$) of `Theorem 2`. $ \mathcal { L } _ { 4 } ( \theta ) = \frac { 1 } { \left| \tilde { S } \setminus \tilde { S } _ { u } \right| } \sum _ { s \in \tilde { S } \setminus \tilde { S } _ { u } } \left( \operatorname* { m a x } \left\{ \sum _ { s ^ { \prime } \in \mathcal { D } _ { s } } \frac { h _ { \theta } ( s ^ { \prime } ) } { N } - h _ { \theta } ( s ) + \zeta , 0 \right\} \right) $ Here, $\mathcal{D}_s := \{s' | s' = f(s, \pi(s+\delta_i)), \delta_i \sim \mu, i \in [1, N]\}$ is a set of $N$ `successor states` sampled with `noise`. The sum approximates the `expected value` $\mathbb{E}_{\delta \sim \mu} [\dots]$. $\zeta > 0$ is a small constant used to tighten the condition (making it $\leq -\zeta$ instead of $\leq 0$). * **`Simulation-Guided Loss Term`** ($\mathcal{L}_5(\theta)$): This is a novel term to improve the `tightness` of the bounds. $ \mathcal { L } _ { 5 } ( \theta ) = \frac { 1 } { \vert \tilde { S } _ { 0 } \vert } \sum _ { s \in \tilde { S } _ { 0 } } \left( \operatorname* { m a x } \{ \mathbb { f } _ { s } + h _ { \theta } ( s ) - 1 , 0 \} \right) $ For each initial state $s_0 \in \tilde{S}_0$, $N'$ episodes are simulated to estimate the `safety frequency` $\mathbb{f}_s$ over `infinite time horizons`. This term penalizes `NBCs` whose calculated lower bound ($1-h_{\theta}(s)$) is too far below the `simulated frequency` $\mathbb{f}_s$. Intuitively, it forces $h_{\theta}(s)$ to be smaller if $\mathbb{f}_s$ is high, thus making $1-h_{\theta}(s)$ higher and tighter to the true safety probability. 3. **Validation Phase:** After training, the candidate `NBC` $h_{\theta}$ is checked for validity. * **Conditions 1-3 (for Theorem 2):** These are checked using `interval bound propagation (IBP)` [21, 58]. The goal is to verify if: $ \operatorname* { i n f } _ { s \in S } h _ { \theta } ( s ) \geq 0 \ \wedge \ \operatorname* { s u p } _ { s \in S _ { 0 } } h _ { \theta } ( s ) \leq \epsilon \ \wedge \ \operatorname* { i n f } _ { s \in S _ { u } } h _ { \theta } ( s ) \geq 1 $ If any state violates these, it's a `counterexample`. * **Condition 4 (for Theorem 2):** $\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \leq 0$ is checked. `Theorem 11` is used to reduce this check from infinite states to finite states: **Theorem 11.** Given an $M_{\mu}$ and a function $B: S \to \mathbb{R}$, we have $\mathbb{E}_{\delta \sim \mu} [ B(f(s, \pi(s+\delta))) \mid s ] - B(s) \leq 0$ for any state $s \in S \setminus S_u$ if the formula below $ \mathbb { E } _ { \delta \sim \mu } [ B ( f ( \tilde { s } , \pi ( \tilde { s } + \delta ) ) ) \mid \tilde { s } ] \le B ( \tilde { s } ) - \zeta $ holds for any state $\tilde{s} \in \tilde{S} \setminus \tilde{S}_u$, where `\zeta = \tau \cdot L_B \cdot (1 + L_f \cdot (1 + L_{\pi}))`. Here $\tau$ is the granularity of $\tilde{S}$, and $L_B, L_f, L_{\pi}$ are `Lipschitz constants` of $B, f, \pi$ respectively. * To compute the `expected value` for validation, `interval arithmetic` is used to bound it from above: $ \mathbb { E } _ { \delta \sim \mu } [ h _ { \theta } ( f ( \tilde { s } , \pi ( \tilde { s } + \delta ) ) ) \mid \tilde { s } ] \leq \sum _ { W _ { i } \in \mathrm { c e l l } ( \mathbb { W } ) } \operatorname* { m a x } \mathrm { v o l } \cdot \operatorname* { s u p } _ { \delta } F ( \delta ) $ where $F(\delta) = h_{\theta}(f(\tilde{s}, \pi(\tilde{s}+\delta)))$. The `support` $W$ of $\mu$ is partitioned into cells $W_i$, and $\operatorname{maxvol}$ is the maximal volume of these cells. The supremum over $\delta$ within each cell is computed using `interval arithmetic`. * **Counterexample Generation:** If validation fails for any condition, `counterexamples` are generated and added to the training set $\tilde{S}$. The granularity $\tau$ might also be reduced. 4. **Iteration:** The process (`training` $\rightarrow$ `validation` $\rightarrow$ `counterexample generation`) repeats until a valid `NBC` is found or a timeout is reached. 5. **Soundness (Theorem 12):** If a trained `NBC` is valid, it `certifies` the safety property (almost-sure safety or specific bounds). **Theorem 12 (Soundness).** If a trained `NBC` is valid, it can certify the `almost-sure safety` for the `qualitative verification`, or the derived bound by the `NBC` is a `certified lower/upper bound` on the `safety probability` for the `quantitative case`. This rigorous `CEGIS` loop, combined with the specific `loss functions` and `validation techniques`, ensures that the synthesized `NBCs` are mathematically sound and capable of providing `certified safety guarantees`. # 5. Experimental Setup ## 5.1. Datasets The experiments evaluate the approach on four classic `DNN-controlled tasks` from public benchmarks: 1. **Pendulum (PD):** From OpenAI's Gym [11]. This is a classic control problem involving a pendulum that starts in a random position and aims to swing up and balance vertically. 2. **Cartpole (CP):** From OpenAI's Gym [11]. Another classic control problem where a pole is attached by an un-actuated joint to a cart, which moves along a frictionless track. The system's goal is to keep the pole upright by moving the cart left or right. 3. **B1:** A benchmark system commonly used by state-of-the-art safety verification tools [28]. (Specific details on the dynamics are not provided in the paper's main text). 4. **Tora:** Another benchmark system commonly used by state-of-the-art safety verification tools [28]. (Specific details on the dynamics are not provided in the paper's main text). These datasets/tasks are standard in the field of `reinforcement learning` and `control theory`, making them effective for validating the method's performance and comparability with other approaches. They represent diverse dynamical systems, some with higher dimensionality or more complex control challenges. The paper considers `state perturbations` using `uniform noises` with zero means and different radii. For each state $s = (s_1, \ldots, s_n)$, noises $X_1, \ldots, X_n$ are added to each dimension, resulting in the perturbed state $(s_1 + X_1, \ldots, s_n + X_n)$, where $X_i \sim \mathbf{U}(-r, r)$ for $1 \leq i \leq n$ and $r \geq 0$ is the `perturbation radius`. ## 5.2. Evaluation Metrics The paper evaluates its approach based on: 1. **Qualitative Verification Outcome:** * \checkmark$$: System is verified to be almost-surely safe (an NBC from Theorem 1 or Theorem 8 was successfully trained and validated).
  • Unknown: No valid barrier certificate was trained within the given timeout.
  • #Fail: Number of episodes where the system enters the unsafe region during simulation. This is used as a baseline for qualitative assessment.

2. Quantitative Safety Probabilities (Lower and Upper Bounds):

   • For QVITH and QVFTH, the primary metrics are the certified lower bounds ($l$) and upper bounds ($u$) on the safety probability. These are derived from the validated NBCs using the formulas provided in Theorems 2-7 (and their k-inductive variants).
   • The paper calculates the mean values of these bounds over 10,000 randomly chosen initial states.
   • Baseline for quantitative evaluation: Simulation outcomes (statistical results) are used. This involves running 10,000 episodes starting from each of the 10,000 initial states under different perturbations and recording the safety frequency (the proportion of trajectories that remain safe). The certified bounds are then compared against these simulation outcomes to assess their tightness and correctness.

3. Synthesis Time: The time taken (in seconds) to synthesize different types of NBCs (normal vs. k-inductive). This measures the efficiency of the synthesis process.

4. Improvement in Tightness: For the simulation-guided training method, the improvement in tightness is measured by comparing the width of the certified bounds (difference between upper and lower bound) and how close they are to the simulation outcomes, relative to NBCs trained without the simulation-guided loss term.

   The mathematical formulas for the bounds are provided within the Methodology section, as they are central to the proposed theorems. For instance, the lower bound for infinite-time safety is $1 - B(s_0)$, and the upper bound is also $1 - B(s_0)$ (though $B(s_0)$ has different properties for upper and lower bounds). The complexity of these bounds varies, for example, the exponential upper bound is given by $\exp \left( - \frac{2 (\epsilon \cdot T - B(s_0))^2}{T \cdot (b - a)^2} \right)$. Each of these bounds is a direct output of the theorems once a valid B(s) is found.

5.3. Baselines

The paper's method is primarily compared against:

• Simulation Results: For qualitative verification, simulations are run to count the number of failed episodes (trajectories entering the unsafe region). For quantitative verification, safety probabilities are estimated through extensive simulations (10,000 episodes for each of 10,000 initial states). These simulation outcomes serve as the ground truth or baseline against which the certified bounds from NBCs are validated and their tightness is assessed.

• Non-k-inductive NBCs: When evaluating k-inductive variants, the performance (synthesis time, tightness of bounds) is compared against the corresponding NBCs without k-induction ($k=1$).

• NBCs without Simulation-Guided Loss Terms: To demonstrate the effectiveness of the simulation-guided training, the bounds obtained from NBCs trained with this specialized loss term are compared against those trained using only the standard BC conditions in their loss function.

  The paper implicitly references state-of-the-art tools like Verisig [28] for B1 and Tora benchmarks, indicating these are commonly used systems for such comparisons, though no direct numerical comparisons against those tools are presented for the specific problem formulation of stochasticity and quantitative bounds that this paper tackles.

6. Results & Analysis

6.1. Core Results Analysis

The paper presents experimental results to validate three aspects of its framework: (i) effectiveness of qualitative and quantitative verification, (ii) benefits of k-inductive BCs, and (iii) impact of simulation-guided training.

6.1.1. Effectiveness of Qualitative Safety Verification

The following are the results from Table 1 of the original paper:

Analysis:

• Consistency: For systems where qualitative verification (Verification column) is successful (✓), the simulation (#Fail. column) consistently shows 0 failures. Conversely, for CP with $r=0.03$ and PD with $r=0.01$ and $r=0.03$, where simulations show failures, the qualitative verification result is Unknown. This consistency between formal verification and simulation reflects the effectiveness of the approach.
• Impact of Perturbation: As the perturbation radius $r$ increases (e.g., PD from $r=0$ to $r=0.01$), qualitative verification often shifts from ✓ to Unknown, and simulation failures appear. This indicates that almost-sure safety becomes harder to guarantee with increasing noise, which is expected.
• Efficacy of k-inductive BCs:
  • For CP with $r=0.01$, Theorem 1 (with $k=1$) fails to synthesize an NBC (Unknown), even though simulation shows 0 failures. However, using a 2-inductive NBC ($k=2$, Theorem 8) successfully verifies the system (✓).
  • Similarly, for Tora with $r=0.02$, Theorem 1 fails, but a 2-inductive NBC succeeds.
  • This demonstrates that k-inductive variants can relax the strict conditions of NBCs, making synthesis possible in cases where standard NBCs fail, thereby easing the verification process.

6.1.2. Effectiveness of Quantitative Safety Verification over Infinite Time Horizon

The following figure (Figure 3 from the original paper) shows the certified upper and lower bounds over infinite and finite time horizons, respectively, and their comparison with the simulation results:

Analysis of Figures 3 (a-d) (Infinite Time Horizons):

• Enclosure of Simulation: The certified upper (blue lines with $\cdot_+$) and lower bounds (red lines with $\cdot_\cdot$) consistently enclose the simulation outcomes (black lines with $\bullet_\bullet$). This visually confirms the soundness of the NBCs in providing valid safety probability bounds.

• Impact of Perturbation (r): As the perturbation radius $r$ increases, the safety probabilities (both simulated and certified bounds) generally decrease. This reflects the intuitive understanding that higher noise leads to lower safety guarantees.

• k-inductive Bounds: 2-inductive upper (purple lines with \cdot_{\text{}}) and lower bounds` (green lines with $\cdot_{\times}$) are also shown. These also enclose the simulation results.

• Tightness: The gap between the lower and upper bounds indicates the tightness of the certification. While the bounds are generally valid, there's a visible gap, suggesting room for improvement in tightness.

  The following are the results from Table 2 of the original paper:

  Task	Lower	2-Lower	Upper	2-Upper
  CP	2318.5	1876.0	2891.9	2275.3
  PD	1941.6	1524.0	2282.7	1491.5
  Tora	280.3	218.5	895.1	650.7
  B1	587.4	313.6	1127.3	840.1

Analysis of Table 2 (Synthesis Time):

• Efficiency of k-inductive NBCs: The synthesis time for 2-inductive NBCs (2-Lower, 2-Upper columns) is consistently lower than for regular NBCs (Lower, Upper columns). On average, k-inductive NBCs are 25% faster to synthesize. This empirically supports the claim that relaxing BC conditions via k-induction eases the synthesis process, leading to reduced verification overhead.
• Trade-off: The paper notes that this speedup comes "at the sacrifice of tightness," though it also states that tightness varies by system and perturbation. This highlights a potential trade-off between synthesis speed and the precision of the resulting bounds.

6.1.3. Effectiveness of Quantitative Safety Verification over Finite Time Horizon

Analysis of Figures 3 (e-h) (Finite Time Horizons):

• Enclosure of Simulation: Similar to infinite-time horizons, the certified linear (red lines for lower, green lines for upper) and exponential (purple lines for lower, blue lines for upper) bounds for finite-time safety consistently enclose the simulation outcomes (black lines). This further demonstrates the soundness of the proposed methods.
• Comparison of Linear vs. Exponential Bounds:
  • The exponential upper bounds (blue lines) are generally tighter than the linear upper bounds (green lines).
  • The exponential lower bounds (purple lines) become tighter than the linear lower bounds (red lines) as the time horizon $T$ increases. This suggests that exponential bounds capture the long-term decay of safety probabilities more accurately.
• Declining Safety over Time: All bounds and simulations show a clear declining trend in safety probabilities as the finite time horizon $T$ increases, which is expected when almost-sure safety cannot be guaranteed.

6.1.4. Effectiveness of Simulation-guided Loss Term

The following figure (Figure 4 from the original paper) shows the certified bounds w/ and w/o simulation-guided loss terms over infinite time horizons:

Analysis of Figure 4:

• Improved Tightness:
  • The upper bounds (blue lines with $\cdot_+$) and lower bounds (red lines with $\cdot_\cdot$) obtained with the simulation-guided loss term are noticeably tighter (closer to the simulation results and to each other) than those obtained without it (green lines with $\cdot_{\times}$ for upper, purple lines with \cdot_{\text{}}` for lower).
  • Specifically, the average improvement in tightness is 47.5% for lower bounds and 31.7% for upper bounds.
• Crucial Role: This result strongly indicates that the simulation-guided loss term is essential for practical quantitative safety verification, as it significantly enhances the precision of the certified bounds. Without it, the bounds might be too loose to be practically useful.

6.2. Ablation Studies / Parameter Analysis

The paper implicitly conducts ablation studies and parameter analysis through its comparisons:

• k-inductive BCs vs. $k=1 BCs$: By comparing synthesis time and (implied) tightness, the paper shows the benefit of relaxing the inductive conditions with $k > 1$. This is an ablation on the inductive step's complexity.

• Simulation-guided Loss Term vs. No Simulation-guided Loss Term: This is a direct ablation study on the proposed loss term, demonstrating its isolated impact on the tightness of certified bounds.

• Linear vs. Exponential Bounds: While not strictly an ablation study on model components, the comparison between linear and exponential bounds highlights the impact of the underlying mathematical formulation (and thus different BC conditions) on the resulting tightness over finite time horizons.

  The effect of the perturbation radius $r$ is also systematically analyzed across all experiments, showing how this key environmental hyper-parameter influences the almost-sure safety status and the probabilistic safety bounds. The results consistently show a decrease in safety with increasing $r$.

7. Conclusion & Reflections

7.1. Conclusion Summary

This paper presents a comprehensive and unified framework for qualitative and quantitative safety verification of DNN-controlled systems. It successfully reduces these verification problems into the task of synthesizing Neural Barrier Certificates (NBCs). The framework systematically addresses the challenge of stochasticity and uncertainty inherent in DNN-controlled systems by incorporating state perturbations into its BC conditions.

Key contributions include:

• Novel theoretical results defining NBCs for both almost-sure safety and probabilistic safety bounds over infinite and finite time horizons, with linear and exponential forms for the latter.

• The introduction of k-inductive NBCs to relax constraints and accelerate training (average 25% faster synthesis).

• A simulation-guided training approach that significantly improves the tightness of certified bounds (up to 47.5% for lower bounds).

• A prototype tool UniQQ demonstrating the efficacy of the framework across classic DNN-controlled systems, with experimental results consistently validating the soundness of the certified bounds against simulations.

  The framework provides a holistic approach to delivering various safety guarantees, accommodating qualitative or quantitative results, and spanning different time horizons and bound forms, thereby addressing a critical need in DNN-controlled system deployment.

7.2. Limitations & Future Work

The authors acknowledge the following:

• Dependence on NBC Quality: Both qualitative and quantitative verification results are significantly dependent on the quality of the trained NBCs. This implies that the expressiveness, convergence, and robustness of the neural network chosen for the NBC directly influence the verification outcome.

• Factors Influencing Tightness: While the paper explores k-inductive variants and simulation-guided training for tightness, it also notes that the tightness of certified bounds depends on specific systems and perturbations. Investigating what factors influence this tightness to yield tighter bounds is an interesting future work.

  Based on these, the authors plan to:

• Explore more sophisticated deep learning methods to train valid NBCs for achieving more precise verification results. This could involve advancements in neural network architectures, training algorithms, or optimization techniques.

7.3. Personal Insights & Critique

This paper offers a substantial contribution to the field of DNN-controlled system verification by providing a unified and comprehensive framework. The emphasis on stochasticity is particularly valuable, as it bridges the gap between theoretical verification and real-world uncertainties. The introduction of k-inductive NBCs and simulation-guided training are practical innovations that make the framework more efficient and the results more meaningful.

Strengths:

• Completeness: The framework covers qualitative vs. quantitative, infinite vs. finite time horizons, and linear vs. exponential bounds, offering a very comprehensive set of safety guarantees.
• Practicality: The k-inductive variants address the computational challenge of NBC synthesis, while simulation-guided training directly tackles the issue of bound tightness, both crucial for real-world applicability.
• Rigorous Theoretical Foundation: The detailed theorems provide clear conditions for NBCs and explicit formulas for safety bounds, ensuring the certified nature of the results.
• Empirical Validation: The experiments on classic DNN-controlled systems with varying perturbation radii provide strong evidence of the framework's effectiveness and the benefits of its components.

Potential Issues/Areas for Improvement:

• Generalizability of Simulation-Guided Training: While effective, the simulation-guided training relies on simulations to estimate safety frequencies. The accuracy of these simulation estimates could impact the tightness and potentially the soundness if the simulations are not sufficiently representative or long enough. A deeper analysis of the required simulation length and sampling strategy would be beneficial.
• Computational Cost of Validation: NBC validation often involves interval arithmetic and potentially SMT solvers for checking conditions over continuous state spaces. While Theorem 11 helps, these operations can still be computationally intensive for high-dimensional or very complex DNNs, potentially being a bottleneck for scalability.
• Choice of $k$ and hyperparameters: The optimal choice of $k$ for k-inductive NBCs and other hyperparameters ($k_i$ in the loss function, $\zeta$, $\tau$) can significantly influence synthesis time and bound tightness. The paper acknowledges this for $k$ but a more systematic approach to selecting these parameters could further enhance the framework.
• Interpretability of NBCs: While NBCs provide mathematical proofs, the DNN itself remains a black box. Understanding why a particular NBC works (or fails) might be challenging, limiting insights into the system's vulnerabilities beyond just the numerical bounds.

Transferability: The methods, particularly the CEGIS approach for NBC synthesis with k-induction and simulation-guided loss terms, are highly transferable. They could be applied to:

• Other DNN-controlled systems: Beyond the classic benchmarks, to more complex autonomous systems (e.g., self-driving cars, drone swarms).

• Different types of certificates: The general principle could be extended to synthesize other neural certificates, such as Lyapunov functions for stability or contractivity certificates for robustness, under stochastic settings.

• Hybrid Systems: The approach for discrete-time systems could potentially be adapted for hybrid systems (systems with both continuous and discrete dynamics), which are common in many safety-critical applications.

  Overall, this paper lays a strong foundation for future research in certified AI safety, offering a robust and adaptable methodology for formally reasoning about DNN-controlled systems in uncertain environments.