Pith. sign in

REVIEW 1 major objections 4 minor 26 references

This survey claims to be the first to organize data-driven formal verification and synthesis for dynamical systems into a single grid of three methodological pillars and three out-of-sample guarantee families.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-07-31 23:13 UTC pith:Q4VPSZ6Q

load-bearing objection Useful survey with a real hole: the three-category guarantee taxonomy does not cover the Bayesian/GP work the paper itself reviews. the 1 major comments →

arxiv 2607.27908 v1 pith:Q4VPSZ6Q submitted 2026-07-30 eess.SY cs.SY

Data-Driven Formal Methods for Complex Dynamical Systems: A Survey

Behrad Samari , Alessandro Abate , Antoine Girard , Majid Zamani , Amy Nejati , Abolfazl Lavaei This is my paper
classification eess.SY cs.SY
keywords data-driven controlformal verificationcontroller synthesisabstraction-based methodsbarrier certificatesPAC guaranteesLipschitz continuitycompositional methods
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The paper tries to establish that the scattered literature on data-driven formal verification and controller synthesis can be coherently organized by three methodological pillars — abstraction-based techniques, functional certificates, and compositional methods — and by three families of out-of-sample guarantees: PAC/scenario-based, Lipschitz-based, and structural-property-based. The survey argues that this organization covers both deterministic and stochastic systems and that it is the first to do so. A sympathetic reader would care because the field has grown to a few hundred articles with no shared map, making it hard to know which method applies when. If the taxonomy is right, newcomers can choose a method by asking which guarantee type they need and which data collection scheme is feasible.

Core claim

The central claim is that every notable direct data-driven approach for formal verification or synthesis of dynamical systems falls into a 3-by-3 grid: abstraction-based, functional-certificate, or compositional methodology on one axis, and PAC/scenario, Lipschitz, or structural-property guarantee on the other. The survey asserts that this classification reveals principled trade-offs — PAC-style guarantees tolerate rare violations and need i.i.d. samples; Lipschitz-based guarantees remove the violation parameter but suffer exponential sample complexity; structural-property methods need only a single trajectory but require known system structure such as linearity or monotonicity. The paper fu

What carries the argument

The organizing device is the taxonomy itself, summarized in Fig. 1: three methodological pillars crossed with three out-of-sample guarantee families. The technical core that carries the classification is the trio of guarantee mechanisms presented in Section 2 — the scenario/PAC bound (Theorem 1), the Lipschitz violation-free bound (Theorem 2), and the structural data-parameterized representation (Theorem 3) — which the survey uses to sort every reviewed result. These mechanisms define what 'formal' means in the data-driven setting: a guarantee that conclusions from finite data extend to unseen data, either with violation/confidence levels, without violations, or with deterministic certainty

Load-bearing premise

The map only works if the 'few hundred articles' from the abstract mostly fall into the paper's three guarantee families; if a large share of the literature lives in the deliberately excluded branches (data-driven reachable-set computation, known-model neural-network verification) or does not sort cleanly into PAC/scenario, Lipschitz, or structural guarantees, the claimed comprehensiveness fails.

What would settle it

