PaperlayerView exact revision on arXiv

Source-linked AI summary

Non-parametric Formal Synthesis of Unknown Stochastic Systems: Asymptotic Convergence Guarantees

Zhi Zhang, Sadegh Soudjani

arXiv:2609.06206v1eess.SYcs.SY

TL;DR

When system dynamics are unknown, whether data-driven satisfaction results converge remains an open question. The paper uses non-parametric estimation to bound abstract transition probabilities and estimate a Lipschitz-constant upper bound, then combines these results to guarantee probabilistic asymptotic convergence of verification results.

  • Problem

    It was unclear whether satisfaction probabilities computed from a data-driven abstraction of an unknown system converge with high confidence to those of the system within a predefined threshold.

    Source: §1 · p. 2, §2.5 · p. 9

  • Method

    The approach uses non-parametric estimation to bound transition probabilities in a finite MDP abstraction, estimate an upper bound on the system's Lipschitz constant, and incorporate these bounds into abstraction-closeness guarantees.

    Source: §1 · p. 3

  • Results

    The framework guarantees probabilistic asymptotic convergence of verification results and asymptotic closeness between the original system and its data-driven finite abstraction.

    Source: §6 · pp. 31–32

  • Takeaways & Limitations

    The resulting synthesis procedure is presented as a reliable approach when the system model is unknown.

    Source: §4.1 · p. 23

    The guarantees assume a sufficiently smooth conditional density, including bounded second-order partial derivatives and bounded mixed third-order partial derivatives.

    Source: §3.1 · p. 10

Abstract

from arXiv · show

Data-driven techniques have shown promising potential for checking behavior of complex systems operating in safety-critical domains against safety and other temporal requirements. This paper studies a class of data-driven techniques that are based on learning a representation of the system from data using non-parametric estimation. The proposed approach is able to formally verify discrete-time stochastic dynamical systems against temporal logic specifications only using observation samples and without the knowledge of the model, and provides a probabilistic guarantee on the satisfaction of the specification. We first consider finite abstract representations of the system in the form of Markov decision processes (MDPs) and derive asymptotic convergence guarantees between the transition probabilities of the abstract MDP and their estimation using Bernstein's inequality and statistical properties of non-parametric estimators. We then propose theoretical results for estimating the asymptotic upper bound of the \emph{Lipschitz constant} (LC) of the stochastic system, which can determine the size of the finite abstract MDP for a given precision error. Under appropriate assumptions, our results prove that the asymptotic convergence rate of the estimations is $O(n^{-1/(3+d)})$ for both the transition probabilities and the LC, where $\mathsf d$ is the dimension of the system and $n$ is the data scale. By integrating these results, we can guarantee the asymptotic closeness in formal verification and policy synthesis performed on the original system and its finite abstraction based on the size of the dataset. Multiple case studies are presented to validate the effectiveness of the proposed method.

1 Introduction

The introduction motivates data-driven formal verification for systems whose black-box dynamics make precise modeling difficult, while noting that convergence foundations remain underdeveloped. It presents non-parametric estimation as a route to asymptotic guarantees for verification and synthesis of unknown stochastic systems.

1 Introduction

  • Data-driven results are stochastic, yet most prior work had not addressed whether formal synthesis results converge, leaving their long-term reliability an open question.Black-box components and unpredictable operating environments also make precise system models challenging to construct.Source: §1 · pp. 1–2
  • Under appropriate assumptions, transition-probability estimates and the estimated Lipschitz-constant upper bound converge at O(n^-1/(3+d)).Here, d is the state dimension and n is the data scale.Source: §1 · p. 2
  • Integrating these estimates with model-based abstraction-closeness bounds yields asymptotically convergent formal synthesis for unknown stochastic systems.The paper frames this as a guarantee for synthesis results on the original system and its finite abstraction.Source: §1 · pp. 2–3
  • Prior methods often assume known dynamics, restrict barrier approaches to particular system classes or known Lipschitz constants, or impose noise and structure assumptions absent here.The introduction also notes that fully unknown-dynamics approaches remain scarce.Source: §1 · pp. 3–4
  • Compared with the earlier conference version, this paper adds convergence results for transition estimates, confidence bounds for the estimated Lipschitz constant, and convergence guarantees for specification-satisfaction probabilities.Source: §1 · p. 4

