Pith. sign in

REVIEW 3 major objections 5 minor 2 cited by

Data-Driven Certificate Synthesis

T0 review · 3 major / 5 minor · reviewed 2026-08-08 · deepseek-v4-flash

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

Pith's one-line read Sampled trajectories alone can yield reachability, safety, and reach-while-avoid certificates whose PAC risk is set by a compression set, not state dimension.

desk verdict The compression-set construction is genuinely new, but the missing grid-error analysis leaves the PAC certificate guarantee unsupported for the implemented method. read the letter →

arxiv 2502.05510 v3 pith:6PDUVPCD submitted 2025-02-08 eess.SY cs.SY

Luke Rickard , Alessandro Abate , Kostas Margellos This is my paper · ORCID
classification eess.SYcs.SY
keywords certificatesynthesisreachabilitysafetyreach-while-avoidPACguaranteescompressionsetscenarioapproachnon-convexoptimization
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

The paper tries to establish that verification certificates for discrete-time dynamical systems can be learned from a finite collection of trajectories, with no model of the dynamics and no knowledge of its Lipschitz constant. The properties covered are reachability, safety, and reach-while-avoid; for each, a scalar function $V$ is trained by minimizing a loss whose zero value encodes the certificate conditions. The accompanying guarantee, Theorem 1, is PAC in nature: with confidence at least $1-\beta$, the probability that a newly drawn trajectory violates the certificate conditions—and hence the property—is at most $\epsilon(C_N,\beta,N)$, where $C_N$ is the number of training trajectories in a compression set. A compression set is a subset of the data that would produce the exact same certificate as the full dataset, and its size, rather than state dimension, controls the risk bound. The paper also provides the algorithms that construct the certificate and the compression set simultaneously, so the guarantee is usable in practice.

What carries the argument

The central object is the compression set: a subset $C_N$ of the training trajectories which, when used as the algorithm's input, returns the same certificate $V_N$ as the full dataset. Its cardinality $C_N = |C_N|$ enters the risk formula (19), so smaller compression sets give tighter PAC guarantees. Algorithm 1 is the constructive mechanism: it performs subgradient descent on the worst-case loss and, when it finds a training sample whose subgradient is misaligned with the current descent direction, it 'jumps' along that subgradient and adds the sample to $C_N$; the paper proves that this creates a genuine compression set. Algorithm 2 wraps Algorithm 1, discarding each returned compression set from the training pool until the worst-case loss reaches zero, at the cost of a larger final compression set. The loss functions (25)–(27) translate the certificate conditions—initial-set, goal-set, unsafe-set, outside-domain, and along-trajectory decrease constraints—into integrals over the relevant regions, with the integrals approximated in implementation by sums over deterministic grids.

What would settle it

Construct a smooth scalar function whose sampled loss (26) is zero on the deterministic grids described in Section 4.3 but whose true value violates one of the continuous conditions, for example a sublevel well inside $X_G$ that sits between grid points and dips below $-\delta$; existence of such a function would refute the dense-grid implication and hence the premise of Theorem 1. Concretely, one can run the method and then check the returned certificate with a dense adaptive search or global optimizer; any violation found outside the training grid is a direct falsifier.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central claim is a theorem about any certificate-synthesis algorithm that satisfies two structural properties: preference and non-associativity (Assumption 2). Theorem 1 states that if such an algorithm returns a certificate $V_N$ satisfying the certificate conditions on all $N$ sampled trajectories, then, with confidence at least $1-\beta$, the probability that a new trajectory violates those conditions—and therefore the property $\varphi$—is bounded by $\epsilon(C_N,\beta,N)$, the solution of equation (19) evaluated at the compression-set cardinality. The proof routes the violation probability through the probability that a new sample changes the compression set, which the paper controls via a compression-generalization result. The paper then claims that its own Algorithm 1, a subgradient-descent scheme with deliberate jumps triggered by misaligned subgradients, terminates, returns a compression set, and satisfies Assumption 2 (Proposition 4), and that Algorithm 2, which discards compression sets until the loss reaches zero, does the same (Proposition 5). If these propositions hold, the PAC bound applies to the certificates actually constructed in the numerical studies, including the partially unsafe example where classical exact methods cannot give a certificate.

Load-bearing premise

