PaperlayerView exact revision on arXiv

Source-linked AI summary

Converse Barrier Certificates for Set-Based Stochastic Reach-Avoid Verification

Bai Xue, C. -H. Luke Ong

arXiv:2608.30318v1eess.SY

TL;DR

The paper addresses whether the pointwise converse characterization for stochastic reach-avoid verification extends to a set of initial states. It constructs uniform barrier certificates over compact initial sets under continuity and related assumptions, showing that a common discount factor and an alternative auxiliary-function formulation are necessary.

  • Problem

    The open question is whether necessary-and-sufficient barrier-like characterization from a single initial state extends to uniform verification over a compact initial set.

    Source: §I · p. 1

  • Method

    Under continuity, measurability, openness, compactness, and a strict uniform probability margin, the paper uses discounted reach-avoid value functions and a common discount factor to construct uniform certificates.

    Source: C. Necessity of Uniform Barrier-Like… · p. 5

  • Results

    The paper establishes necessary barrier-like conditions with a common γ ∈(0, 1) and also proves necessity for an auxiliary-function formulation without an explicit discount factor.

    Source: §I · p. 2, §V · p. 7

  • Takeaways & Limitations

    The pointwise converse characterization extends to uniform infinite-horizon reach-avoid verification over compact initial sets, with both formulations demonstrated through SOS-based computations.

    Source: §I · p. 2, §V · p. 7

Abstract

from arXiv · show

Recent work established sufficient and necessary barrier-like conditions for infinite-horizon reach-avoid verification of stochastic discrete-time systems from a single initial state. Whether such a converse characterization extends to a set of initial states, however, remains open. In this paper, we answer this question affirmatively for compact initial sets. We consider a uniform reach-avoid specification requiring the reach-avoid probability to exceed a prescribed threshold for every initial state in a compact set. Under appropriate assumptions, including continuous system transitions, together with a strict uniform probability margin, we extend the pointwise converse characterization to the uniform setting.

I. INTRODUCTION

The paper extends necessary-and-sufficient barrier-like reach-avoid verification from a single initial state to compact initial sets. Under continuity, compactness, openness, measurability, and a strict uniform probability margin, it establishes a common certificate characterization.

  • Necessary-and-sufficient barrier-like conditions remove the ambiguity left by sufficient-only certificates in probabilistic reach-avoid verification.Source: §I · p. 1
  • The paper asks whether the pointwise converse characterization extends to a compact set of possible initial states.The uniform setting reflects uncertainty in the initial state, including sensor noise.Source: §I · p. 1
  • Pointwise discount factors may approach one across initial states, so applying the pointwise result separately does not yield a common γ < 1.Source: §I · p. 1
  • Under continuity, measurability, openness, compactness, and a strict uniform probability margin, the paper bounds state-dependent discount factors uniformly away from one.Source: §I · p. 1
  • The resulting uniform characterization uses a bounded function v and a common γ, while an auxiliary-function formulation removes the explicit discount factor for implementation.Source: §I · p. 2

II. PRELIMINARIES

The paper introduces the stochastic discrete-time systems, reach-avoid probability, pointwise characterization, assumptions, and uniform verification problem used in the analysis.

  • The preliminaries define the system dynamics and associated reach-avoid probability before recalling pointwise and uniform verification problems.Source: §II · p. 2

A. Stochastic Systems

The stochastic model uses state dynamics driven by i.i.d. disturbances, with safe and target sets defining reach-avoid behavior through a hitting time and product probability measure.

  • The system is driven by i.i.d. disturbance realizations with distribution Pθ and expectations taken with respect to that distribution.Source: A. Stochastic Systems · p. 2
  • A trajectory starts from an initial state x and is indexed by a disturbance realization π.Source: A. Stochastic Systems · p. 2
  • The safe set X contains the target set Xr, and reach-avoid behavior is defined by reaching Xr while remaining in X.Source: A. Stochastic Systems · p. 2
  • The hitting time is infinite if the target is never reached safely or if the trajectory exits the safe set first.Source: A. Stochastic Systems · p. 2
  • The trajectory probability uses the canonical product measure induced by the i.i.d. disturbance distribution, with PRA(x) fixed at 0 outside X and 1 on Xr.Source: A. Stochastic Systems · p. 2

B. Pointwise Reach-Avoid Verification

Pointwise reach-avoid verification characterizes a probability guarantee through a discounted value function and barrier certificate. Its necessity does not automatically extend uniformly over an initial-state set because the discount factor may depend on the state.

C. Uniform Reach-Avoid Verification

The section formulates uniform reach-avoid verification over a compact initial set and states the assumptions supporting a common barrier certificate.

III. NECESSITY OF UNIFORM REACH-AVOID VERIFICATION

The necessity proof first establishes regularity of the discounted value and then uses the strict margin to obtain one discount factor across the compact initial set.

  • The proof establishes lower semicontinuity of the discounted reach-avoid value and then selects a single γ ∈(0, 1) uniformly over X0.Source: §III · p. 3