2 Preliminaries and Problem Statement

This section establishes the stochastic-system and temporal-logic setting, then formulates data-driven verification and synthesis as estimating an unknown system’s behavior from samples and ensuring convergence to its behavior.

2 Preliminaries and Problem Statement

  • A discrete-time stochastic control system has a continuous state space, finite action space, i.i.d. noise, and a measurable state-evolution function.The setup assumes the system is unknown but sampled trajectories are available.Source: §2 · pp. 4–5

2.1 Non-parametric Estimation of Density Functions

  • Kernel estimators use sampled data to estimate densities, while conditional-density estimation represents the next-state distribution given the current state and action.Bandwidth selection balances bias and variance; poor choices can under-smooth or over-smooth.Source: §2.1 · pp. 5–6

2.2 Interval Markov Decision Processes

  • An IMDP represents transition probabilities as intervals rather than fixed values, accommodating uncertainty in the system’s dynamics.An ordinary MDP is the special case in which each interval is a singleton.Source: §2.2 · pp. 6–7

2.3 Probabilistic Computation Tree Logic (PCTL)

  • PCTL expresses stochastic-system requirements using probabilistic and temporal operators, including bounded and unbounded until.Bounded eventually specifies that a property holds within a given number of steps.Source: §2.3 · pp. 7–8

2.4 IMDP Policy Synthesis

  • IMDP synthesis computes lower and upper satisfaction-probability bounds by recursively optimizing over actions and feasible transition distributions.For bounded-until specifications, the recursive computation terminates in finitely many steps.Source: §2.4 · p. 8

2.5 Problem Formulation

  • The problem is to use sampled trajectories and non-parametric estimation to verify and synthesize policies for an unknown system, with high-probability convergence to its behavior as data grows.The system dynamics, noise distribution, and Lipschitz constant are unknown.Source: §2 · p. 5, §2.5 · p. 9

3 Main Results

This section develops nonparametric estimation results for stochastic-system transition probabilities and Lipschitz constants, including a kernel-based LC estimator and asymptotic convergence guarantees. These results support abstractions whose specification-satisfaction probabilities remain close to those of the original system.

3.1 Preparation of the Main Results

  • The analysis assumes uniformly sampled states and sufficiently smooth conditional transition densities, including bounded second-order and mixed third-order derivatives; it also allows non-additive noise.The regularity conditions support the concentration analysis of the non-parametric estimators.Source: §3.1 · pp. 9–10

3.2 Asymptotic Convergence of Transition Probabilities and the Estimated LC

  • O(n^-1/(3+d)) is the transition-probability error convergence rate when bandwidth h=O(n^-1/(6+2d)), under the stated regularity conditions.The confidence bound covers transitions from a state to any set in the specified domain.Source: §3.2 · pp. 14–15
  • The LC estimated from the kernel-based density estimator converges to the true LC with high probability, while a precise bound requires closeness guarantees for third-derivative estimates.A coarse asymptotic upper bound is also available when only loose bounds on higher-order conditional-density derivatives are known.Source: §3.2 · p. 18

3.3 LC Estimation Algorithm and Closeness Guarantee

  • The authors propose an NPE algorithm to estimate the transition-density LC and provide a probabilistic asymptotic bound to guide partitioning for close specification-satisfaction probabilities.The partitioning strategy is discussed in Section 4.Source: §3.3 · p. 19
  • Algorithm 1 samples X uniformly, draws conditional Y samples, estimates the conditional density, and takes the maximum absolute derivative across dimensions; more iterations reduce total variance.The maximum corresponds to the infinity norm; the theoretical results assume uniform sampling, though similar results can be obtained for other distributions.Source: §3.3 · p. 19

3.3.1 Bias of LC Estimation.

  • Under Assumption 1, if h→0 and n h^(2d+2)→∞, LC estimation error converges at O(n^-1/(3+d)), with best epsilon_b,i rate O(n^-2/(3+d)).The stated bandwidth order for that best bias rate is h=O(n^-1/(6+2d)).Source: §3.3.1 · p. 20