The argument stands on the assumption that a certificate whose discretized loss (26) is zero on a finite grid, with the outside-domain condition checked only on the boundary of $X$, satisfies the exact continuous certificate conditions over the whole state space; the paper states the grid is 'dense enough' but offers no error bound or verification step for that implication.

Editorial extensions

If this is right

  • A direct corollary is that property verification becomes model-free: only sampled trajectories are needed, not the system equations, so the method applies to black-box or simulation-only systems.
  • Because the risk bound depends on compression-set size rather than exponentially on state-space dimension, the guarantees can remain informative for higher-dimensional systems where grid-based and Lipschitz-based scenario bounds become vacuous.
  • The discarding mechanism lets the method produce a probabilistic certificate even when some sampled trajectories enter the unsafe set, a case in which exact certificate synthesis would simply fail.
  • The certificate itself, not just a yes/no property answer, is made available, which the paper identifies as a step toward control synthesis.
  • The compression-set computation is constructive for a non-convex optimization program, extending a mechanism that was previously a general meta-algorithm to a concrete subgradient-descent instance.

Reading between the lines

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

  • The paper leaves implicit that the 'dense enough' grid in Section 4.3 is doing logical work: if a counterexample could hide between grid points, the validity implication from the discretized loss (26) to the continuous conditions (3)–(6) would break, so an error bound or post-hoc verification would turn the method into a fully rigorous one.
  • A testable extension suggested by the framework is to use the learned certificate itself to search for violations: since the certificate defines level sets, one can run a global optimizer over $V$ on each region and check the continuous conditions, converting the grid assumption into a verifiable certificate.
  • The same compression-set construction should transfer to other non-convex learning-with-guarantees tasks beyond dynamical-system verification, because Algorithm 1 only relies on subgradients and a worst-case loss over samples.
  • The PAC guarantee is relative to the distribution of initial conditions used for sampling; an adversarial or unknown initial-state distribution would require additional robustness machinery not present in the paper.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper proposes a data-driven method for synthesizing neural-network certificates for reachability, safety, and reach-while-avoid properties of deterministic discrete-time systems. It encodes certificate conditions as a loss function, introduces Algorithm 1 as a subgradient-descent procedure that simultaneously builds a compression set, and Algorithm 2 as a discarding mechanism to drive the loss to zero. The main theoretical result, Theorem 1, uses compression-based scenario theory to give a PAC-style bound on the probability that a new trajectory violates the certificate conditions and thereby the underlying property. The paper reports numerical experiments on benchmark systems, including a comparison with the scenario-optimization approach of [34], and states that code is publicly available.

Significance. If fully established, the contribution would be significant: it aims to provide model-free probabilistic verification guarantees without requiring Lipschitz constants of the dynamics, and it gives a constructive, iterative mechanism for computing compression sets in a non-convex setting. The explicit comparison with [34] and the availability of code are strengths. The value of the paper is, however, conditional on closing the gap between the continuous certificate conditions used in the theory and the finite, grid-based loss actually minimized in the implementation, and on a correct proof that the discarding algorithm indeed produces a compression set.

major comments (3)
  1. [Section 4.3, Eq. (26)] The replacement of the integrals in (25) by the finite sums in (26), with the exterior-positivity condition checked only on the boundary ∂X, is not supported by any error analysis. The text states that the grid is 'dense enough' but gives no Lipschitz estimate for V_θ and no post-verification step. A continuous function can satisfy (26) and yet violate (5) between grid points, or violate (6) in an arbitrarily thin layer just outside X. Since Theorem 1 and Definition 1 require V to satisfy the continuous conditions ψ_s and ψ_Δ, the implication 'zero discretized loss ⇒ property φ' is not established for the implemented algorithm.
  2. [Section 4.2 and Appendix A.3, Proposition 5(2)] The proof that R_N is a compression set for Algorithm 2 is not valid as written. To show A_2(R_N)=A_2({ξ_i}), the proof re-runs Algorithm 2 on R_N and asserts that the first call to Algorithm 1 returns C_1; however, that first call is fed with R_N rather than the original multiset, and Proposition 4 only guarantees that C_1 is a compression set for the original invocation. No argument is given that Algorithm 1 on R_N produces the same sequence of sets C_i and the same final parameter vector. Without a correct proof that R_N is a compression set, Theorem 1 cannot be invoked with R_N for Algorithm 2.
  3. [Section 3.2, Theorem 1 and Eq. (21)] Theorem 1 is stated under the hypothesis V_N = A({ξ_i}) satisfies ψ_s and all sampled conditions ψ_Δ(ξ_i). Algorithm 2, however, terminates when the loss is zero only on the remaining set D, and samples in R_N are removed precisely because their loss may be positive. The paper does not explain how the final certificate satisfies the theorem's hypothesis, nor why the first inclusion in (21) remains valid for an algorithm that discards violating samples. A separate argument is needed to justify that a new violating trajectory still implies a change of the compression set.