Count the papers cited in the survey and those in the excluded topics: if the reachable-set and known-model neural-network verification bodies are comparable in size to the surveyed literature, or if a cluster of published works on conformal-prediction-based safety guarantees cannot be represented as PAC-style without significant reframing, the partition is incomplete.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • If the map is correct, a newcomer can select a method by asking which guarantee type is acceptable and which data collection scheme is feasible, rather than reading through the entire literature.
  • The three guarantee families trade off strength against data requirements: PAC-style methods are most flexible but tolerate violations; Lipschitz methods remove violations but scale exponentially; structural methods need only one trajectory but require known structure.
  • Stochastic systems are inherently harder because system noise adds a probability layer on top of the sampling confidence, and the survey shows this literature is thinner and less mature.
  • The eight research avenues identify concrete gaps, such as data-driven construction of infinite abstractions for networks and for stochastic systems, and k-inductive certificates with noisy data.
  • The exclusions in Section 1.6 define a boundary: data-driven reachable-set computation and known-model neural-network verification are set aside, implying the surveyed field is specifically about unknown dynamics with formal out-of-sample guarantees.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The grid suggests hybrid opportunities: combining Lipschitz-based violation-free guarantees with structural data-parameterized representations might reduce sample complexity while preserving determinism, a direction the survey does not explicitly develop.
  • The paper's own exclusions imply that data-driven reachable-set computation and known-model neural-network verification are mature enough to warrant dedicated surveys; if those bodies are actually smaller than the surveyed one, the 'first survey' claim is stronger than the field's maturity justifies.
  • The taxonomy invites a quantitative test: classify all cited articles into the 3-by-3 cells and count how many occupy exactly one cell versus multiple, which would reveal whether the grid is a clean partition or a convenient approximation.
  • The 'first survey' claim is time-sensitive; the map itself may become the standard organization, which could be checked by whether subsequent papers adopt the three-family taxonomy.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 4 minor

Summary. This survey organizes the literature on data-driven formal verification and controller synthesis for deterministic and stochastic dynamical systems. It proceeds along three methodological pillars — (in)finite abstractions, functional certificates (barrier, k-inductive, and closure certificates), and compositional techniques — and classifies out-of-sample guarantees into PAC/scenario-based, Lipschitz-based, and structural-property-based families. Sections 2–8 review direct and selected indirect data-driven methods, state the main theorems with explicit attribution to the original sources, and conclude with eight research avenues. The paper's central claim is that it is the first survey to combine these lenses and to map the field along the axes of Fig. 1.

Significance. If the organizational claim is correct, the survey fills a clear need: the field is fragmented across method-specific papers, and the three-pillar/three-guarantee map together with the eight research avenues would genuinely help new researchers and expose gaps. The manuscript is careful in attributing theorems to prior work, distinguishes deterministic from stochastic settings, and provides useful schematic figures. The main weakness is that the three-category guarantee taxonomy is not exhaustive for works that the survey itself includes: GP/Bayesian methods reviewed in §3.3, §4.1, and §6.1 provide guarantees that do not fall into PAC/scenario, Lipschitz, or structural-property categories. The 'first systematic survey' claim therefore needs either an additional guarantee family or an explicit scope restriction.

major comments (1)
  1. [Abstract, §1.6, Fig. 1 vs. §3.3, §4.1, §6.1] The survey's central organizing claim is that data-driven guarantees fall into three categories: PAC/scenario, Lipschitz-based, and structural-property-based. However, the survey itself reviews Bayesian/GP-based methods whose guarantees are none of these. Jackson et al. (2020) and Skovbekk et al. (2025) in §3.3 are described as providing 'Bayesian-based probabilistic guarantees'; Jackson et al. (2021), Reed et al. (2023), and Schön et al. (2024, 2025) in §6.1 rely on Bayesian credible sets or posterior guarantees; §4.1 surveys GP-based safety certificates with confidence-level guarantees. These are not distribution-free finite-sample violation bounds, do not use covering-radius or Lipschitz-margin conditions, and do not exploit data-parameterized representations or monotonicity. Since §1.1 explicitly includes selected indirect approaches for completeness, these works are inside the surve
minor comments (4)
  1. [§5, first paragraph] The phrase 'we first clarify that why the data-driven studies' should read 'clarify why'.
  2. [§2.2, Theorem 2] The function κ and its inverse are invoked in condition (6) but are not defined or described beyond a pointer to external remarks. Since Theorem 2 is a template for later sections, at least one sentence stating the role of κ — e.g., that it encodes the sampling distribution and geometry of X — should appear in the main text for self-containedness.
  3. [Fig. 6(c)] The figure illustrates the structural-property-based approach only through data-parameterized representations, but Section 2.3 also includes monotonicity-based methods. Adding a subpanel or caption note for the monotonicity case would make the figure consistent with the taxonomy.
  4. [§6, Eq. (47)-(49)] The Chebyshev-based empirical approximation introduces a confidence level ¯ε2, but no guidance is given on how to choose ˆN, ¯ε, and ¯ε2 in practice. A reference to a concrete concentration bound or sample-complexity expression would help readers apply the template.