4 Construction of IMDP Using Non-parametric Estimation

The section constructs a non-parametric IMDP abstraction from estimated transition intervals, establishes high-probability closeness guarantees, and gives an algorithm for verification and policy synthesis.

4 Construction of IMDP Using Non-parametric Estimation

  • The estimated lower and upper transition-probability bounds over each abstract state form the intervals used to construct the IMDP abstraction.The bounds represent pessimistic and optimistic transition probabilities from states in one abstract state to another under an action.Source: §4 · pp. 20–21

4.1 Closeness Guarantees for the IMDP Verification

  • The satisfaction probabilities of the unknown system and its data-driven abstraction are close with high probability, with closeness converging at O(k n_Q n^-1/(3+d)).Refining the partition and collecting more data can reduce the errors in the guarantee.Source: §4.1 · pp. 22–23
  • The error bound grows linearly with the specification horizon, while handling unbounded until with MDP abstractions requires additional structural assumptions on the dynamics.The stated guarantee is therefore suited to time-bounded specifications.Source: §4.1 · p. 23

4.2 Non-parametric Formal Verification Algorithm

  • The algorithm estimates an LC upper bound, uses it and a target error to set the state-space partition, then computes the specification’s satisfaction probability and a control policy.The stated asymptotic guarantee requires rough values for the parameters in Assumption 1.Source: §4.2 · p. 23

5 Numerical Study

The numerical studies assess transition-probability and Lipschitz-constant estimation, verification, policy synthesis, and comparison with empirical transition-probability estimation.

5.1 Estimation of Transition Probabilities and LC

  • As data scale increases, transition-probability errors diminish and cluster more tightly, and the estimated LC approaches the original value 0.1931.The transition-probability estimate uses Scott’s formula bandwidth, with error of order O(n^-2/(4+d)) with high probability.Source: §5.1 · p. 24
  • Theorem-based bandwidth estimates produce a smoother, more similar CoDF than Scott’s formula, while the LC bound tightens with data and empirical values remain below it.For original LC 0.0968, the bound is [0.057, 0.142] at n=10^5; empirical mean and 99% intervals use 150 runs per data scale.Source: §5.1 · p. 25
  • Under Cauchy noise, the LC bound interval narrows as data scale increases, and all empirical estimates remain within the analytical bounds.The original LC is 0.4135; empirical means and 99% confidence intervals use 100 independent runs per data scale.Source: §5.1 · p. 26

5.2 Case Studies

  • Across verification case studies, increasing data narrows the verification gap, while the maximum satisfaction-probability difference increases with the horizon K.For policy synthesis, satisfaction-probability bounds draw closer and the n=5×10^4 policy more closely matches the model-based result than the n=2×10^4 policy.Source: §5.2 · pp. 26–27

5.3 Comparison with an Alternative Approach

  • For NPE, estimated satisfaction probabilities closely match the original system, while empirical bounds do not narrow significantly under a finer partition.At δ=0.1, NPE also shows greater state-to-state variation than at δ=0.4.Source: §5.3 · pp. 30–31, Figure 10 · p. 30
  • Across data scales 10^4 to 5 × 10^4, under the same heavy-tailed disturbance, proposed NPE consistently achieves verification errors much smaller than the empirical method, and increasing data reduces both methods’ errors.The empirical method uses a 95% confidence level.Source: §5.3 · p. 31

6 Conclusions

The paper proposes a data-driven formal verification and synthesis framework for unknown stochastic systems, with probabilistic asymptotic convergence guarantees. It connects transition-probability bounds and an asymptotic upper bound on the Lipschitz constant to convergence between verification on the original system and its finite abstraction.

6 Conclusions

  • Integrating transition-probability bounds with an asymptotic upper bound on the Lipschitz constant guarantees asymptotic closeness between verification on the original system and its data-driven finite abstraction.The verification results converge asymptotically to a specified value.Source: §6 · pp. 31–32
  • Case studies demonstrate the effectiveness of the proposed data-driven framework.Source: §6 · p. 32
  • Future work aims to improve performance when additional information about the conditional density, such as known moment constraints, is available.Source: §6 · p. 32