minor comments (5)
  1. [Theorem 1 statement] The notation '⋀_{i=0}^N ψ_Δ(ξ_i)' appears to have an indexing typo; it should presumably be i=1,...,N.
  2. [Section 2.1 and Property 2] Section 2.1 states that X is bounded, while Property 2 says the safety property may be constructed for unbounded X; these statements should be reconciled.
  3. [Section 4.3, Eq. (27)] The sample-dependent loss l_Δ contains the term sup_{x∈X_I} V_θ(x), but the implementation of this supremum over a continuous set is not discussed; presumably it is also discretized, and this should be stated explicitly.
  4. [Section 6.4] The sentence 'the approach of [34] with 10^19 samples results in a confidence of at least 10^{-30}' appears to invert the intended statement; a confidence should be close to one, while a risk level would be small.
  5. [Section 4.3] The phrase 'by Certificate 1' should presumably read 'by Proposition 1'.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular reduction; the PAC guarantee is an external compression/scenario application, with the main caveat being a discretization soundness gap rather than circularity.

full rationale

The claimed derivation chain is not circular. Theorem 1 is a direct application of the external compression/scenario bound of Campi and Garatti [14, Thm. 7]; Assumption 2 is explicitly 'adapted from [14]', and Proposition 4(3) proves that Algorithm 1 satisfies those properties from the algorithm's own deterministic update rule, not by invoking the target guarantee. The compression set follows the standard Definition 2 (a subset reproducing the same output), and the reported risk ε(C_N,β,N) is a posteriori in the observed cardinality; it is not a fitted parameter relabelled as a prediction. The self-citations that appear ([1], [3], [8], [21], [42], [43], [46], among others) occur in related-work, benchmark, or extension contexts and do not carry the load-bearing argument. The principal caveat is a soundness gap, not circularity: Section 4.3 replaces the continuous integrals in (25) with the finite deterministic grid sum (26) and asserts the grid is 'generated densely enough' with no error bound or continuous verification step, while the outside-domain condition is checked only on ∂X; zero value of (26) therefore does not formally certify V|=ψ_s over the whole space, which is the precondition for Theorem 1. That is a missing-support/correctness issue and should be weighed in a correctness review, but it is not an equivalence-by-construction or a self-citation chain, so it does not raise the circularity score beyond the minor self-citation level.

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

The paper introduces no new physical or mathematical entities; compression sets and certificates are borrowed from prior literature. The new component is an algorithm, not an entity. The ledger is dominated by the unverified discretization assumption and the algorithm hyperparameters.

free parameters (4)
  • delta (sublevel threshold) = chosen by hand, no value given
    Design parameter in reachability and RWA certificate conditions (3)-(7) and in the loss (25); must be fixed before learning and affects feasibility of the certificate conditions.
  • Finite grid for state-dependent loss = not specified
    The integrals in (25) are replaced by sums over |X_G|, |X_I|, and |X_domain| grid points; the grid density is chosen in implementation without error analysis, and the outside-X condition is enforced only on the border.
  • Algorithm hyperparameters alpha and eta = not specified
    Subgradient step size and tolerance in Algorithm 1; no theoretical guidance is given for choosing them, and they affect termination, loss value, and compression set size.
  • Neural network architecture = e.g., 2 hidden layers, 5 or 10 neurons, sigmoid activation
    Free modeling choice; the method's guarantees are stated for any parameterized template, but success depends on sufficient expressivity and the architecture is not derived from the theory.
