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.

  • 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.

  • 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.

  • 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.

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.
  • 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.
  • Pointwise discount factors may approach one across initial states, so applying the pointwise result separately does not yield a common γ < 1.
  • Under continuity, measurability, openness, compactness, and a strict uniform probability margin, the paper bounds state-dependent discount factors uniformly away from one.
  • The resulting uniform characterization uses a bounded function v and a common γ, while an auxiliary-function formulation removes the explicit discount factor for implementation.

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.

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.
  • A trajectory starts from an initial state x and is indexed by a disturbance realization π.
  • The safe set X contains the target set Xr, and reach-avoid behavior is defined by reaching Xr while remaining in X.
  • The hitting time is infinite if the target is never reached safely or if the trajectory exits the safe set first.
  • 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.

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.

  • Pointwise verification seeks to show that the probability of reaching Xr while remaining in X is at least a prescribed threshold ǫ from one initial state.
  • The discounted reach-avoid value function is the unique bounded solution to a Bellman equation for each γ ∈(0, 1).
  • A bounded barrier certificate v and γ ∈(0, 1) satisfying the barrier-like inequalities are sufficient for PRA(x0) ≥ǫ.
  • When PRA(x0) >ǫ, a suitable γ and barrier certificate exist, making the pointwise characterization necessary as well as sufficient.
  • The discounted value converges to the reach-avoid probability as γ approaches one, enabling construction of a certificate for a sufficiently large discount factor.
  • For an initial-state set, the pointwise condition may remain non-necessary because each state can require a different discount factor, preventing a common γ < 1.

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.

  • Uniform verification requires the reach-avoid probability to exceed threshold ǫ for every initial state in X0.
  • The objective is to construct a barrier certificate v and common γ ∈(0, 1) satisfying the barrier conditions uniformly over X0.
  • The assumptions require continuous state transitions, measurable disturbance dependence, open safe and target sets, and compactness of X0.
  • A strict margin PRA(x) > ǫ for all x ∈X0 is assumed, with compactness and continuity essential to uniform characterization.
  • Under these assumptions, trajectory measurability makes the hitting time, reach-avoid probability, and discounted value well-defined.

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.

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.

  • For each disturbance realization, the discounted hitting-time payoff is lower semicontinuous with respect to the initial state.
  • The pathwise lower-semicontinuity result transfers to the expected discounted value through Fatou’s lemma.
  • Continuity of finite-horizon trajectories follows from continuous dynamics, while openness of the safe and target sets supports the hitting-time argument.
  • Under Assumption 1, the discounted reach-avoid value eVγ is lower semicontinuous on X0 for every γ ∈(0, 1).

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.

  • The discounted value converges to PRA(x) as γ ↑1, so the strict margin gives each initial state a discount factor with value above ǫ.
  • The uniform discount-factor proof uses the nonemptiness of the threshold set and continuity of the discounted value in γ.
  • The threshold function γǫ is upper semicontinuous, because its strict sublevel sets are relatively open in X0.
  • Compactness of X0 implies the existence of a common ¯γ ∈(0, 1) satisfying eV¯γ(x) > ǫ for every x ∈X0.
  • Without the strict margin, required discount factors may approach one along initial-state sequences, preventing a single γ < 1 from existing.

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.
  • Necessity construction: 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.
  • Necessity construction: 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.
  • 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.
  • Auxiliary-function formulation: 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.
  • 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.

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.
  • 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.
  • 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.
  • 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.
  • Discounted formulation: 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.
  • 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.

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.
  • Future work: Future work will relax the assumptions and develop computational methods for higher-dimensional nonlinear stochastic systems.
Loading 2608.30318v1…