Circularity Check

0 steps flagged

No significant circularity: the survey organizes external literature and reproduces cited theorems; no prediction reduces to its inputs.

full rationale

This manuscript is a survey rather than a derivation. Its central claims — that it is the first survey systematically organizing data-driven formal verification and synthesis, and that guarantees can be grouped into PAC/scenario, Lipschitz, and structural classes — are organizational claims supported by the surveyed external literature and by explicit comparison with prior surveys (Martin et al. 2023; De Persis & Tesi 2023). Theorems 1–10 are presented as adaptations of previously published results with stated assumptions; even when the cited works include current authors, these citations function as pointers to independent, parameter-free results, not as load-bearing self-citations that establish a novel conclusion. No fitted parameter is renamed as a prediction, no ansatz is justified solely by a self-citation, and no uniqueness theorem from the authors is invoked to force a choice. The noted inconsistency that some reviewed Bayesian/GP works do not sort into the three stated guarantee families is a classification/completeness issue, not a circularity: the manuscript does not define its categories in terms of the works it excludes. Accordingly, no specific circular reduction can be quoted, and the honest finding is no circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 7 axioms · 0 invented entities

Free parameters: none, the survey fits no numbers; all constants (epsilon1, epsilon2, delta, L, rho) belong to the surveyed frameworks, not to the survey's own claim. Invented entities: none, the 'three pillars' and 'three guarantee families' are classification constructs, not postulated objects. The axioms are the load-bearing premises: domain assumptions inherited from the surveyed methods, plus two ad-hoc-to-paper choices (taxonomy exhaustiveness and scope exclusions) that the comprehensiveness claim depends on. The survey itself flags several of these, e.g., i.i.d. data being simulator-suited and the Section 1.6 exclusions.

axioms (7)
  • domain assumption Samples can be drawn i.i.d. from the state space, or the system can be re-initialized for grid-based coverage
    Scenario/PAC guarantees (Theorem 1) assume i.i.d. samples; Lipschitz guarantees (Theorem 2) assume grid coverage (5). Sections 2.1-2.2, Fig. 6(a)-(b). The survey notes this is simulator-suited.
  • domain assumption Lipschitz constants of the constraint function h(x,d) (and of f) are known
    Theorem 2 and the barrier-certificate SCP in Section 4.1 (Theorem 7) require Lipschitz constants L, L1, Lf; without them the violation-free guarantee cannot be evaluated.
  • domain assumption Complete finite abstractions require incremental input-to-state stability (delta-ISS), which for linear systems is stability
    Section 3.2 states the existence of an SF to a complete abstraction is guaranteed under delta-ISS (Definition 5); this restricts the class of systems the surveyed abstraction methods cover.
  • domain assumption Persistency-of-excitation rank condition on collected data (Assumption 1, rank([O;I]) = n+m)
    Section 2.3, Assumption 1: the data-parameterized representation (Theorem 3) is valid only if data are sufficiently rich; noise-free data are also assumed.
  • domain assumption Known dictionary M(x) for polynomial/input-affine systems (Assumption 2)
    Section 4, Assumption 2: the unknown dynamics f(x) = A*M(x) require the user to know which monomials appear; an upper bound on the degree suffices, per Remark 9.
  • ad hoc to paper The three-category guarantee taxonomy (PAC/scenario, Lipschitz, structural) is exhaustive for the surveyed literature
    Section 1.5 and Fig. 1 impose the partition; the survey does not prove exhaustiveness and even excludes data-driven reachability computation (Section 1.6), so coverage of the claimed 'few hundred articles' rests on this classification choice.
  • ad hoc to paper Excluded topics (data-driven reachable-set computation; verification with known dynamics) do not belong in a coherent survey of data-driven formal methods
    Section 1.6: 'fall outside the scope of this survey and are not reviewed here...'; the comprehensiveness claim in the abstract depends on this scope decision being accepted.