assumptions (5)
  • domain assumption Assumption 1: P{xi}=0 for any xi in Xi
    Ensures no duplicate samples, used in the proofs of Assumption 2 and non-associativity.
  • domain assumption Assumption 2: Algorithm A satisfies Preference and Non-associativity
    Needed for Theorem 1; proved for Algorithm 1 and Algorithm 2, but stated as a generic condition on any algorithm A.
  • domain assumption Assumption 3: Minimizers of max_{xi in D} L(theta,xi) exist for any non-empty D
    Used to prove termination of Algorithm 1; may fail for neural networks with unbounded parameter spaces.
  • standard math Theorem 7 of Campi and Garatti [14] bounding the probability that the compression set changes
    External scenario-approach result used directly in the proof of Theorem 1; not re-derived in the paper.
  • ad hoc to paper The discretized loss (26) accurately represents the continuous loss (25), so zero discrete loss implies the continuous state conditions hold
    This is the main load-bearing gap: no error bound is given, and the outside-X condition is checked only on the boundary.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Data-Driven Certificate Synthesis." pith.science (2026). https://pith.science/paper/6PDUVPCD

@misc{pith2026250205510,
  author       = {Pith},
  title        = {Pith review of: Data-Driven Certificate Synthesis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6PDUVPCD}},
  note         = {Machine review of arXiv:2502.05510}
}
read the original abstract

We investigate the problem of verifying different properties of discrete time dynamical systems, namely, reachability, safety and reach-while-avoid. To achieve this, we adopt a data driven perspective and, using past system trajectories as data, we aim at learning a specific function termed certificate for each property we wish to verify. We seek to minimize a loss function, designed to encompass conditions on the certificate to be learned that encode the satisfaction of the associated property. Besides learning a certificate, we quantify probabilistically its generalization properties, namely, how likely it is for a certificate to be valid (and hence for the associated property to be satisfied) when it comes to a new system trajectory not included in the training data set. We view this problem under the realm of probably approximately correct (PAC) learning under the notion of compression, and use recent advancements of the so-called scenario approach to obtain scalable generalization bounds on the learned certificates. To achieve this, we design a novel algorithm that minimizes the loss function and hence constructs a certificate, and at the same time determines a quantity termed compression, which is instrumental in obtaining meaningful probabilistic guarantees. This process is novel per se and provides a constructive mechanism for compression set calculation, thus opening the road for its use to more general non-convex optimization problems. We verify the efficacy of our methodology on several numerical case studies, and compare it (both theoretically and numerically) with closely related results on data-driven property verification.

Figures

Figures reproduced from arXiv: 2502.05510 by the authors.

