Pith. sign in

REVIEW 2 major objections 6 minor 1 cited by

Data-Driven Yet Formal Policy Synthesis for Stochastic Nonlinear Dynamical Systems

T0 review · 2 major / 6 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Formal control policies for stochastic nonlinear systems can be synthesized from data samples alone, with probably approximately correct reach-avoid guarantees.

desk verdict Useful data-driven abstraction for nonlinear stochastic systems, but the unproved scaling formula in Eq. (10) can break soundness; fixable with a proper one-dimensional search. read the letter →

arxiv 2501.01191 v3 pith:Q3TDH2OD submitted 2025-01-02 eess.SY cs.SY

Mahdi Nazeri , Thom Badings , Sadegh Soudjani , Alessandro Abate This is my paper · ORCID
classification eess.SYcs.SY MSC 93E2093C1068Q60
keywords data-drivenabstractionintervalMDPstochasticnonlinearsystemsreach-avoidspecificationPACguaranteesbackwardreachabilityClopper-Pearsonpolicysynthesis
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Many real-world control tasks involve nonlinear dynamics with unknown stochastic noise, where classical model-based synthesis is impossible. The paper claims that samples of the system's deterministic part and of its noise are enough to build a finite interval Markov decision process (IMDP) abstraction, and that policies synthesized on this abstraction transfer to the original system with a probably approximately correct (PAC) reach-avoid guarantee. The key result is that, with high confidence over the collected samples, the robust reach-avoid value computed on the IMDP is a lower bound on the true probability of the refined policy on the concrete system. This provides a route to formal, guaranteed controller synthesis from black-box data rather than from a known model.

What carries the argument