pith-pipeline@v1.3.0-daily-deepseek · 48828 in / 17250 out tokens · 150641 ms · 2026-07-31T23:13:31.844137+00:00 · methodology

0 comments
read the original abstract

Data-driven approaches with formal guarantees have recently emerged as a powerful means for the verification and controller synthesis of complex dynamical systems. Interest in these methods is rapidly growing, as system models are often unavailable in practice, and challenges such as nonlinear behavior, uncertainty, and the curse of dimensionality typically render accurate modeling infeasible. These difficulties motivate leveraging limited data collected from the system while still providing formal guarantees on its overall behavior. The community has therefore proposed a few hundred articles on the development of data-driven frameworks that enable the formal verification and synthesis of dynamical systems without explicit models, addressing complex specifications beyond stability. Despite this rapid growth, existing results remain scattered and lack a coherent organization, limiting a clear understanding of their principles, distinctions, and practical potential. This survey fills this gap by providing a comprehensive overview of these data-driven methods for both deterministic and stochastic dynamical systems. We structure the literature around three main methodological pillars in formal methods: (in)finite-abstraction-based techniques, functional certificate approaches, such as control barrier certificates, and compositional methods. For each of these approaches, we classify the resulting data-driven guarantees into three main categories: (i) statistical guarantees grounded in probably approximately correct and scenario-based frameworks, (ii) guarantees derived from Lipschitz continuity, and (iii) guarantees exploiting structural properties. While the literature on deterministic systems is considerably richer, we also devote particular attention to the stochastic counterpart, highlighting the inherent differences and challenges that arise compared to the deterministic case.

Figures

Figures reproduced from arXiv: 2607.27908 by Abolfazl Lavaei, Alessandro Abate, Amy Nejati, Antoine Girard, Behrad Samari, Majid Zamani.