Figure 1
Figure 1. Pictorial illustration of the level sets associated [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Pictorial illustration of (a) reachability, (b) safe [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Pictorial illustration of the compression set notio [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: Graphical illustration of Algorithm 1. Proposition 4 implies that we can construct a certificate VN = Vθ ⋆ , while the algorithm that returns this certifi￾cate satisfies Assumption 2 and admits a compression set CN with cardinality CN . As such, Algorithm 1 of￾fers a c…
Figure 5
Figure 5. Figure 5: Comparison of the bounds in Theorem 1 and Propo [PITH_FULL_IMAGE:figures/full_fig_p011_5.png]
Figure 6
Figure 6. Figure 6: Phase plane plot for the dynamical system of (35). [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 8
Figure 8. Figure 8: Surface plot of the safety/barrier certificate. 2 4 4 4 0.01 0.00 0.01 0.02 [PITH_FULL_IMAGE:figures/full_fig_p013_8.png]
Figure 12
Figure 12. Figure 12: Comparison with [34]. The zero-level set of the safety certificate of our approach is dashed; level sets that separate the initial and unsafe sets (i.e. γ- and λ- level sets) from [34] are dotted. For this certificate, we obtained a theoretical risk bound ε = 0.388 (s…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

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

  1. Robustness Certificates for Neural Networks Against Data Poisoning and Evasion Attacks

    cs.LG 2025-12 unverdicted novelty 6.0 of 10

    A neural-network barrier certificate over training trajectories certifies ℓ_p-bounded data-poisoning and evasion budgets, with PAC-style confidence, on MNIST, SVHN, and CIFAR-10.

  2. Multi-Object Sketch Animation with Grouping and Motion Trajectory Priors

    cs.CV 2025-08 unverdicted novelty 6.0 of 10

    GroupSketch animates multi-object vector sketches in two stages: user-guided grouping and keyframes, then a group-based displacement network that uses text-to-video priors for consistent motion.

Reference graph

Works this paper leans on

49 extracted references · 47 canonical work pages · cited by 2 Pith papers

  1. [34]

    Formal Verification of Unknown Discrete- and Continuous-Time Systems: A Data- Driven Approach

    Ameneh Nejati, Abolfazl Lavaei, Pushpak Jagtap, Sadeg h Soudjani, and Majid Zamani. Formal Verification of Unknown Discrete- and Continuous-Time Systems: A Data- Driven Approach. IEEE Trans. Autom. Control., 68(5):3011– 3024, 2023

    work page 2023

  2. [35]

    Campi, and Simone Garatti

    Dario Paccagnan, Marco C. Campi, and Simone Garatti. The Pick-to-Learn Algorithm: Empowering Compression for Tight Generalization Bounds and Improved Post-Training Performance. In NeurIPS, 2023

    work page 2023

  3. [1]

    FOSSIL: A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates Using Neural Networks

    Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe, and Andrea Peruffo. FOSSIL: A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates Using Neural Networks. In HSCC, pages 24:1– 24:11. ACM, 2021

    work page 2021

  4. [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 Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification , pages 395–419, 2024

    work page 2024

  5. [3]

    Model Checking and Strategy Synthesis with Abstractions and Certificates , pages 360–391

    Alessandro Abate, Mirco Giacobbe, Diptarko Roy, and Yannik Schnitzer. Model Checking and Strategy Synthesis with Abstractions and Certificates , pages 360–391. 2025

    work page 2025

  6. [4]

    Ahmed, A

    D. Ahmed, A. Peruffo, and A. Abate. Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers. In Proceedings of TACAS, LNCS 12078 , pages 97–114, 2020

    work page 2020

  7. [5]

    Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada

    Aaron D. Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada. Control Barrier Functions: Theory and Applications. In ECC, pages 3420–3431. IEEE, 2019

    work page 2019

  8. [6]

    Formally Verified Neural Network Control Barrier Certificates for Unknown Systems

    Mahathi Anand and Majid Zamani. Formally Verified Neural Network Control Barrier Certificates for Unknown Systems. IF AC-PapersOnLine, 56(2):2431–2436, 2023

    work page 2023

Show all 49 references
  1. [7]

    Badings, Murat Cubuktepe, Nils Jansen, Sebastia n Junges, Joost-Pieter Katoen, and Ufuk Topcu

    Thom S. Badings, Murat Cubuktepe, Nils Jansen, Sebastia n Junges, Joost-Pieter Katoen, and Ufuk Topcu. Scenario- Based Verification of Uncertain Parametric MDPs. Int. J. Softw. Tools Technol. Transf. , 24(5):803–819, 2022

    2022

  2. [8]

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

    Thom S. Badings, Licio Romao, Alessandro Abate, David Parker, Hasan A. Poonawala, Mari¨ elle Stoelinga, and Nils Jansen. Robust Control for Dynamical Systems with Non- Gaussian Noise via Formal Abstractions. Journal of Artificial Intelligence Research, 76:341–391, 2023

    2023

  3. [9]

    Boyd and Lieven Vandenberghe

    Stephen P. Boyd and Lieven Vandenberghe. Convex Optimization. Cambridge University Press, 2014

    2014

  4. [10]

    Introduction to the Scenario Approach

    Marco Campi and Simone Garatti. Introduction to the Scenario Approach. SIAM Series on Optimization, 2018

    2018

  5. [11]

    Campi and Simone Garatti

    Marco C. Campi and Simone Garatti. The Exact Feasibilit y of Randomized Solutions of Uncertain Convex Programs. SIAM J. Optim. , 19(3):1211–1230, 2008

    2008

  6. [12]

    Campi and Simone Garatti

    Marco C. Campi and Simone Garatti. A Sampling-and- Discarding Approach to Chance-Constrained Optimization: Feasibility and Optimality. Journal of Optimization Theory and Applications , 148(2):257–280, 2011

    2011

  7. [13]

    Campi and Simone Garatti

    Marco C. Campi and Simone Garatti. W ait-and-judge scenario optimization. Math. Program. , 167(1):155–189, 2018

    2018

  8. [14]

    Campi and Simone Garatti

    Marco C. Campi and Simone Garatti. Compression, Generalization and Learning. J. Mach. Learn. Res., 24:339:1– 339:74, 2023

    2023

  9. [15]

    A General Scenario Theory for Nonconvex Optimization and Decision Making

    Marco Claudio Campi, Simone Garatti, and Federico Alessandro Ramponi. A General Scenario Theory for Nonconvex Optimization and Decision Making. IEEE Trans. Autom. Control. , 63(12):4067–4078, 2018

    2018

  10. [16]

    Neural Lyapunov Control

    Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov Control. In NeurIPS, pages 3240–3249, 2019

    2019

  11. [17]

    A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the sum of Observations

    Herman Chernoff. A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the sum of Observations. The Annals of Mathematical Statistics , 23(4):493 – 507, 1952

    1952

  12. [18]

    Frank H. Clarke. Optimization and Nonsmooth Analysis . Society for Industrial and Applied Mathematics, 1990

    1990

  13. [19]

    Counter-example guided synthesis of neural network Lyapunov functions for piecewise linear systems

    Hongkai Dai, Benoit Landry, Marco Pavone, and Russ Tedrake. Counter-example guided synthesis of neural network Lyapunov functions for piecewise linear systems. In CDC, pages 1274–1281. IEEE, 2020

    2020

  14. [20]

    Safe Control With Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction Methods for Robotics and Control

    Charles Dawson, Sicun Gao, and Chuchu Fan. Safe Control With Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction Methods for Robotics and Control. IEEE Trans. Robotics , 39(3):1749–1767, 2023

    2023

  15. [21]

    Fos sil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models

    Alec Edwards, Andrea Peruffo, and Alessandro Abate. Fos sil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models. In HSCC, pages 26:1–26:10. ACM, 2024

    2024

  16. [22]

    W armuth

    Sally Floyd and Manfred K. W armuth. Sample Compression , Learnability, and the Vapnik-Chervonenkis Dimension. Mach. Learn., 21(3):269–304, 1995

    1995

  17. [23]

    Simone Garatti and Marco C. Campi. Risk and complexity in scenario optimization. Math. Program., 191(1):243–279, 2022

    2022

  18. [24]

    Garcia, David M

    Carlos E. Garcia, David M. Prett, and Manfred Morari. Model predictive control: Theory and practice - A survey. Autom., 25(3):335–348, 1989

    1989

  19. [25]

    Hirsch, Stephen Smale, and Robert L

    Morris W. Hirsch, Stephen Smale, and Robert L. Devaney. Differential Equations, Dynamical Systems, and an Introduction to Chaos. 2003

    2003

  20. [26]

    Probability Inequalities for Sums o f Bounded Random Variables

    W assily Hoeffding. Probability Inequalities for Sums o f Bounded Random Variables. Journal of the American Statistical Association, 58(301):13–30, 1963

    1963

  21. [27]

    Stinchcombe, and Halbert White

    Kurt Hornik, Maxwell B. Stinchcombe, and Halbert White . Multilayer feedforward networks are universal approximators. Neural Networks , 2(5):359–366, 1989

    1989

  22. [28]

    Formal Synthesis of Stochastic Systems via Control Barrier Certificates

    Pushpak Jagtap, Sadegh Soudjani, and Majid Zamani. Formal Synthesis of Stochastic Systems via Control Barrier Certificates. IEEE Trans. Autom. Control., 66(7):3097–3110, 2021

    2021

  23. [29]

    Neural Certificates for Safe Control Policies

    W anxin Jin, Zhaoran W ang, Zhuoran Yang, and Shaoshuai Mou. Neural Certificates for Safe Control Policies. CoRR, abs/2006.08465, 2020

    2006 arXiv

  24. [30]

    Kingma and Jimmy Ba

    Diederik P. Kingma and Jimmy Ba. Adam: A Method for Stochastic Optimization. In ICLR (Poster) , 2015

    2015

  25. [31]

    The General Problem of the Stability of Motion

    Alexander Mikhailovich Lyapunov. The General Problem of the Stability of Motion. 1994

    1994

  26. [32]

    On the Connection Between Compression Learning and Scenario Based Single-Stage and Cascading Optimization Problems

    Kostas Margellos, Maria Prandini, and John Lygeros. On the Connection Between Compression Learning and Scenario Based Single-Stage and Cascading Optimization Problems. IEEE Trans. Autom. Control. , 60(10):2716–2721, 2015

    2015

  27. [33]

    Performance Bounds for the Scenario Approach and an Extension to a Class of Non-Convex Programs

    Peyman Mohajerin Esfahani, Tobias Sutter, and John Lygeros. Performance Bounds for the Scenario Approach and an Extension to a Class of Non-Convex Programs. IEEE Transactions on Automatic Control , 60(1):46–58, 2015

    2015

  28. [36]

    On the Construction of Lyapunov Functions Using the Sum of Squares Decomposition

    Antonis Papachristodoulou and Stephen Prajna. On the Construction of Lyapunov Functions Using the Sum of Squares Decomposition. In CDC, pages 3482–3487. IEEE, 2002. 15

    2002

  29. [37]

    Safety Verification o f Hybrid Systems Using Barrier Certificates

    Stephen Prajna and Ali Jadbabaie. Safety Verification o f Hybrid Systems Using Barrier Certificates. In HSCC, volume 2993 of Lecture Notes in Computer Science , pages 477–492. Springer, 2004

    2004

  30. [38]

    Stephen Prajna, Ali Jadbabaie, and George J. Pappas. Stochastic safety verification using barrier certificates. In CDC, pages 929–934. IEEE, 2004

    2004

  31. [39]

    Stephen Prajna, Ali Jadbabaie, and George J. Pappas. A Framework for W orst-Case and Stochastic Safety Verification Using Barrier Certificates. IEEE Trans. Autom. Control. , 52(8):1415–1428, 2007

    2007

  32. [40]

    Model Predictive Control with Reach-avoid Analysis

    Dejin Ren, W anli Lu, Jidong Lv, Lijun Zhang, and Bai Xue. Model Predictive Control with Reach-avoid Analysis. In IJCAI, pages 5437–5445. ijcai.org, 2023

    2023

  33. [41]

    Learning Robust Policies for Uncertain Parametric Markov Decision Processes

    Luke Rickard, Alessandro Abate, and Kostas Margellos. Learning Robust Policies for Uncertain Parametric Markov Decision Processes. In L4DC, volume 242 of Proceedings of Machine Learning Research, pages 876–889. PMLR, 2024

    2024

  34. [42]

    Continuous-time Data-driven Barrier Certificate Synthesi s

    Luke Rickard, Alessandro Abate, and Kostas Margellos. Continuous-time Data-driven Barrier Certificate Synthesi s. CoRR, abs/2503.13392, 2025

    2025 arXiv

  35. [43]

    Badings, Licio Romao, and Alessandro Abate

    Luke Rickard, Thom S. Badings, Licio Romao, and Alessandro Abate. Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics. In QEST, volume 14287 of Lecture Notes in Computer Science , pages 10–29. Springer, 2023

    2023

  36. [44]

    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(4):1986–2001, 2023

    1986

  37. [45]

    Data-Driven Verification and Synthesis of Stochast ic Systems via Barrier Certificates

    Ali Salamati, Abolfazl Lavaei, Sadegh Soudjani, and Ma jid Zamani. Data-Driven Verification and Synthesis of Stochast ic Systems via Barrier Certificates. Autom., 159:111323, 2024

    2024

  38. [46]

    Certified Approximate Reachability (CARe): Formal Error Bounds on Deep Learning of Reachable Sets, 2025

    Prashant Solanki, Nikolaus Vertovec, Yannik Schnitze r, Jasper Van Beers, Coen de Visser, and Alessandro Abate. Certified Approximate Reachability (CARe): Formal Error Bounds on Deep Learning of Reachable Sets, 2025

    2025

  39. [47]

    Learning Certifie d Control Using Contraction Metric

    Dawei Sun, Susmit Jha, and Chuchu Fan. Learning Certifie d Control Using Contraction Metric. In CoRL, volume 155 of Proceedings of Machine Learning Research, pages 1519–1539. PMLR, 2020

    2020

  40. [48]

    W ood and B

    Graham R. W ood and B. P. Zhang. Estimation of the Lipschitz Constant of a Function. 8(1):91–103, 1996

    1996

  41. [49]

    Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysis

    Yujie Yang, Hanjiang Hu, Tianhao W ei, Shengbo Eben Li, and Changliu Liu. Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysis. CoRR, abs/2407.20532, 2024. A Proofs A.1 Certificate Proofs A.1.1 Proof of Proposition 1 – Reachabil...

    2024 arXiv

Pith tools

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