A.1 Supplementary of Section 2.1

This supplement reviews kernel-density estimation accuracy and bandwidth and kernel selection. It describes how bandwidth choice affects the bias–variance balance and summarizes common selection approaches.

Accuracy and bandwidth

  • The supplement derives asymptotic bias and variance for the density estimator and states an optimal bandwidth and AMISE convergence rate.It also gives asymptotic bias and variance for a univariate conditional density estimator.Source: §A.1 · pp. 35–36
  • The AMISE depends primarily on bandwidth choice, while the kernel affects it only through characteristics such as the order of its first nonzero moments.Source: §A.1 · p. 35

Kernel choice

  • Different kernels can achieve approximately the same smoothness after bandwidth adjustment; the supplement recommends smooth, unimodal, symmetric kernels while also considering computation and differentiability.Table 1 lists commonly used kernels and their canonical bandwidths.Source: §A.1 · p. 35, Table 1 · p. 35

Bandwidth selection

  • Bandwidth selection approaches include rules of thumb, cross-validation, plug-in methods, and numerical AMISE minimization.Source: §A.1 · p. 35
  • Scott’s formula selects bandwidth for a normal distribution with a specified covariance structure.Source: §A.1 · p. 36
  • Cross-validation selects bandwidth by minimizing an unbiased or approximately unbiased estimate of MISE, while bandwidth-selection methods generally balance bias and variance to avoid under- or over-smoothing.Source: §A.1 · p. 36

B Supplementary of Section 2.5

This supplement describes finite MDP abstraction of a stochastic system and the associated verification-closeness guarantee. The partition size can be selected from a desired error threshold and the system’s horizon and Lipschitz bound.

Finite MDP abstraction

  • The finite MDP partitions the state space, uses representative points to define transition probabilities, and measures partition size by the maximum within-cell distance.Source: B Supplementary of Section 2.5 · p. 36

Closeness guarantee

  • For finite-horizon PCTL specifications, the closeness bound depends on the horizon, partition diameter, Lipschitz constant, and Lebesgue measure of the specification set.Source: B Supplementary of Section 2.5 · p. 36

Choosing the partition

  • Given a desired error threshold, choosing the partition parameter from the horizon, Lipschitz bound, and specification-set measure guarantees absolute satisfaction-probability error below that threshold.Source: B Supplementary of Section 2.5 · p. 36

C SUPPLEMENTARY OF SECTION 3

The supplement develops confidence bounds using density-estimation results and finite-cover arguments. It also states that failure of Assumption 1 yields a weaker result, with larger error bounds than those in the main text.

Scope of the results

  • If Assumption 1 is not satisfied, the supplement gives a weaker result, and the cited error bounds are much larger than the corresponding main-text bounds.Source: C SUPPLEMENTARY OF SECTION 3 · p. 37

Density-estimation bounds

  • The conditional-density estimation lemma assumes uniformly sampled inputs and Gaussian kernels, with each paired output drawn from the conditional density.Source: C SUPPLEMENTARY OF SECTION 3 · p. 37
  • The supplement derives a confidence bound for the conditional-density ratio using an earlier bound on the joint-density estimation error.Source: C SUPPLEMENTARY OF SECTION 3 · p. 38

Transition-probability bounds

  • For transition errors, compact abstract states and a Lipschitz condition support uniform bounds via finite covers and pointwise error bounds.The finite-cover radius is selected using the data scale and the transition-error Lipschitz constant.Source: C SUPPLEMENTARY OF SECTION 3 · pp. 38–39

Uniform bounds

  • The transition-error bounds extend across target states, then across source states and actions, using union bounds and confidence corrections absorbed into an O(log n) term.Source: C SUPPLEMENTARY OF SECTION 3 · pp. 39–40
  • A finite cover over the output domain extends pointwise conditional-density error bounds uniformly when the estimation error is Lipschitz in the output variable.Source: C SUPPLEMENTARY OF SECTION 3 · p. 40
Loading 2609.06206v1…