The central object is the scaled polytope $R_j(\lambda)$ --- region $R_j$ shrunk or enlarged about its centre --- which defines an abstract action through its backward reachable preimage $\mathrm{Pre}(R_j(\lambda))$. The data-driven mechanism replaces exact preimage computation with the certified underapproximation $A_j(x)=\{y\in R_i : \|J^+(R_i)|x-y|\|_\infty\le r_j(x',\lambda)\}$, where $J^+(R_i)$ is the entry-wise maximum absolute Jacobian of $f$ over $R_i$ and $r_j(x',\lambda)$ is the radius of the largest $L^\infty$ ball contained in $R_j(\lambda)$ around a sampled successor $x'$; Theorem 7 guarantees $A_j(x)\subseteq \mathrm{Pre}(R_j(\lambda))$. On the stochastic side, the Clopper--Pearson confidence interval converts counts of noise samples into per-transition probability intervals valid with confidence $1-\beta$. A probabilistic alternating simulation relation --- a behavioural matching between IMDP and system under a concrete policy --- then lets the abstract robust value compose with the PAC probability intervals to yield the transfer guarantee of Corollary 10.

What would settle it

Fix a scalar system, say $f(x)=ax$ with target interval $R_j=[0,1]$, a voxel away from $x'$, and a sample with $x'\in R_j$; compute $\lambda^+$ from Eq. (10) and the exact $\lambda^\star=\inf\{\lambda: \phi\subseteq A_j(x)\}$ (e.g. by bisection on $r_j(x',\lambda)$). Exhibit any case with $\lambda^+<\lambda^\star$: then the action-enabling step can enable $a_j$ while the target set is too small, invalidating the soundness of the abstraction that Corollary 10 relies on.

Watch

Extended reading notes

Core claim

For a discrete-time nonlinear system $x_{k+1}=f(x_k,u_k)+w_k$ with differentiable $f$, known local Jacobian bounds $J^+(R_i)$, and unknown additive i.i.d. noise $w_k\sim\mathbb{P}$, the paper constructs a finite interval MDP purely from samples of $f$ and of $\mathbb{P}$. Each abstract action $a_j$ in state $s_i$ corresponds to a target polytope $R_j(\lambda_{i\to j})$ scaled around its centre; using the Jacobian bound, every forward sample $(x,u,x')$ with $x'\in R_j(\lambda_{i\to j})$ is inflated into a ball $A_j(x)$ that provably underapproximates the backward reachable set $\mathrm{Pre}(R_j(\lambda_{i\to j}))$ (Theorem 7), and a voxel-covering loop over the region $R_i$ decides when $a_j$ is enabled. Transition probability intervals are obtained by applying the Clopper--Pearson two-sided binomial interval to counts of noise samples (Theorem 9, Eq. (14)). Under the probabilistic alternating simulation relation of Definition 11, Corollary 10 asserts that for every scheduler $\sigma$ of the IMDP there is a policy $\pi$ of the concrete system such that, with probability at least $1-\beta|S|^2|\mathrm{Act}|$ over the samples, $\min_{P\in\mathcal{P}}\Pr^{\mathrm{MI}'}_{\sigma,P}(S_G,S_U,h) \le \Pr^{S}_{\pi}(X_G,X_U,h)$, i.e., the robust reach-avoid value of the abstraction is a lower bound on the true reach-avoid probability.

Load-bearing premise

The whole guarantee rests on the unproven claim that Eq. (10) always produces a scaling factor $\lambda^+$ that overestimates the exact minimal scaling $\lambda^\star$ required for a voxel to be covered, and this can fail when the exact scaling is below 1.

Editorial extensions

If this is right

  • For every IMDP scheduler there exists a concrete policy whose reach-avoid probability is at least the robust IMDP value, with confidence $1-\beta|S|^2|\mathrm{Act}|$ over the sample set (Corollary 10).
  • Increasing the number of noise samples $N$ tightens the Clopper--Pearson intervals and raises the guaranteed reach-avoid probability, as the experiments show.
  • The maximum scaling factor $\Lambda$ trades abstraction richness for performance: setting $\Lambda=1$ drops the guaranteed reach-avoid probability to zero on the pendulum and oscillator benchmarks, while larger $\Lambda$ improves it.
  • Clopper--Pearson intervals dominate the scenario-approach intervals on all three benchmarks, giving higher reach-avoid guarantees with the same number of samples $N=1{,}000$ or $N=10{,}000$.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same alternating-simulation machinery should extend to specifications beyond reach-avoid, such as safety or $\omega$-regular objectives, since the relation preserves PCTL-style properties; the paper's proof route is not specific to reach-avoid arithmetic.
  • Treating the known Jacobian bound $J^+(R_i)$ as a form of model knowledge, a purely sample-only variant would need to estimate these bounds from data, adding a second PAC layer that the current guarantee does not cover.
  • The voxel-covering structure of Algorithm 1 suggests an adaptive refinement extension: when the action-enabling check fails locally, subdividing only the undercovered voxels would improve the action set at lower sample cost than a global refinement.
  • A natural follow-up is to compute upper bounds on the reach-avoid probability as well, converting the one-sided lower-bound certificate into an interval-valued guarantee; the probability-interval machinery already yields both sides of each transition interval.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The manuscript proposes a data-driven abstraction framework for discrete-time nonlinear stochastic systems with additive noise and unknown noise distribution. It constructs an interval MDP (IMDP) by using forward samples of the nominal dynamics to underapproximate backward reachable sets and to decide which abstract actions are enabled, and by using Clopper-Pearson confidence intervals on noise samples to bound transition probabilities. The authors claim PAC-style lower bounds on concrete reach-avoid probabilities via a probabilistic alternating simulation relation, and they demonstrate the method on an inverted pendulum, a nonlinear oscillator, and a car-parking benchmark. The main theoretical claim is Corollary 10: with probability at least max(0, 1 - beta * |S|^2 * |Act|) over the noise samples, the robust reach-avoid value of the IMDP lower-bounds the reach-avoid probability of the refined policy on the original system.

Significance. If the correctness argument were complete, this would be a useful contribution: it extends sampling-based formal abstraction from linear or known dynamics to Lipschitz nonlinear systems with additive stochastic noise, and the use of Clopper-Pearson intervals over the scenario approach is well motivated by tighter empirical intervals. The paper also ships detailed proofs for Theorems 5, 7, and 9, and the experimental section reports abstraction sizes, runtimes, and comparisons in a reproducible way. However, the central soundness claim currently rests on an unproved and, in general, false inequality in Eq. (10). Because that step is load-bearing for the action-enabling procedure, Lemma 13 and Corollary 10 are not established as written.

major comments (2)
  1. [Section 4, Eq. (10)] The displayed inequality lambda+ >= lambda* is asserted without proof and is false in general. For a fixed sample (x, u, x'), the function r_j(x', lambda) is the distance from x' to the boundary of the scaled polytope R_j(lambda), and because R_j(lambda) is defined by the affine inequalities in Definition 2, r_j(x', lambda) is the minimum of affine functions of lambda and hence concave. Eq. (10) uses the secant line through lambda = 1 and lambda = 2. For a concave function the chord lies below the graph on [1,2] and the extrapolated secant lies above the graph outside [1,2]. Consequently, lambda+ is an upper bound on lambda* only when lambda* lies in [1,2]. When the required radius C = ||J^+(Ri) * (|x - c_phi| + delta_phi)||_infinity is below r_j(x',1) (so lambda* < 1) or above r_j(x',2) (so lambda* > 2), Eq. (10) gives lambda+ <= lambda*, and lambda+ can even be negative. Algorithm 1 then computes lambda_i->j = max_phi min_sample lambda+ and can enable an action at a value of lambda_i->j for which the target set R_j(lambda_i->j) is too small to cover the voxel. In that case the premise of Theorem 7 is not met, the inclusion R_i subset of Pre(R_j(lambda_i->j)) can fail, Lemma 13 breaks down, and the soundness underpinning Corollary 10 is invalidated. A correct implementation should compute lambda* by binary search on r_j(x', lambda), or else use a safe overapproximation that is valid on all of [0, Lambda].
  2. [Section 4, Eq. (11) and policy refinement paragraph] The min over samples in Eq. (11), and the subsequent choice of the control input in the policy-refinement paragraph, must be restricted to samples (x, u, x') with x in R_i. As written, Eq. (11) minimizes over all samples in D_K(R_j), and the text says the refined policy chooses the input u attaining the minimal lambda+ over all samples in Eq. (11). If the minimizing sample has x outside R_i, Theorem 7 gives no guarantee that the chosen u steers points in the current voxel into R_j(lambda_i->j), so the refined policy in Eq. (8) may be undefined and condition (2) of Definition 11 may fail. The pseudocode in Algorithm 1 already contains an 'if x in R_i' guard, so this may be a presentation gap rather than an intrinsic flaw, but the formal statements and the policy-refinement argument need to impose the restriction explicitly.
minor comments (6)
  1. [Section 3.1] The sentence 'any underapproximation preserves correction of our abstraction' should read 'preserves the correctness of our abstraction'.
  2. [Section 4, Eq. (10)] The notation r_j(x',1) and r_j(x',2) is used before Definition 6 introduces r_j(x', lambda); please state explicitly that these are the radii from Definition 6 evaluated at lambda = 1 and lambda = 2.
  3. [Appendix B] In the proof of Theorem 5, the maxima are written over x in R^l; this should be over x in R_i, the region under consideration.
  4. [After Corollary 10] The sentence 'The factor of |S|^2 * |Act| in Theorem 10' should refer to Corollary 10, not Theorem 10.
  5. [Section 4] The phrase 'Since union over phi of phi = R_i' is missing the index set; it should read 'Since union over phi in Phi(R_i) of phi equals R_i'.
  6. [Figure 1] The caption uses the notation B^infinity_{r(.)(x')}(x') and A_j(x) without defining the subscript function r(.); aligning this notation with Definition 6 would improve readability.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: the PAC reach-avoid guarantee is assembled from an externally published abstraction theorem and standard confidence intervals, not from the target bound itself.

full rationale

The derivation chain is not circular. Corollary 10 combines Theorem 9 (Clopper-Pearson intervals, proved in the paper from standard binomial bounds) with Theorem 4, stated as 'Policy synthesis (Badings et al., 2023b)' and delegated for proof to prior work. Although Theorem 4 is authored by overlapping researchers and is load-bearing for the concrete-to-abstract value bound, it is an independent published theorem with its own stated assumptions (probabilistic alternating simulation, Definition 11) and does not assume the reach-avoid PAC conclusion; citing it is therefore evidence, not circularity. The data-driven quantities, namely the scaling factors lambda_i->j from Eq. (11) and the probability intervals from Theorem 9, are inputs to the guarantee rather than fitted predictions of the reach-avoid value. The action-enabling overapproximation in Eq. (10) is asserted without proof and may fail outside lambda in [1,2], but that is a soundness and correctness gap, not a circular definition or a fitted-parameter rename. The paper's own stated limitations, including the restriction to additive i.i.d. noise and sensitivity to hyperparameters, do not reveal a circular step. Overall, the core result does not reduce to its inputs by construction, so the circularity score remains low even though self-citation is present and should be kept in mind.

Assumptions & free parameters 4 free parameters · 6 assumptions · 0 invented entities

The central guarantee depends on standard statistical facts (Clopper-Pearson) and on the prior alternating-simulation theorem of Badings et al., plus the paper's own Lipschitz-based underapproximation. No new entities are postulated. The main fragility is the unproved scaling formula in Eq. (10), which is listed as an ad hoc axiom.

free parameters (4)
  • Lambda (maximum scaling factor) = 1.5 (car), 2.0 (pendulum), 3.0 (oscillator)
    Hyperparameter bounding lambda_i->j; controls the number of enabled actions. Chosen per benchmark, not fitted to a target result.
  • N (noise samples per transition) = 1,000 or 10,000
    Determines the tightness of Clopper-Pearson intervals; larger N gives narrower intervals.
  • beta (per-transition confidence error) = intended 0.05/T; text writes 1 - 0.05/T
    Sets the overall PAC confidence through Corollary 10; the text has an inconsistency.
  • Partition and sampling grid sizes = e.g., 40x40 states, 7x7 state samples, 7x21 control samples, 7x7 voxels
    Chosen per benchmark to balance abstraction accuracy and computational cost.
assumptions (6)
  • domain assumption The transition function f is differentiable with bounded first-order partial derivatives, and the noise measure P is absolutely continuous (Assumption 1).
    Needed for the mean value theorem bound in Theorem 5 and for zero-probability boundaries in the abstraction function T.
  • domain assumption An upper bound on the matrix J+(Ri) or a Lipschitz constant of f is known.
    Required to compute the sets Aj(x) in Theorem 7; if the bound is wrong, the underapproximation of the backward reachable set can be unsound.
  • domain assumption Independent sampling access to f and to the i.i.d. noise w is available, with f samples not used for the probability intervals.
    The dataset DK and the noise samples are separate inputs to the abstraction and interval estimation.
  • standard math Clopper-Pearson intervals give valid two-sided confidence bounds for binomial proportions (Theorem 9).
    Standard exact binomial confidence interval, used to bound transition probabilities from N noise samples.
  • domain assumption The probabilistic alternating simulation theorem of Badings et al. (2023b) preserves reach-avoid lower bounds (Theorem 4/14).
    Bridges the IMDP robust value to the concrete system; the theorem is cited from prior work by overlapping authors.
  • ad hoc to paper Equation (10) correctly overapproximates the minimal scaling factor lambda_star for all relevant lambda, and the resulting lambda_i->j yields a sound action-enabling decision.
    This is the fragile step: the assertion is unproved and fails for lambda below 1, which can make the abstraction unsound.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Data-Driven Yet Formal Policy Synthesis for Stochastic Nonlinear Dynamical Systems." pith.science (2026). https://pith.science/paper/Q3TDH2OD

@misc{pith2026250101191,
  author       = {Pith},
  title        = {Pith review of: Data-Driven Yet Formal Policy Synthesis for Stochastic Nonlinear Dynamical Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/Q3TDH2OD}},
  note         = {Machine review of arXiv:2501.01191}
}
read the original abstract

The automated synthesis of control policies for stochastic dynamical systems presents significant challenges. A standard approach is to construct a finite-state abstraction of the continuous system, typically represented as a Markov decision process (MDP). However, generating abstractions is challenging when (1) the system's dynamics are nonlinear, and/or (2) we do not have complete knowledge of the dynamics. In this work, we introduce a novel data-driven abstraction technique for nonlinear Lipschitz continuous dynamical systems with additive stochastic noise that addresses both of these issues. As a key step, we use samples of the dynamics to learn the enabled actions and transition probabilities of the abstraction. We represent abstractions as MDPs with intervals of transition probabilities, known as interval MDPs (IMDPs). These abstractions enable the synthesis of policies for the concrete nonlinear system, with probably approximately correct (PAC) guarantees on the probability of satisfying a specified control objective. Our numerical experiments illustrate the effectiveness and robustness of our approach in achieving reliable control under uncertainty.

Figures

Figures reproduced from arXiv: 2501.01191 by the authors.

Figure 1
Figure 1. Three samples (x, u, x′ ) with x ′ ∈ Rj (λi→j ), and the balls B∞ r(·) (x ′ ) around each x ′ and Aj (x) around each x (shown in gray) for fixed values of λi→j = 0.95 (left) and λi→j = 0.80 (middle). On the right, we show sets Aj (x) for two samples such that voxel ϕ ∈ Φ(Ri) is contained. 4. Data-Driven Underapproximations of Backward Reachable Sets In this section, we compute the enabled actions Act(si) ⊆ Act in ea… view at source ↗
Figure 2
Figure 2. Reach-avoid probabilities PrS π (XG, XU , h) for the car benchmark with (a) probability intervals from Theorem 9 and (b) the approach from Badings et al. (2022), both with N = 10 000 samples. Fig. (c) shows simulated trajectories under the resulting policy from Eq. (8) for our method. trajectory under the resulting policy obtained from Eq. (3). These results confirm that our method yields reliable policies with non-… view at source ↗
Figure 3
Figure 3. Reach-avoid probabilities PrS π (XG, XU , h) for pendulum with (a) probability intervals from Theorem 9 and (b) the approach from Badings et al. (2022), both with N = 10 000 samples. Fig. (c) shows simulated trajectories under the resulting policy from Eq. (8) for our method. −10 −5 0 5 10 x −10 −6 −2 2 6 10 v 0.0 0.2 0.4 0.6 0.8 1.0 1 (a) Clopper-Pearson intervals −10 −5 0 5 10 x −10 −6 −2 2 6 10 v 0.0 0.2 0.4 0.6 … view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: Reach-avoid probabilities PrS π (XG, XU , h) for the oscillator with (a) probability intervals from Theorem 9 and (b) the approach from Badings et al. (2022), both with N = 10 000 samples. Fig. (c) shows simulated trajectories under the resulting policy from Eq. (8) fo…
Figure 5
Figure 5. Figure 5: Reach-avoid probabilities PrS π (XG, XU , h) for all three benchmarks, with a reduced upper bound of Λ = 1 on each λi→j . We use Theorem 9 with N = 10 000 to compute probability intervals. Reach-avoid probabilities and trajectories. First, we present the heatmaps and t…
Figure 6
Figure 6. Figure 6: Reach-avoid probabilities PrS π (XG, XU , h) for car parking with (a) probability intervals from Theorem 9 and (b) the approach from Badings et al. (2022), both with N = 1 000 samples. −3.14 −1.57 0.00 1.57 3.14 θ −2.0 −1.2 −0.4 0.4 1.2 2.0 ω 0.0 0.2 0.4 0.6 0.8 1.0 1 …
Figure 7
Figure 7. Figure 7: Reach-avoid probabilities PrS π (XG, XU , h) for pendulum with (a) probability intervals from Theorem 9 and (b) the approach from Badings et al. (2022), both with N = 1 000 samples. −10 −5 0 5 10 x −10 −6 −2 2 6 10 v 0.0 0.2 0.4 0.6 0.8 1.0 1 (a) Clopper-Pearson interv…
Figure 8
Figure 8. Figure 8: Reach-avoid probabilities PrS π (XG, XU , h) for the oscillator with (a) probability intervals from Theorem 9 and (b) the approach from Badings et al. (2022), both with N = 1 000 samples. 22 [PITH_FULL_IMAGE:figures/full_fig_p022_8.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Beyond Interval MDPs: Tight and Efficient Abstractions of Stochastic Systems

    eess.SY 2025-07 accept novelty 7.0 of 10

    Set-valued MDP abstractions are sound and dominate interval-based abstractions in tightness for any fixed state and disturbance partition, while supporting LP-free control synthesis.

Reference graph

Works this paper leans on

65 extracted references · 57 canonical work pages · cited by 1 Pith paper

  1. [1]

    Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems

    Alessandro Abate, Maria Prandini, John Lygeros, and Shankar Sastry. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Autom., 44 0 (11): 0 2724--2734, 2008

    work page 2008

  2. [2]

    Stochastic omega-regular verification and control with supermartingales

    Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Stochastic omega-regular verification and control with supermartingales. In CAV (3) , volume 14683 of LNCS, pages 395--419. Springer, 2024

    work page 2024

  3. [3]

    Set propagation techniques for reachability analysis

    Matthias Althoff, Goran Frehse, and Antoine Girard. Set propagation techniques for reachability analysis. Annu. Rev. Control. Robotics Auton. Syst., 4: 0 369--395, 2021

    work page 2021

  4. [4]

    Henzinger, Orna Kupferman, and Moshe Y

    Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. Alternating refinement relations. In CONCUR , volume 1466 of LNCS, pages 163--178. Springer, 1998

    work page 1998

  5. [5]

    Tom. M. Apostol. Mathematical Analysis. Addison-Wesley Publishing Company, 5th edition, 1982

    work page 1982

  6. [6]

    Badings, Alessandro Abate, Nils Jansen, David Parker, Hasan A

    Thom S. Badings, Alessandro Abate, Nils Jansen, David Parker, Hasan A. Poonawala, and Mari \" e lle Stoelinga. Sampling-based robust control of autonomous systems with non-gaussian noise. In AAAI , pages 9669--9678. AAAI Press, 2022

    work page 2022

  7. [7]

    Badings, Licio Romao, Alessandro Abate, and Nils Jansen

    Thom S. Badings, Licio Romao, Alessandro Abate, and Nils Jansen. Probabilities are not enough: Formal controller synthesis for stochastic dynamical models with epistemic uncertainty. In AAAI , pages 14701--14710. AAAI Press, 2023 a

    work page

  8. [8]

    Badings, Licio Romao, Alessandro Abate, David Parker, Hasan A

    Thom S. Badings, Licio Romao, Alessandro Abate, David Parker, Hasan A. Poonawala, Mari \" e lle Stoelinga, and Nils Jansen. Robust control for dynamical systems with non-gaussian noise via formal abstractions. J. Artif. Intell. Res., 76: 0 341--391, 2023 b

    work page 2023

Show all 65 references
  1. [9]

    Badings, Licio Romao, Alessandro Abate, and Nils Jansen

    Thom S. Badings, Licio Romao, Alessandro Abate, and Nils Jansen. A stability-based abstraction framework for reach-avoid control of stochastic dynamical systems with unknown noise distributions. In ECC , pages 564--570. IEEE , 2024

    2024

  2. [10]

    Principles of model checking

    Christel Baier and Joost - Pieter Katoen. Principles of model checking. MIT Press, 2008

    2008

  3. [11]

    Herbert, and Claire J

    Somil Bansal, Mo Chen, Sylvia L. Herbert, and Claire J. Tomlin. Hamilton-jacobi reachability: A brief overview and recent advances. In CDC , pages 2242--2253. IEEE , 2017

    2017

  4. [12]

    Adrien Banse, Licio Romao, Alessandro Abate, and Rapha \" e l M. Jungers. Data-driven abstractions via adaptive refinements and a kantorovich metric. CoRR, abs/2303.17618, 2023

    2023 arXiv

  5. [13]

    Formal methods for discrete-time dynamical systems, volume 15

    Calin Belta, Boyan Yordanov, and Ebru Aydin Gol. Formal methods for discrete-time dynamical systems, volume 15. Springer, 2017

    2017

  6. [14]

    Bertsekas and Steven E

    Dimitri P. Bertsekas and Steven E. Shreve. Stochastic Optimal Control: The Discrete-time Case. Athena Scientific, 1978. ISBN 1-886529-03-5

    1978

  7. [15]

    Julien Calbert, Antoine Girard, and Rapha \" e l M. Jungers. Classification of simulation relations for symbolic control. CoRR, abs/2410.06083, 2024

    2024

  8. [16]

    Campi, Algo Car \` e , and Simone Garatti

    Marco C. Campi, Algo Car \` e , and Simone Garatti. The scenario approach: A tool at the service of data-driven decision making. Annu. Rev. Control., 52: 0 1--17, 2021

    2021

  9. [17]

    The use of confidence or fiducial limits illustrated in the case of the binomial

    Charles J Clopper and Egon S Pearson. The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika, 26 0 (4): 0 404--413, 1934

    1934

  10. [18]

    Data-driven abstractions for verification of linear systems

    Rudi Coppola, Andrea Peruffo, and Manuel Mazo Jr. Data-driven abstractions for verification of linear systems. IEEE Control. Syst. Lett. , 7: 0 2737--2742, 2023

    2023

  11. [19]

    Interval markov decision processes with continuous action-spaces

    Giannis Delimpaltadakis, Morteza Lahijanian, Manuel Mazo Jr., and Luca Laurenti. Interval markov decision processes with continuous action-spaces. In HSCC , pages 12:1--12:10. ACM , 2023

    2023

  12. [20]

    Symbolic abstractions from data: A PAC learning approach

    Alex Devonport, Adnane Saoud, and Murat Arcak. Symbolic abstractions from data: A PAC learning approach. In CDC , pages 599--604. IEEE , 2021

    2021

  13. [21]

    Controller synthesis made real: Reach-avoid specifications and linear dynamics

    Chuchu Fan, Umang Mathur, Sayan Mitra, and Mahesh Viswanathan. Controller synthesis made real: Reach-avoid specifications and linear dynamics. In CAV (1) , volume 10981 of LNCS, pages 347--366. Springer, 2018

    2018

  14. [22]

    Leach, and Thomas L

    Robert Givan, Sonia M. Leach, and Thomas L. Dean. Bounded-parameter markov decision processes. Artif. Intell., 122 0 (1-2): 0 71--109, 2000

    2000

  15. [23]

    Data-driven strategy synthesis for stochastic systems with unknown nonlinear disturbances

    Ibon Gracia, Dimitris Boskos, Luca Laurenti, and Morteza Lahijanian. Data-driven strategy synthesis for stochastic systems with unknown nonlinear disturbances. In L4DC , volume 242 of Proceedings of Machine Learning Research, pages 1633--1645. PMLR , 2024 a

    2024

  16. [24]

    Temporal logic control for nonlinear stochastic systems under unknown disturbances

    Ibon Gracia, Luca Laurenti, Manuel Mazo Jr., Alessandro Abate, and Morteza Lahijanian. Temporal logic control for nonlinear stochastic systems under unknown disturbances. CoRR, abs/2412.11343, 2024 b

    2024 arXiv

  17. [25]

    Dimarogonas

    Kazumune Hashimoto, Adnane Saoud, Masako Kishida, Toshimitsu Ushio, and Dimos V. Dimarogonas. Learning-based symbolic abstractions for nonlinear control systems. Autom., 146: 0 110646, 2022

    2022

  18. [26]

    Probabilistic logical characterization

    Holger Hermanns, Augusto Parma, Roberto Segala, Bj \" o rn Wachter, and Lijun Zhang. Probabilistic logical characterization. Inf. Comput., 209 0 (2): 0 154--172, 2011

    2011

  19. [27]

    Garud N. Iyengar. Robust dynamic programming. Math. Oper. Res., 30 0 (2): 0 257--280, 2005

    2005

  20. [28]

    Frew, and Morteza Lahijanian

    John Jackson, Luca Laurenti, Eric W. Frew, and Morteza Lahijanian. Strategy synthesis for partially-known switched stochastic systems. In HSCC , pages 6:1--6:11. ACM , 2021

    2021

  21. [29]

    Data-driven abstraction-based control synthesis

    Milad Kazemi, Rupak Majumdar, Mahmoud Salamati, Sadegh Soudjani, and Ben Wooding. Data-driven abstraction-based control synthesis. CoRR, abs/2206.08069, 2022

    2022 arXiv

  22. [30]

    Nonlinear systems, volume 3

    Hassan K Khalil and Jessy W Grizzle. Nonlinear systems, volume 3. Prentice hall Upper Saddle River, NJ, 2002

    2002

  23. [31]

    Kwiatkowska, Gethin Norman, and David Parker

    Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV , volume 6806 of LNCS, pages 585--591. Springer, 2011

    2011

  24. [32]

    Andersson, and Calin Belta

    Morteza Lahijanian, Sean B. Andersson, and Calin Belta. Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control. , 60 0 (8): 0 2031--2045, 2015

    2015

  25. [33]

    Bisimulation through probabilistic testing

    Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94 0 (1): 0 1--28, 1991

    1991

  26. [34]

    Automated verification and synthesis of stochastic hybrid systems: A survey

    Abolfazl Lavaei, Sadegh Soudjani, Alessandro Abate, and Majid Zamani. Automated verification and synthesis of stochastic hybrid systems: A survey. Autom., 146: 0 110617, 2022 a

    2022

  27. [35]

    Constructing mdp abstractions using data with formal guarantees

    Abolfazl Lavaei, Sadegh Soudjani, Emilio Frazzoli, and Majid Zamani. Constructing mdp abstractions using data with formal guarantees. IEEE Control Systems Letters, 7: 0 460--465, 2022 b

    2022

  28. [36]

    A compositional dissipativity approach for data-driven safety verification of large-scale dynamical systems

    Abolfazl Lavaei, Sadegh Soudjani, and Emilio Frazzoli. A compositional dissipativity approach for data-driven safety verification of large-scale dynamical systems. IEEE Trans. Autom. Control. , 68 0 (12): 0 7240--7253, 2023

    2023

  29. [37]

    Efficient data-driven abstraction of monotone systems with disturbances

    Anas Makdesi, Antoine Girard, and Laurent Fribourg. Efficient data-driven abstraction of monotone systems with disturbances. In ADHS , volume 54 of IFAC-PapersOnLine, pages 49--54. Elsevier, 2021

    2021

  30. [38]

    Calvert, and Luca Laurenti

    Frederik Baymler Mathiesen, Simeon C. Calvert, and Luca Laurenti. Safety certification for stochastic systems via neural barrier functions. IEEE Control. Syst. Lett. , 7: 0 973--978, 2023

    2023

  31. [39]

    Scalable control synthesis for stochastic systems via structural imdp abstractions, 2024

    Frederik Baymler Mathiesen, Sofie Haesaert, and Luca Laurenti. Scalable control synthesis for stochastic systems via structural imdp abstractions, 2024

    2024

  32. [40]

    What are the odds? improving the foundations of statistical model checking

    Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienh \" o ft. What are the odds? improving the foundations of statistical model checking. CoRR, abs/2404.05424, 2024

    2024 arXiv

  33. [41]

    Mitchell

    Ian M. Mitchell. Comparing forward and backward reachability as tools for safety analysis. In HSCC , volume 4416 of LNCS, pages 428--443. Springer, 2007

    2007

  34. [42]

    Formal verification of unknown discrete- and continuous-time systems: A data-driven approach

    Ameneh Nejati, Abolfazl Lavaei, Pushpak Jagtap, Sadegh Soudjani, and Majid Zamani. Formal verification of unknown discrete- and continuous-time systems: A data-driven approach. IEEE Trans. Autom. Control. , 68 0 (5): 0 3011--3024, 2023

    2023

  35. [43]

    Two-sided confidence intervals for the single proportion: comparison of seven methods

    Robert G Newcombe. Two-sided confidence intervals for the single proportion: comparison of seven methods. Statistics in medicine, 17 0 (8): 0 857--872, 1998

    1998

  36. [44]

    Robust control of markov decision processes with uncertain transition matrices

    Arnab Nilim and Laurent El Ghaoui. Robust control of markov decision processes with uncertain transition matrices. Oper. Res., 53 0 (5): 0 780--798, 2005

    2005

  37. [45]

    Data-driven abstractions with probabilistic guarantees for linear PETC systems

    Andrea Peruffo and Manuel Mazo. Data-driven abstractions with probabilistic guarantees for linear PETC systems. IEEE Control. Syst. Lett. , 7: 0 115--120, 2023

    2023

  38. [46]

    The temporal logic of programs

    Amir Pnueli. The temporal logic of programs. In FOCS , pages 46--57. IEEE Computer Society, 1977

    1977

  39. [47]

    Puterman

    Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, 1994

    1994

  40. [48]

    Feedback refinement relations for the synthesis of symbolic controllers

    Gunther Reissig, Alexander Weber, and Matthias Rungger. Feedback refinement relations for the synthesis of symbolic controllers. IEEE Trans. Autom. Control. , 62 0 (4): 0 1781--1796, 2017

    2017

  41. [49]

    Katz, Chelsea Sidrane, Esen Yel, Michael Everett, Mykel J

    Nicholas Rober, Sydney M. Katz, Chelsea Sidrane, Esen Yel, Michael Everett, Mykel J. Kochenderfer, and Jonathan P. How. Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems. CoRR, abs/2209.14076, 2022

    2022 arXiv

  42. [50]

    On the exact feasibility of convex scenario programs with discarded constraints

    Licio Romao, Antonis Papachristodoulou, and Kostas Margellos. On the exact feasibility of convex scenario programs with discarded constraints. IEEE Trans. Autom. Control. , 68 0 (4): 0 1986--2001, 2023

    1986

  43. [51]

    Data-driven verification and synthesis of stochastic systems via barrier certificates

    Ali Salamati, Abolfazl Lavaei, Sadegh Soudjani, and Majid Zamani. Data-driven verification and synthesis of stochastic systems via barrier certificates. Autom., 159: 0 111323, 2024

    2024

  44. [52]

    Measure and Integration

    Dietmar Salamon. Measure and Integration. European Mathematical Society, 2016, 2016

    2016

  45. [53]

    Data-driven abstractions via binary-tree G aussian processes for formal verification

    Oliver Sch \"o n, Shammakh Naseer, Ben Wooding, and Sadegh Soudjani. Data-driven abstractions via binary-tree G aussian processes for formal verification. IFAC-PapersOnLine, 58 0 (11): 0 115--122, 2024

    2024

  46. [54]

    Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes

    Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. , 12 0 (2): 0 921--956, 2013

    2013

  47. [55]

    FAUST \( ^ 2 \) : Formal abstractions of uncountable-state stochastic processes

    Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts, and Alessandro Abate. FAUST \( ^ 2 \) : Formal abstractions of uncountable-state stochastic processes. In TACAS , volume 9035 of LNCS, pages 272--286. Springer, 2015

    2015

  48. [56]

    Stipanovic, Inseok Hwang, and Claire J

    Dusan M. Stipanovic, Inseok Hwang, and Claire J. Tomlin. Computation of an over-approximation of the backward reachable set using subsystem level set functions. In ECC , pages 300--305. IEEE , 2003

    2003

  49. [57]

    Bovy, David Parker, and Nils Jansen

    Marnix Suilen, Thom Badings, Eline M. Bovy, David Parker, and Nils Jansen. Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet, pages 126--154. Springer Nature Switzerland, Cham, 2025. ISBN 978-3-031-75778-5. doi:10.1007/978-3-031-75778-5\\_7

    2025 doi

  50. [58]

    Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem

    Sean Summers and John Lygeros. Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Autom., 46 0 (12): 0 1951--1961, 2010

    1951

  51. [59]

    Verification and Control of Hybrid Systems - A Symbolic Approach

    Paulo Tabuada. Verification and Control of Hybrid Systems - A Symbolic Approach . Springer, 2009

    2009

  52. [60]

    The cost of using exact confidence intervals for a binomial proportion

    Måns Thulin. The cost of using exact confidence intervals for a binomial proportion. Electronic Journal of Statistics, 8 0 (1), January 2014. ISSN 1935-7524. doi:10.1214/14-ejs909

    2014 doi

  53. [61]

    Syscore: Synthesis via stochastic coupling relations

    Birgit van Huijgevoort, Oliver Sch \" o n, Sadegh Soudjani, and Sofie Haesaert. Syscore: Synthesis via stochastic coupling relations. In HSCC , pages 13:1--13:11. ACM , 2023

    2023

  54. [62]

    Wolff, Ufuk Topcu, and Richard M

    Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. Robust control of uncertain markov decision processes with temporal logic specifications. In CDC , pages 3372--3379. IEEE , 2012

    2012

  55. [63]

    Efficient backward reachability using the minkowski difference of constrained zonotopes

    Liren Yang, Hang Zhang, Jean - Baptiste Jeannin, and Necmiye Ozay. Efficient backward reachability using the minkowski difference of constrained zonotopes. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. , 41 0 (11): 0 3969--3980, 2022

    2022

  56. [64]

    Packard, Murat Arcak, and Peter J

    He Yin, Andrew K. Packard, Murat Arcak, and Peter J. Seiler. Finite horizon backward reachability analysis and control synthesis for uncertain nonlinear systems. In ACC , pages 5020--5026. IEEE , 2019

    2019

  57. [65]

    Henzinger, and Krishnendu Chatterjee

    Dorde Zikelic, Mathias Lechner, Thomas A. Henzinger, and Krishnendu Chatterjee. Learning control policies for stochastic systems with reach-avoid guarantees. In AAAI , pages 11926--11935. AAAI Press, 2023

    2023

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.