Data-Driven Verification under Signal Temporal Logic Constraints

1. INTRODUCTION

• Accurate physical-system models can be difficult to construct, while statistical model checking may require many experiments and handle system uncertainty inefficiently.The introduction also notes that statistical model checking does not handle synthesis problems directly.Source: §1 · p. 1
• Related work spans data-driven STL control, Bayesian inference (Haesaert et al., 2015, 2016), and reinforcement-learning synthesis (Lavaei et al., 2020).The cited literature also includes temporal-logic learning, parameter inference, and approaches to satisfying temporal-logic properties.Source: §1 · p. 1
• The framework combines Bayesian confidence over STL satisfaction with prior system knowledge and collected data for partially unknown, linearly parameterized stochastic models.Its stated contributions also include a less conservative under-approximation of the chance-constraint feasible domain and two numerical approaches for computing feasible parameter sets.Source: §1 · pp. 1–2
• The method under-approximates the feasible parameter set through algebraic inequalities, updates the parameter distribution with data, and relaxes inequalities to reduce conservativeness.Confidence is computed from the feasible set and updated parameter distribution.Source: §1 · p. 2

2. PRELIMINARIES AND PROBLEM FORMULATION

• Process noise affects system dynamics, while measurement noise affects outputs during data collection; the formulation assumes a true parameterized model describes the system.The true parameter is generally unknown.Source: §2 · p. 2

2.1 Data Collection

• Data consist of input-output pairs from repeated experiments, with inputs selectable within an acceptable range.The acceptable data-collection input range may exceed the verification range to provide more precise confidence; the stated assumptions include independent, identically distributed noises uncorrelated with inputs and a known initial state.Source: §2.1 · p. 2

2.2 Stochastic Bayesian Confidence

• The stochastic satisfaction function marks a parameter as satisfying the chance constraint when its property probability meets the threshold 1−δ.The constraint is Pr(M(θ) |= ψ) ≥ 1−δ.Source: §2.2 · p. 2
• Confidence is computed from the posterior parameter distribution by integrating the stochastic satisfaction function over the parameter space.The posterior is conditioned on collected input-output data.Source: §2.2 · p. 3

2.3 Parametric LTI Systems

• The integral is generally difficult to compute analytically, motivating a computational approach for LTI systems with known A and B matrices and Gaussian process and measurement noise.The valid input set is bounded, and both noise types are assumed uncorrelated with input signals.Source: §2.3 · p. 3

2.4 Problem Statement

• The parameterized stochastic models omit measurement noise, and the formulation assumes one model in the family describes the stochastic system.Collected output data are noisy, and prior parameter knowledge may improve the posterior distribution used for confidence.Source: §2.4 · p. 3
• The objective is confidence that a system satisfies an STL property, with the problem statement requiring satisfaction independently of the input value.The property is defined over system trajectories, and the confidence combines Bayesian inference with model-based techniques.Source: §2 · p. 2, §2.4 · p. 3
• The overview distinguishes the initial feasible parameter set from the data-updated posterior used to compute confidence.The posterior is updated from collected input-output data, with prior information also eligible for incorporation.Source: §2.4 · p. 3

3. Bayesian Inference

• The posterior parameter distribution is updated by weighting the prior p(θ) with the likelihood p(D | θ) of the observed input-output data.The likelihood is computed from noisy measurements and the prior represents initial system knowledge.Source: §3 · p. 3
• With process noise, measurements are dependent, so the likelihood is modeled as a joint multivariate Gaussian rather than a product of independent measurement likelihoods.The Gaussian output distribution has a parameter-dependent mean and covariance incorporating process and measurement noise.Source: §3 · pp. 3–4
• For Nexp noisy measurements, the parameter-dependent covariance combines propagated process-noise covariance with measurement-noise covariance.The paper gives the covariance as M(θ)ΣW M(θ)T + ΣE.Source: §3 · p. 4

4.1 Signal Temporal Logic (STL)

• STL formulas combine state predicates, negation, conjunction, and bounded until; checking a formula requires only a finite trajectory up to its horizon.Bounded until requires the second formula to hold at some time in the interval while the first holds throughout the preceding interval.Source: §4.1 · p. 4

4.2 STL Robustness

• Positive STL robustness implies satisfaction, and robustness is computed recursively from the formula structure using min–max operators.For stochastic systems, satisfaction is a Bernoulli random variable and robustness is a real-valued random variable.Source: §4.2 · p. 4

4.3 Under-approximation of STL Constraints

• Chance constraints on STL satisfaction are under-approximated by constraints on atomic predicates, which become algebraic inequalities when trajectory statistics are known.For LTI systems with Gaussian disturbances, states are Gaussian with known mean and covariance; the affine-predicate chance constraint can be written as an affine constraint in the input trajectory.Source: §4.3 · p. 5

4.4 A Less Conservative Approximation

• Intermediate weights make the under-approximation less conservative by enlarging its feasible set, but introduce more variables.Weights can use known probabilities of some predicates to make the approximation more precise.Source: §4.4 · p. 5

5.1 Feasible Set Computation

• Robust linear programming and a dual reformulation characterize constraints that must hold across the full input range; solving them across predicates and time steps yields the feasible parameter set.The dual reformulation removes a universal quantifier using Farkas’ lemma.Source: §5.1 · p. 6
• Confidence is computed by integrating the updated posterior over the feasible parameter set using numerical techniques.The paper presents Monte Carlo sampling and piecewise-affine approximation for this computation.Source: §5.1 · p. 6, §5.2 · p. 6

5.2 Confidence Computation Techniques

• Monte Carlo estimates the confidence integral by sampling feasible parameter points, with optimization able to restrict sampling to a smaller region.The estimate is described as a random variable whose precision depends on the sample count and error choice.Source: §5.2 · p. 6
• The piecewise-affine method linearizes the nonlinear term over polytopic regions; its feasible set recovers the real feasible set in the limit as the number of regions increases.The linearization area can be reduced by optimizing over the constraints to find parameter extremes.Source: §5.2 · pp. 6–7

6. Experimental Results

• The case study used a noisy linear system with true parameter [−0.5, 1]T and tested whether output stayed in [−0.5, 0.5] until reaching [−0.1, 0.1] during [2, 4].The chance constraint used δ = 0.01; the Monte Carlo and PWA feasible sets were computed using 27,947 samples and 25 regions, respectively.Source: §6 · p. 7
• 0.9099 and 0.8962 were the post-data confidence values for Monte Carlo and PWA, up from prior values of 0.0279 and 0.0258, respectively.The posterior used data from 50 consecutive measurements; the paper reports confidence using the uniform prior and updated posterior.Source: §6 · p. 7
• Parameters deep inside the feasible set had high-confidence values with low variance; values were lower and more variable near its edges, and tended toward zero far outside it.The reported pattern applied to both Monte Carlo and PWA confidence computations.Source: §6 · p. 7

• The scheme addresses stochastic systems that lack a precise model but have an available parametric model.Source: §7 · p. 8
• It transforms temporal properties into algebraic inequalities, updates unknown-parameter densities using collected system data, and computes confidence over the feasible parameter domain.Source: §7 · p. 8
• Confidence is computed using Monte Carlo and piecewise affine approximation; future work includes maximum-likelihood input selection and real-time integration of Bayesian data analysis with model-based techniques.Source: §7 · p. 8