Figure 1
Figure 1. Figure 1: Roadmap of the survey, providing a summary of the considered system types, mathematical tools studied, and primary [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Conceptual comparison of indirect and direct data– [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: General schematic of data-driven abstraction-based approaches, where symbols associated with the ROM are denoted [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Illustration of a barrier certificate: The blue dashed [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Overall diagram of data-driven functional certificate approaches, illustrated using control barrier certificates as a [PITH_FULL_IMAGE:figures/full_fig_p006_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Schematic illustration of three main data collection approaches associated with the data-driven frameworks providing [PITH_FULL_IMAGE:figures/full_fig_p008_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Construction of a finite MDP for a stochastic dynam [PITH_FULL_IMAGE:figures/full_fig_p034_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Illustration of an IMC. tion probability matrix that defines a finite Markov deci￾sion process (MDP) (Lavaei, Soudjani, Abate & Zamani 2022); see also [PITH_FULL_IMAGE:figures/full_fig_p035_8.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

26 extracted references · 8 linked inside Pith

  1. [1]

    & Roy, D

    Abate, A., Giacobbe, M. & Roy, D. (2024), Stochastic omega- regular verification and control with supermartingales,in ‘Proceedings of International Conference on Computer Aided Verification’, Springer, pp. 395–419. Agrawal, A. & Sreenath, K. (2017), Discrete control bar- rier functions for safety-critical control of discrete systems with application to bi...

    arXiv 2024

  2. [6]

    & Jungers, R

    Calbert, J., Girard, A. & Jungers, R. M. (2026), ‘Character- izing simulation relations through control architectures in abstraction-based control’,Automatica190. Campi, M. C. & Garatti, S. (2008), ‘The exact feasibility of randomized solutions of uncertain convex programs’, SIAM Journal on Optimization19(3), 1211–1230. Campi, M. C. & Garatti, S. (2011), ...

    2026

  3. [14]

    B., Lahijanian, M

    Mathiesen, F. B., Lahijanian, M. & Laurenti, L. (2024), ‘IntervalMDP.jl: Accelerated value iteration for inter- val Markov decision processes’,IF AC-PapersOnLine 58(11), 1–6. Mazo Jr, M., Davitian, A. & Tabuada, P. (2010), Pessoa: A tool for embedded controller synthesis,in‘Proceedings of International Conference on Computer Aided Verifica- tion’, Springe...

    Pith/arXiv arXiv 2024

  4. [32]

    F., Akametalu, A

    Fisac, J. F., Akametalu, A. K., Zeilinger, M. N., Kay- nama, S., Gillula, J. & Tomlin, C. J. (2019), ‘A general safety framework for learning-based control in uncertain robotic systems’,IEEE Transactions on Automatic Con- trol64(7), 2737–2752. Gadginmath, D., Krishnan, V. & Pasqualetti, F. (2024), ‘Data-driven feedback linearization using the Koopman gene...

    2019

  5. [56]

    & Arcak, M

    Devonport, A., Saoud, A. & Arcak, M. (2021), Symbolic ab- stractions from data: A PAC learning approach,in‘Pro- ceedings of the 60th IEEE Conference on Decision and Control’, pp. 599–604. Dhiman, V., Khojasteh, M. J., Franceschetti, M. & Atanasov, N. (2023), ‘Control barriers in Bayesian learn- ing of system dynamics’,IEEE Transactions on Automatic Contro...

    Pith/arXiv arXiv 2021

  6. [58]

    J., Camlibel, M

    van Waarde, H. J., Camlibel, M. K., Eising, J. & Trentelman, H. L. (2023), ‘Quadratic matrix inequalities with appli- cations to data-based control’,SIAM Journal on Control and Optimization61(4), 2251–2281. van Waarde, H. J., Camlibel, M. K. & Mesbahi, M. (2020), ‘From noisy data to feedback controllers: Nonconservative design via a matrix S-lemma’,IEEE T...

    2023

  7. [100]

    & Zamani, M

    Nadali, A., Murali, V., Trivedi, A. & Zamani, M. (2024), Neural closure certificates,in‘Proceedings of the AAAI Conference on Artificial Intelligence’, Vol. 38, pp. 21446– 21453. Nadali, A., Trivedi, A. & Zamani, M. (2023), Transfer learn- ing for barrier certificates,in‘Proceedings of the 62nd IEEE Conference on Decision and Control’, pp. 8000–

    2024

  8. [121]

    & Kapoor, A

    Luo, W., Sun, W. & Kapoor, A. (2020), ‘Multi-robot colli- sion avoidance under uncertainty with probabilistic safety barrier certificates’,Advances in Neural Information Pro- cessing Systems33, 372–383. Luppi, A., Bisoffi, A., De Persis, C. & Tesi, P. (2024), ‘Data- driven design of safe control for polynomial systems’,Eu- ropean Journal of Control75. Mak...

    2020

  9. [175]

    Berberich, J., K¨ ohler, J., M¨ uller, M. A. & Allg¨ ower, F. (2020), ‘Data-driven model predictive control with sta- bility and robustness guarantees’,IEEE Transactions on Automatic Control66(4), 1702–1717. Berger, G. O. & Jungers, R. M. (2025), ‘PAC learnability of scenario decision-making algorithms: Necessary con- ditions and sufficient conditions’,IE...

    2020

  10. [189]

    Campi, M. C. & Garatti, S. (2023), ‘Compression, general- ization and learning’,Journal of Machine Learning Re- search24(339), 1–74. Campi, M. C., Garatti, S. & Prandini, M. (2009), ‘The sce- nario approach for systems and control design’,Annual Reviews in Control33(2), 149–157. Campi, M. C. & Weyer, E. (2002), ‘Finite sample properties of system identifi...

    Pith/arXiv arXiv 2023

  11. [316]

    G., Fridman, E

    Rueda-Escobedo, J. G., Fridman, E. & Schiffer, J. (2022), ‘Data-driven control for linear discrete-time de- lay systems’,IEEE Transactions on Automatic Control 67(7), 3321–3336. Sadraddini, S. & Belta, C. (2018), Formal guarantees in data- driven model identification and control synthesis,in‘Pro- ceedings of the 21st International Conference on Hybrid Sys...

    Pith/arXiv arXiv 2022

  12. [438]

    & Zamani, M

    Lavaei, A., Somenzi, F., Soudjani, S., Trivedi, A. & Zamani, M. (2020), Formal controller synthesis for continuous- space MDPs via model-free reinforcement learning,in ‘Proceedings of ACM/IEEE 11th International Confer- ence on Cyber-Physical Systems’, pp. 98–107. Lavaei, A., Soudjani, S., Abate, A. & Zamani, M. (2022), ‘Automated verification and synthes...

    arXiv 2020

  13. [492]

    N., R¨ uffer, B

    Dashkovskiy, S. N., R¨ uffer, B. S. & Wirth, F. R. (2010), ‘Small gain theorems for large scale systems and construc- tion of ISS Lyapunov functions’,SIAM Journal on Control and Optimization48(6), 4089–4118. Dawson, C., Gao, S. & Fan, C. (2023), ‘Safe control with learned certificates: A survey of neural Lyapunov, barrier, and contraction methods for robo...

    2010

  14. [1179]

    & Coogan, S

    Santoyo, C., Dutreix, M. & Coogan, S. (2021), ‘A barrier function approach to finite-time stochastic system verifi- cation and control’,Automatica125. Saoud, A. & Arcak, M. (2024), ‘Characterization, verifica- tion and computation of robust controlled invariants for monotone dynamical systems’,Mathematics of Control, Signals, and Systems36(1), 71–100. Sca...

    arXiv 2021

  15. [1698]

    Antoulas, A. C. (2005),Approximation of Large-Scale Dy- namical Systems, SIAM. Arcak, M., Meissen, C. & Packard, A. (2016),Networks of Dissipative Systems: Compositional Certification of Sta- bility, Performance, and Safety, Springer. Ashoori, M., Aminzadeh, A., Nejati, A. & Lavaei, A. (2025), ‘Physics-informed data-driven control of nonlinear poly- nomia...

    Pith/arXiv arXiv 2005

  16. [1848]

    Wang, Z., Jungers, R. M. & Ong, C. J. (2023), ‘Computation of invariant sets via immersion for discrete-time nonlinear systems’,Automatica147. Wieland, P. & Allg¨ ower, F. (2007), ‘Constructive safety us- 50 ing control barrier functions’,IF AC Proceedings Volumes 40(12), 462–467. Willems, J. C., Rapisarda, P., Markovsky, I. & De Moor, B. L. (2005), ‘A no...

    Pith/arXiv arXiv 2023

  17. [2054]

    & Cort´ es, J

    Haseli, M. & Cort´ es, J. (2022), ‘Learning Koopman eigen- functions and invariant subspaces from data: Symmet- ric subspace decomposition’,IEEE Transactions on Au- tomatic Control67(7), 3442–3457. Hashimoto, K., Saoud, A., Kishida, M., Ushio, T. & Di- marogonas, D. V. (2022), ‘Learning-based symbolic ab- stractions for nonlinear control systems’,Automati...

    Pith/arXiv arXiv 2022

  18. [2138]

    & G¨ ossler, G

    Mouelhi, S., Girard, A. & G¨ ossler, G. (2013), CoSyMA: A tool for controller synthesis using multi-scale abstractions, in‘Proceedings of the 16th ACM International Conference on Hybrid Systems: Computation and Control’, pp. 83–88. Murali, V., Trivedi, A. & Zamani, M. (2022), ‘A scenario approach for synthesizingk-inductive barrier certificates’, IEEE Con...

    2013

  19. [2215]

    A., Alanwar, A

    Oumer, M. A., Alanwar, A. & Zamani, M. (2025), Data- driven safety verification using barrier certificates and ma- trix zonotopes,in‘Proceedings of the 64th IEEE Confer- ence on Decision and Control’, pp. 3913–3918. Oymak, S. & Ozay, N. (2019), Non-asymptotic identification of LTI systems from a single trajectory,in‘Proceedings of IEEE American Control Co...

    2025

  20. [2250]

    & Jungers, R

    Banse, A., Romao, L., Abate, A. & Jungers, R. (2023a), Data-driven memory-dependent abstractions of dynami- cal systems,in‘Proceedings of the 5th Annual Learning for Dynamics & Control Conference’, Vol. 211 ofProceed- ings of Machine Learning Research, PMLR, pp. 891–902. Banse, A., Romao, L., Abate, A. & Jungers, R. M. (2023b), Data-driven abstractions vi...

    2025

  21. [3423]

    & Vovk, V

    Shafer, G. & Vovk, V. (2008), ‘A tutorial on conformal pre- diction’,Journal of Machine Learning Research9(3). Shakouri, A., van Waarde, H. J. & Kanat Camlibel, M. (2025), ‘A new perspective on Willems’ fundamental lemma: Universality of persistently exciting inputs’,IEEE Control Systems Letters9, 583–588. Sheeran, M., Singh, S. & St ˚ almarck, G. (2000),...

    2008

  22. [3894]

    & Pappas, G

    Girard, A. & Pappas, G. J. (2007), ‘Approximation metrics for discrete and continuous systems’,IEEE Transactions on Automatic Control52(5), 782–798. 45 Girard, A. & Pappas, G. J. (2009), ‘Hierarchical control system design using approximate simulation’,Automatica 45(2), 566–571. Givan, R., Leach, S. & Dean, T. (2000), ‘Bounded-parameter Markov decision pr...

    2007

  23. [4946]

    & Lahijanian, M

    Reed, R., Laurenti, L. & Lahijanian, M. (2023), ‘Promises of deep kernel learning for control synthesis’,IEEE Control Systems Letters7, 3986–3991. Reed, R., Laurenti, L. & Lahijanian, M. (2025), Error bounds for Gaussian process regression under bounded support noise with applications to safety certification,in‘Proceed- ings of the AAAI Conference on Arti...

    2023

  24. [6875]

    & Soudjani, S

    Zhang, Z., Ma, C., Soudijani, S. & Soudjani, S. (2024), For- mal verification of unknown stochastic systems via non- parametric estimation,in‘Proceedings of the 27th Inter- national Conference on Artificial Intelligence and Statis- tics’, Vol. 238, PMLR, pp. 3277–3285. Zhao, H., Zeng, X., Chen, T. & Liu, Z. (2020), Synthesizing barrier certificates using ...

    2024

  25. [7700]

    Valiant, L. G. (1984), ‘A theory of the learnable’,Commu- nications of the ACM27(11), 1134–1142. van Huijgevoort, B., Engelaar, M., Soudjani, S. & Haesaert, S. (2025), ‘SySCoRe 2.0: Toolset for formal control syn- thesis of continuous-state stochastic systems and temporal logic specifications’,Nonlinear Analysis: Hybrid Systems

    1984

  26. [8005]

    & Zamani, M

    Nadali, A., Trivedi, A. & Zamani, M. (2024), ‘Transfer of safety controllers through learning deep inverse dynamics model’,IF AC-PapersOnLine58(11), 129–134. Nadali, A., Trivedi, A. & Zamani, M. (2025a), On choice of loss functions for neural control barrier certificates,in ‘Proceedings of International Conference on Quantitative Evaluation of Systems and...

    Pith/arXiv arXiv 2024