A. Lower Semicontinuity of the Discounted Value Function

The discounted reach-avoid value is shown to be lower semicontinuous in the initial state by combining pathwise trajectory regularity with Fatou’s lemma.

B. Existence of a Uniform Discount Factor

The strict probability margin and lower semicontinuity allow state-dependent discount requirements to be bounded uniformly below one on compact X0.

C. Necessity of Uniform Barrier-Like Conditions

The paper proves necessity of uniform barrier-like conditions over compact initial sets by constructing certificates from a common discounted reach-avoid value function. It also establishes necessity for an auxiliary-function formulation that avoids explicit discount-factor bilinearity.

Necessity construction

  • A common discount factor enables the pointwise converse construction to extend uniformly over the compact initial set.The certificate is constructed from the discounted reach-avoid value function associated with this common factor.Source: C. Necessity of Uniform Barrier-Like… · p. 5
  • The Bellman equation supplies the one-step barrier condition, while prescribed value-function bounds supply the remaining certificate conditions.This directly links the discounted reach-avoid value function to the required barrier certificate.Source: C. Necessity of Uniform Barrier-Like… · p. 5
  • Under Assumption 1, there exist a constant γ ∈(0, 1) and a barrier certificate v bounded over X satisfying the uniform barrier-like conditions.The conditions include bounds on the target, unsafe, and non-target safe regions, together with the Bellman-derived one-step condition.Source: C. Necessity of Uniform Barrier-Like… · p. 5

Auxiliary-function formulation

  • The alternative formulation introduces functions v and bounded w whose conditions imply PRA(x0) ≥ǫ for every x0 ∈ X0.Its necessity follows by defining w from the discounted reach-avoid value function.Source: C. Necessity of Uniform Barrier-Like… · p. 5
  • Replacing the explicit discount factor with an auxiliary function yields constraints affine in v and w, avoiding bilinearity when γ and v are jointly optimized.For fixed γ, the original condition is affine in v, but jointly optimizing γ and v is not convex.Source: C. Necessity of Uniform Barrier-Like… · pp. 5–6

Computational domain

  • The barrier-like conditions may be enforced on a computational domain containing the safe set and its one-step successor set rather than all of Rn.This restriction is justified by a switched system that keeps the state fixed after it leaves the safe set.Source: C. Necessity of Uniform Barrier-Like… · p. 6

IV. EXAMPLES

The example applies SOS-based semidefinite programming to search for polynomial barrier certificates and evaluates two barrier-like formulations. Feasibility improves with larger polynomial degree and discount factors closer to one, while the auxiliary-function formulation avoids prescribed-discount sensitivity.

SOS-based computation

  • The example encodes polynomial barrier-certificate constraints as semidefinite programs using sum-of-squares decompositions and solves them with Mosek.Unknown polynomial coefficients are restricted to [-100, 100] for numerical stability.Source: §IV · p. 6

Example setup

  • The system uses polynomial dynamics, semi-algebraic safe and target sets, and a compact initial set for the reach-avoid example.The example specifies the disturbance range and the sets X0, X, Xr, and bX through polynomial inequalities.Source: §IV · p. 6

Empirical validation

  • 0.8445 is the empirical worst-case reach-avoid probability over sampled initial states in the Monte Carlo validation.The study samples initial states and simulates independent disturbed trajectories to estimate reach-avoid probabilities.Source: §IV · p. 6

Discounted formulation

  • For γ = 0.9, no tested polynomial degree yields a feasible certificate, whereas γ closer to one and higher degree improve feasibility.The discounted reach-avoid value function more closely approximates the undiscounted probability as γ increases.Source: §IV · p. 6
  • At γ = 0.999, degree 20 is feasible for all four thresholds through ǫ = 0.83, while γ = 0.9999 enables ǫ = 0.75 at degree 10 and ǫ = 0.80 at degree 14.Larger degrees and discount factors closer to one generally permit less conservative probability thresholds.Source: §IV · pp. 6–7

Auxiliary-function formulation

  • The auxiliary-function formulation requires no prescribed discount factor and is feasible at degree 10 for ǫ = 0.7 and ǫ = 0.75, degree 12 for ǫ = 0.80, and degree 20 for ǫ = 0.83.It avoids the γ sensitivity observed for the discounted formulation and provides feasible certificates at lower degrees for several thresholds.Source: §IV · p. 7

V. CONCLUSION

The paper establishes necessity of two barrier-like formulations for uniform infinite-horizon reach-avoid verification over compact initial sets and demonstrates both through SOS computations. Future work targets weaker assumptions and higher-dimensional nonlinear stochastic systems.

Conclusion

  • Under appropriate assumptions, the paper establishes necessity of discounted and auxiliary-function barrier-like conditions for uniform reach-avoid verification over compact initial sets.The result concerns stochastic discrete-time systems and is demonstrated through SOS-based computations.Source: §V · p. 7

Future work

  • Future work will relax the assumptions and develop computational methods for higher-dimensional nonlinear stochastic systems.Source: §V · p. 7
Loading 2608.30318v1…