Pith. sign in

REVIEW 3 major objections 5 minor 59 references

Scalable Synthesis and Verification of String Stable Neural Certificates for Interconnected Systems

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

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

Pith's one-line read This paper claims that string stability of large-scale interconnected systems with neural-network controllers can be formally guaranteed by training and verifying discrete-time scalable input-to-state stability certificates that explicitly

desk verdict Solid theory, but the formal guarantee for unknown dynamics depends on a Lipschitz constant the paper assumes without showing it holds in the drone experiment. read the letter →

arxiv 2509.10118 v1 pith:Z24ODGNI submitted 2025-09-12 eess.SY cs.SY

Jingyuan Zhou , Haoze Wu , Haokun Yu , Kaidi Yang This is my paper · ORCID
classification eess.SYcs.SY MSC 93D3093A1593C10
keywords neuralcertificatesstringstabilityinterconnectedsystemsscalableinput-to-statenetworkverificationvectorLyapunovfunctionscounterexample-guidedinductivesynthesislarge-scalecontrol
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 aims to close the gap between learning-based control and formal guarantees by proving that discrete-time scalable input-to-state stability (sISS), a stronger, network-size-independent form of string stability, can be certified for interconnected systems even when the dynamics are neural surrogates of unknown true dynamics. Its central claim is that a vector Lyapunov function, verified with a margin that accounts for the discrepancy between true and approximate dynamics, suffices to guarantee string stability of the true closed-loop system. To make this practical, the paper proves structural reuse theorems that let certificates trained on small or symmetric systems be cheaply lifted to large ones, and validates the pipeline on platoons, drone formations, and microgrids. A sympathetic reader would care because it offers a path to deploy black-box RL controllers with formal safety guarantees in safety-critical networked systems.

What carries the argument

A discrete-time sISS vector Lyapunov certificate: a set of local neural-network Lyapunov functions V_i together with a coupling matrix Γ, satisfying a local decremental condition and a global small-gain condition max_i Σ_{j∈E_i∪{i}} γ_{i,j} ≤ 1−ε. The verification step uses off-the-shelf neural network verifiers to check these local conditions on the surrogate model with a robust margin, and the synthesis step uses counterexample-guided inductive synthesis (CEGIS) to alternately train the certificates and controllers against violating counterexamples.

What would settle it

In a drone formation where the true dynamics are estimated from data, collect a certificate using a Lipschitz constant 10% below the value estimated on a dense hold-out grid, then simulate a sinusoidal disturbance at a point between two grid nodes; if the maximum velocity error gain across the formation exceeds 1, the claimed formal sISS guarantee for the true system is refuted.

Watch

Extended reading notes

Core claim

The paper establishes that discrete-time scalable input-to-state stability (sISS) provides a formal notion of string stability: it requires the maximum state deviation across agents to be bounded by a network-size-independent KL function of the initial deviation plus a K function of the sup-norm of disturbances. The central sufficient condition is a vector Lyapunov function {V_i} with class-K∞ bounds and a decremental inequality V_i(x_i,k+1) ≤ Σ_{j∈E_i∪{i}} γ_{i,j}V_j(x_j,k) + ψ|d_i,k|_2, coupled with a small-gain condition max_i Σ γ_{i,j} ≤ 1−ε. The paper's robust verification theorem shows that if these inequalities hold on a learned surrogate model with an added margin δ_i that covers the

Load-bearing premise

The formal guarantee hinges on knowing a priori a valid Lipschitz constant for the true dynamics on the operating region; if that constant is underestimated, the robust margin is too small and the certificate may not imply string stability for the real system.

Editorial extensions

If this is right

  • If the certificate verifies on the approximated model with the prescribed margin, the true system is guaranteed to be sISS, hence string-stable, independent of network size.
  • Certificates for a small or substructure-isomorphic system can be reused for a larger one without re-verification, reducing the cost of certification at scale.
  • For parameter-affine dynamics and convex Lyapunov functions, certifying only the vertices of a convex parameter region certifies the whole region.
  • Adding a new node to an already-verified subsystem only requires local verification of the coupling if the subsystem dynamics are independent of external states.
  • In closed-loop settings, the framework jointly synthesizes and verifies a controller and a certificate, preserving the original policy's performance via an imitation loss.

Reading between the lines

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

  • The structural reuse theorems suggest that for highly symmetric networks, certification cost could become essentially independent of fleet size, which would make formal guarantees practical for real-time deployment.
  • The reliance on a priori Lipschitz bounds suggests a natural extension where these bounds are themselves verified or tightened online using set-membership identification, rather than assumed from physics.
  • The error bound depends on grid resolution; an adaptive grid that refines near counterexamples could yield tighter margins and less conservative controllers.
  • The same certificate-and-verify machinery could be adapted to other network effects such as safety or stochastic disturbances, provided the analogous approximation-error propagation can be bounded.
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 presents a synthesis-and-verification pipeline for neural Lyapunov certificates — and in the controlled case, neural controllers — for discrete-time interconnected systems. The formal property is discrete-time scalable input-to-state stability (sISS), which the authors use as their notion of string stability. Theorem 1 gives a small-gain vector-Lyapunov sufficient condition for sISS; Theorem 2 extends it to the realistic case where only a neural surrogate of the true dynamics is available, using Lipschitz constants and a grid-based approximation-error bound to impose a robust margin; Section 4 gives the analogous sISS-VCLF result for neural controllers; Theorems 3–6 and Corollaries 3–5 support certificate reuse for substructure-isomorphic, structurally equivalent, parameter-affine, and decomposable networks. The experimental sections apply the pipeline to mixed-autonomy platoons, drone formations, and microgrids, reporting reduced training/verification time via the reuse strategies and error gains below one in Table 3.

Significance. If the formal claims are correct, the framework would be a useful contribution to a difficult area: it would provide a scalable, verifier-backed way to give learned controllers a Lyapunov-based stability certificate in networked systems. The robustification step in Theorem 2 is the most valuable part, since it explicitly propagates surrogate-model error through the certificate, and the node-equivalence/decomposability results are practically relevant. I found no obvious flaw in the core derivation of Theorem 2 under Assumptions 1–2. However, the paper currently overstates what is proved: the formal guarantee is sISS, not the classical string-stability gain of Eq. (37), and the experiments on unknown dynamics do not discharge the sound-Lipschitz-constant assumption that Theorem 2 requires. These points are substantive but addressable.

major comments (3)
  1. [Section 5.1 / Theorem 2 / Remark 1] Section 5.1 says for drone formations 'the true dynamic is unknown F_i, and we estimate it from data'; the HDV model is also treated as unknown. Theorem 2/Remark 1 instead require a sound Lipschitz constant L_fi for the true dynamics. In the proof (Appendix A.2, Eq. (A.13)), L_fi enters epsilon_i = epsilon_hat_i + 0.5(L_fi + L_tilde_fi)|Delta|_2; if L_fi is underestimated, the margin delta_i is too small and Eq. (9) can hold for the surrogate while Eq. (5) fails for the true system. No sound estimator for L_fi is supplied or reported for the drone/HDV experiments. Please either provide verified Lipschitz bounds for the true models used in the experiments, or explicitly restrict the formal guarantee to settings where L_fi is known.
  2. [Section 5.4, Eq. (37)] The abstract and conclusion claim a formal guarantee of 'string stability,' but the formal result is discrete-time sISS (Def. 1), a network-wide ISS estimate. The classical string-stability gain in Eq. (37), max_i ||v_i||_{L2}/||v_{i-1}||_{L2} <= 1, is used in Table 3 without a proof that sISS implies it. Thus Table 3 is an empirical check, not a formal certificate. Please prove the implication under stated assumptions, or revise the claims in the title/abstract/conclusion to say that the framework guarantees sISS and that Eq. (37) is an empirical performance metric.
  3. [Sections 3.1–3.2, Eqs. (3), (5), (9)] The certificate conditions Eqs. (3) and (9) are verified only on the bounded operating region R_i and Z_i, but no forward-invariance of R_i is stated or verified. In the proof of Theorem 1, the class-K∞ bounds are used at every time k (Eqs. (A.6)–(A.9)); if a trajectory leaves R_i, those bounds are no longer available and the sISS estimate is not established. The paper should either prove invariance of R_i, verify the conditions on an absorbing superset, or explicitly state the sISS result as conditional on trajectories remaining in R_i.
minor comments (5)
  1. [Section 3.2, Eq. (9)] The quantifier in Eq. (9) is written 'for any tilde_x_{i,k} in R_i', but the condition involves the neighbor states {x_j,k} and d_i,k. It should quantify over z_i,k in Z_i. The same issue appears in Eq. (23) and Corollary 2.
  2. [Appendix A.5 (proof of Theorem 5)] The proof says 'By Eq. (25)'; Eq. (25) belongs to Corollary 4. The affine dynamics of Theorem 5 are in Eq. (14). Please correct this cross-reference.
  3. [Section 5.3, Tables 1–2] The entries '-' and 'TO' are not explained in the captions. Make explicit that 'Full R.' failed to complete within 4 hours and that '-' indicates no value is reported.
  4. [Throughout] Several typos and notation slips should be cleaned: 'representing its the admissible operating region' (Sec. 3.1), 'The true dynamic is unknown F i' (Sec. 5.1), and inconsistent use of tilde_x_{k+1,i} versus tilde_x_{i,k+1}. Also ensure figure axis labels render legibly in the final version.
  5. [Section 3.4, Theorem 6 / Definition 4] The proof of Theorem 6 assumes the remaining agents satisfy sISS conditions but does not explicitly assemble the combined gain matrix or verify the small-gain condition for the full system. This is likely fixable by setting gains on added edges to zero and checking row sums; please make that argument explicit.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: the sISS derivation is a conditional sound-verification argument; the drone L_fi gap is an assumption risk, not a circular reduction.

full rationale

The central derivation is Theorem 2 (Sec. 3.2, proof A.2): if Assumptions 1-2 hold, then |fi(z)-f̃i(z)| ≤ ε̂i + 0.5(L_fi+L_f̃i)|Δ|2 = εi, and any Vi satisfying Eq. (9) with δi ≥ L_Vi εi also satisfies the true decremental condition Eq. (5). The margin δi appears in the training loss Eq. (13), but the final certificate is checked by an independent sound neural verifier (Marabou/α,β-CROWN) against Eq. (3)∧(9); CEGIS only proposes candidates. Theorems 3-6 and Corollaries 1-5 are proven directly, not imported from self-citations. Self-references [7], [16], [29] are background/experiment-setup citations and are not load-bearing for the sISS guarantee. The only flagged gap is the drone experiment (Sec. 5.1: 'The true dynamic is unknown F i, and we estimate it from data.') versus Remark 1, which assumes L_fi 'known a priori from physics/regularity.' No sound finite-sample estimator for L_fi is supplied, so the formal guarantee may not hold for that experiment. This is a correctness/assumption risk, not a circular step: it does not make any theorem equal to its input by construction. Hence no significant circularity; score 2 reflects the minor non-load-bearing self-citations.

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

The central claim rests on several tuning parameters (gains, margins, K∞ bounds, grid resolution) and on assumptions about Lipschitz constants and sound verifiers. The paper does not specify how these are chosen, and the experiments do not report the exact values, so the formal guarantee is conditional on these choices being sound.

free parameters (5)
  • coupling gains Γ = learned via training
    The gains γ_{i,j} in Eq. (5) are trained as ReLU(Γ_pure)∘G and rescaled to satisfy the small-gain condition (Section 3.3); they are design parameters chosen to make the certificate verifiable, not derived independently.
  • disturbance gain ψ = not specified
    Positive scalar in the decremental inequality Eq. (5) and Eq. (9); its value is chosen (likely tuned) to balance the inequality, and the paper does not state how it is set.
  • small-gain margin ε = not specified
    Appears in Eq. (4) and in the rescaling of Γ; chosen by hand within (0,1).
  • class-K∞ bounds α1, α2 = not specified
    Used in Eq. (3) and in loss Eq. (12) but never instantiated; their concrete form (e.g., c1|x|^p, c2|x|^p) and constants are free choices that directly affect verification.
  • grid step sizes Δ = not specified
    Used to bound the approximation error ε_i in Eq. (8) and Theorem 2; the paper does not report the grid resolution used in experiments, which determines the margin δ_i.
assumptions (7)
  • domain assumption Assumption 1: true dynamics fi and approximated dynamics f̃i are Lipschitz with known/estimated constants L_fi, L_f̃i; Lyapunov functions Vi Lipschitz with constant L_Vi.
    Introduced in Section 3.2 before Theorem 2; required for the error bound Eq. (A.13) and the margin δ_i.
  • domain assumption Assumption 2: the approximation error on a rectangular grid Di is finite (ε̂_i < ∞) and the grid covers the bounded region Zi.
    Needed to bound sup_z |fi - f̃i| over the continuous domain via Lipschitz extrapolation from grid points.
  • domain assumption Assumption 3: controllers π_i are Lipschitz continuous with constants L_π_i.
    Used in Corollary 2 to bound the closed-loop Lipschitz constant as L_fi(1+L_π_i).
  • domain assumption The true dynamics' Lipschitz constant L_fi is known a priori from physics or regularity (Remark 1).
    Explicitly assumed so in Remark 1; without a sound L_fi, the error bound ε_i is not an upper bound and the formal guarantee fails.
  • standard math The neural network verifier (Marabou, α,β-CROWN, NNV) is sound for the queries in Eq. (10) and Eq. (24).
    The framework relies on off-the-shelf sound verifiers to check the conditions; soundness is a property of the tools, not proven in this paper.
  • standard math The neural Lipschitz bounding method (e.g., Eclipse [49]) returns a sound upper bound on L_Vi and L_f̃i.
    Remark 1 states L_f̃i and L_Vi are estimated using such a method; if the estimate is not an upper bound, the margin δ_i could be too small.
  • domain assumption Vi is convex for Theorem 5 and Corollary 4.
    Stated in Theorem 5 ('Assume each Vi is convex'), needed for Jensen's inequality; not specified whether the experimental certificates are convex.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Scalable Synthesis and Verification of String Stable Neural Certificates for Interconnected Systems." pith.science (2026). https://pith.science/paper/Z24ODGNI

@misc{pith2026250910118,
  author       = {Pith},
  title        = {Pith review of: Scalable Synthesis and Verification of String Stable Neural Certificates for Interconnected Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/Z24ODGNI}},
  note         = {Machine review of arXiv:2509.10118}
}
read the original abstract

Ensuring string stability is critical for the safety and efficiency of large-scale interconnected systems. Although learning-based controllers (e.g., those based on reinforcement learning) have demonstrated strong performance in complex control scenarios, their black-box nature hinders formal guarantees of string stability. To address this gap, we propose a novel verification and synthesis framework that integrates discrete-time scalable input-to-state stability (sISS) with neural network verification to formally guarantee string stability in interconnected systems. Our contributions are four-fold. First, we establish a formal framework for synthesizing and robustly verifying discrete-time scalable input-to-state stability (sISS) certificates for neural network-based interconnected systems. Specifically, our approach extends the notion of sISS to discrete-time settings, constructs neural sISS certificates, and introduces a verification procedure that ensures string stability while explicitly accounting for discrepancies between the true dynamics and their neural approximations. Second, we establish theoretical foundations and algorithms to scale the training and verification pipeline to large-scale interconnected systems. Third, we extend the framework to handle systems with external control inputs, thereby allowing the joint synthesis and verification of neural certificates and controllers. Fourth, we validate our approach in scenarios of mixed-autonomy platoons, drone formations, and microgrids. Numerical simulations show that the proposed framework not only guarantees sISS with minimal degradation in control performance but also efficiently trains and verifies controllers for large-scale interconnected systems under specific practical conditions.

Figures

Figures reproduced from arXiv: 2509.10118 by the authors.

Figure 1
Figure 1. Training loss curves in different environments. [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Learned Lyapunov contours for CAV and HDV sys [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. 2D Lyapunov function visualizations for two Drones [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (1 more)
Figure 5
Figure 5. Figure 5: Trajectory visualizations in three environments: (a) [PITH_FULL_IMAGE:figures/full_fig_p012_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

59 extracted references · 1 linked inside Pith

  1. [1]

    Sub- space identification of large-scale interconnected systems

    Aleksandar Haber and Michel Verhaegen. Sub- space identification of large-scale interconnected systems. IEEE Transactions on Automatic Control, 59(10):2754–2759, 2014

    2014

  2. [2]

    Small-gain theorem for safety verification of inter- connected systems

    Ziliang Lyu, Xiangru Xu, and Yiguang Hong. Small-gain theorem for safety verification of inter- connected systems. Automatica, 139:110178, 2022

    2022

  3. [3]

    Privacy-preserving distributed estimation for interconnected dynamic systems

    Yuchen Zhang, Bo Chen, Jianzheng Wang, and Li Yu. Privacy-preserving distributed estimation for interconnected dynamic systems. Automatica, 177:112277, 2025

    2025

  4. [4]

    Lars AL Janssen, Bart Besselink, Rob HB Fey, and Nathan van de Wouw. Modular model reduction 11 /uni00000013 /uni00000015/uni00000013/uni00000013/uni00000017/uni00000013/uni00000013/uni00000019/uni00000013/uni00000013/uni0000001b/uni00000013/uni00000013/uni00000014/uni00000013/uni00000013/uni00000013 /uni00000015/uni00000013 /uni00000015/uni00000015 /uni0...

    2024

  5. [5]

    String stability in microgrids using frequency controlled inverter chains

    Guilherme F Silva, Alejandro Donaire, Maria M Seron, Aaron McFadyen, and Jason Ford. String stability in microgrids using frequency controlled inverter chains. IEEE Control Systems Letters , 6:1484–1489, 2021

    2021

  6. [6]

    Opti- mal control of interconnected systems with time- correlated noises: Application to vehicle platoon

    Yan Wang, Rong Su, and Bohui Wang. Opti- mal control of interconnected systems with time- correlated noises: Application to vehicle platoon. Automatica, 137:110018, 2022

    2022

  7. [7]

    A parameter privacy-preserving strategy for mixed-autonomy platoon control

    Jingyuan Zhou and Kaidi Yang. A parameter privacy-preserving strategy for mixed-autonomy platoon control. Transportation Research Part C: Emerging Technologies, 169:104885, 2024

    2024

  8. [8]

    Model pre- dictive control of interconnected linear and nonlin- ear processes

    Guang-Yan Zhu and Michael A Henson. Model pre- dictive control of interconnected linear and nonlin- ear processes. Industrial & engineering chemistry research, 41(4):801–816, 2002

    2002

Show all 59 references
  1. [9]

    String stability for vehicular platoon control: Definitions and analysis methods

    Shuo Feng, Yi Zhang, Shengbo Eben Li, Zhong Cao, Henry X Liu, and Li Li. String stability for vehicular platoon control: Definitions and analysis methods. Annual Reviews in Control, 47:81–97, 2019

    2019

  2. [10]

    Leading cruise control in mixed traffic flow: System modeling, controllability, and string stability

    Jiawei Wang, Yang Zheng, Chaoyi Chen, Qing Xu, and Keqiang Li. Leading cruise control in mixed traffic flow: System modeling, controllability, and string stability. IEEE Transactions on Intelligent Transportation Systems, 23(8):12861–12876, 2021

    2021

  3. [11]

    String stable and collision-safe model predictive platoon control

    Alexander L Gratzer, Sebastian Thormann, Alexander Schirrer, and Stefan Jakubek. String stable and collision-safe model predictive platoon control. IEEE Transactions on Intelligent Trans- portation Systems, 23(10):19358–19373, 2022

    2022

  4. [12]

    Adaptive learning-based model predictive control for uncer- tain interconnected systems: A set membership identification approach

    Ahmed Aboudonia and John Lygeros. Adaptive learning-based model predictive control for uncer- tain interconnected systems: A set membership identification approach. Automatica, 171:111943, 2025

    2025

  5. [13]

    Distributed adap- tive integrated-sliding-mode controller synthesis for string stability of vehicle platoons

    Xianggui Guo, Jianliang Wang, Fang Liao, and Rodney Swee Huat Teo. Distributed adap- tive integrated-sliding-mode controller synthesis for string stability of vehicle platoons. IEEE Transactions on Intelligent Transportation Sys- tems, 17(9):2419–2429, 2016

    2016

  6. [14]

    End-to-end safe reinforce- ment learning through barrier functions for safety- critical continuous control tasks

    Richard Cheng, G´ abor Orosz, Richard M Murray, and Joel W Burdick. End-to-end safe reinforce- ment learning through barrier functions for safety- critical continuous control tasks. In Proceedings of the AAAI conference on artificial intelligence , vol- ume 33, pages 3387–3395, 2019

    2019

  7. [15]

    A reinforce- ment learning-based vehicle platoon control strat- egy for reducing energy consumption in traffic os- cillations

    Meng Li, Zehong Cao, and Zhibin Li. A reinforce- ment learning-based vehicle platoon control strat- egy for reducing energy consumption in traffic os- cillations. IEEE Transactions on Neural Networks and Learning Systems, 32(12):5309–5322, 2021

    2021

  8. [16]

    En- hancing system-level safety in mixed-autonomy pla- toon via safe reinforcement learning

    Jingyuan Zhou, Longhao Yan, and Kaidi Yang. En- hancing system-level safety in mixed-autonomy pla- toon via safe reinforcement learning. IEEE Trans- 12 actions on Intelligent Vehicles , pages 1–13, 2024

    2024

  9. [17]

    On the string stability of neural network-based car-following models: A generic analysis framework

    Xiaohui Zhang, Jie Sun, Zuduo Zheng, and Jian Sun. On the string stability of neural network-based car-following models: A generic analysis framework. Transportation research part C: emerging technolo- gies, 160:104525, 2024

    2024

  10. [18]

    Lyapunov-stable neural-network control

    Hongkai Dai, Benoit Landry, Lujie Yang, Marco Pavone, and Russ Tedrake. Lyapunov-stable neural-network control. Robotics: Science and Sys- tems, 2021

    2021

  11. [19]

    Lyapunov- stable neural control for state and output feedback: A novel formulation

    Lujie Yang, Hongkai Dai, Zhouxing Shi, Cho-Jui Hsieh, Russ Tedrake, and Huan Zhang. Lyapunov- stable neural control for state and output feedback: A novel formulation. In Forty-first International Conference on Machine Learning, 2024

    2024

  12. [20]

    Safe and reliable training of learning-based aerospace controllers

    Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto Ravaioli, Baoluo Meng, Michael Durling, Kerianne Hobbs, Milan Ganai, et al. Safe and reliable training of learning-based aerospace controllers. In2024 AIAA DATC/IEEE 43rd Digital Avionics Systems C...

    2024

  13. [21]

    Formally verifying deep rein- forcement learning controllers with lyapunov bar- rier certificates

    Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J Ra- vaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, et al. Formally verifying deep rein- forcement learning controllers with lyapunov bar- rier certificates. arXiv preprint arXiv:2...

    2024 arXiv

  14. [22]

    Compositional neural certificates for networked dynamical systems

    Songyuan Zhang, Yumeng Xiu, Guannan Qu, and Chuchu Fan. Compositional neural certificates for networked dynamical systems. In Learning for Dy- namics and Control Conference , pages 272–285. PMLR, 2023

    2023

  15. [23]

    Scal- able input-to-state stability of nonlinear intercon- nected systems

    Guilherme Fr´ oes Silva, Alejandro Donaire, Richard Middleton, Aaron McFadyen, and Jason Ford. Scal- able input-to-state stability of nonlinear intercon- nected systems. IEEE Transactions on Automatic Control, 2024

    2024

  16. [24]

    Heterogeneous string stability of unidirectionally interconnected mimo lti systems

    G´ abor R¨ od¨ onyi. Heterogeneous string stability of unidirectionally interconnected mimo lti systems. Automatica, 103:354–362, 2019

    2019

  17. [25]

    String stable inte- gral control design for vehicle platoons with distur- bances

    Guilherme Fr´ oes Silva, Alejandro Donaire, Aaron McFadyen, and Jason J Ford. String stable inte- gral control design for vehicle platoons with distur- bances. Automatica, 127:109542, 2021

    2021

  18. [26]

    On stochastic string stability with applications to platooning over addi- tive noise channels

    Francisco J Vargas, Marco A Gordon, Andr´ es A Pe- ters, and Alejandro I Maass. On stochastic string stability with applications to platooning over addi- tive noise channels. Automatica, 171:111923, 2025

    2025

  19. [27]

    String stabil- ity of energy-saving aircraft formations

    James R Riehl, Esteban AL Hufstedler, Philippe Chatelain, and Julien M Hendrickx. String stabil- ity of energy-saving aircraft formations. Journal of Guidance, Control, and Dynamics , 45(5):935–943, 2022

    2022

  20. [28]

    Multiobjective h∞ control for string stability of cooperative adaptive cruise con- trol systems

    Erkan Kayacan. Multiobjective h∞ control for string stability of cooperative adaptive cruise con- trol systems. IEEE Transactions on Intelligent Ve- hicles, 2(1):52–61, 2017

    2017

  21. [29]

    Data-driven analysis for disturbance amplification in car-following behavior of automated vehicles

    Yang Zhou, Xinzhi Zhong, Qian Chen, Soy- oung Ahn, Jiwan Jiang, and Ghazaleh Jafarsalehi. Data-driven analysis for disturbance amplification in car-following behavior of automated vehicles. Transportation research part B: methodological , 174:102768, 2023

    2023

  22. [30]

    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 Transactions on Robotics, 39(3):1749–1767, 2023

    2023

  23. [31]

    Model-free safe re- inforcement learning through neural barrier cer- tificate

    Yujie Yang, Yuxuan Jiang, Yichen Liu, Jianyu Chen, and Shengbo Eben Li. Model-free safe re- inforcement learning through neural barrier cer- tificate. IEEE Robotics and Automation Letters , 8(3):1295–1302, 2023

    2023

  24. [32]

    Synthesizing barrier certificates using neu- ral networks

    Hengjun Zhao, Xia Zeng, Taolue Chen, and Zhim- ing Liu. Synthesizing barrier certificates using neu- ral networks. In Proceedings of the 23rd interna- tional conference on hybrid systems: Computation and control, pages 1–11, 2020

    2020

  25. [33]

    Learning a formally verified control barrier function in stochas- tic environment

    Manan Tayal, Hongchao Zhang, Pushpak Jagtap, Andrew Clark, and Shishir Kolathaya. Learning a formally verified control barrier function in stochas- tic environment. In 2024 IEEE 63rd Conference on Decision and Control (CDC) , pages 4098–4104, 2024

    2024

  26. [34]

    Simultaneous synthesis and verification of neural control barrier functions through branch-and-bound verification- in-the-loop training

    Xinyu Wang, Luzia Knoedler, Frederik Baymler Mathiesen, and Javier Alonso-Mora. Simultaneous synthesis and verification of neural control barrier functions through branch-and-bound verification- in-the-loop training. In 2024 European Control Conference (ECC), pages 571–578, 2024

    2024

  27. [35]

    Exact verification of relu neural control barrier functions

    Hongchao Zhang, Junlin Wu, Yevgeniy Vorobey- chik, and Andrew Clark. Exact verification of relu neural control barrier functions. Advances in neu- ral information processing systems , 36:5685–5705, 2023

    2023

  28. [36]

    Data-driven verification and synthesis of stochastic systems via barrier certifi- cates

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

    2024

  29. [37]

    Safe reach set computation via neural barrier certificates

    Alessandro Abate, Sergiy Bogomolov, Alec Ed- wards, Kostiantyn Potomkin, Sadegh Soudjani, and Paolo Zuliani. Safe reach set computation via neural barrier certificates. IF AC-PapersOnLine, 58(11):107–114, 2024

    2024

  30. [38]

    Verification of neural control barrier functions with symbolic derivative bounds propaga- tion

    Hanjiang Hu, Yujie Yang, Tianhao Wei, and Changliu Liu. Verification of neural control barrier functions with symbolic derivative bounds propaga- tion. In Proceedings of The 8th Conference on Robot Learning, volume 270, pages 1797–1814. PMLR, 2024

    2024

  31. [39]

    Gcbf+: A neural graph control barrier function framework for distributed safe multi-agent control

    Songyuan Zhang, Oswin So, Kunal Garg, and Chuchu Fan. Gcbf+: A neural graph control barrier function framework for distributed safe multi-agent control. IEEE Transactions on Robotics, 2025

    2025

  32. [40]

    Counterexample-guided computation of polyhedral 13 lyapunov functions for piecewise linear systems

    Guillaume O Berger and Sriram Sankaranarayanan. Counterexample-guided computation of polyhedral 13 lyapunov functions for piecewise linear systems. Automatica, 155:111165, 2023

    2023

  33. [41]

    Stability analy- sis of switched linear systems with neural lyapunov functions

    Virginie Debauche, Alec Edwards, Rapha¨ el M Jungers, and Alessandro Abate. Stability analy- sis of switched linear systems with neural lyapunov functions. In Proceedings of the AAAI Conference on Artificial Intelligence , volume 38, pages 21010– 21018, 2024

    2024

  34. [42]

    Physics-informed neural network lyapunov functions: Pde characterization, learning, and verification

    Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. Physics-informed neural network lyapunov functions: Pde characterization, learning, and verification. Automatica, 175:112193, 2025

    2025

  35. [43]

    Certified training: Small boxes are all you need

    Mark Niklas Mueller, Franziska Eckert, Marc Fis- cher, and Martin Vechev. Certified training: Small boxes are all you need. In The Eleventh Inter- national Conference on Learning Representations , 2023

    2023

  36. [44]

    On adaptive attacks to ad- versarial example defenses

    Florian Tramer, Nicholas Carlini, Wieland Brendel, and Aleksander Madry. On adaptive attacks to ad- versarial example defenses. Advances in neural in- formation processing systems, 33:1633–1645, 2020

    2020

  37. [45]

    Beta-crown: Efficient bound propagation with per- neuron split constraints for neural network robust- ness verification

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-crown: Efficient bound propagation with per- neuron split constraints for neural network robust- ness verification. Advances in neural information processing systems, 34:29909–29921, 2021

    2021

  38. [46]

    Marabou 2.0: a versatile formal analyzer of neural networks

    Haoze Wu, Omri Isac, Aleksandar Zelji´ c, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Re- faeli, Guy Amir, Kyle Julian, Shahaf Bassan, et al. Marabou 2.0: a versatile formal analyzer of neural networks. InInternational Conference on Computer Aided Verification, pages 2...

    2024

  39. [47]

    Nnv 2.0: the neural network verification tool

    Diego Manzanas Lopez, Sung Woo Choi, Hoang- Dung Tran, and Taylor T Johnson. Nnv 2.0: the neural network verification tool. In International Conference on Computer Aided Verification, pages 397–412. Springer, 2023

    2023

  40. [48]

    A novel counterexample-guided inductive synthe- sis framework for barrier certificate generation

    Mi Ding, Kaipeng Lin, Wang Lin, and Zuohua Ding. A novel counterexample-guided inductive synthe- sis framework for barrier certificate generation. In 2022 IEEE 33rd International Symposium on Soft- ware Reliability Engineering (ISSRE) , pages 263–

    2022

  41. [49]

    Eclipse: Effi- cient compositional lipschitz constant estimation for deep neural networks.Advances in Neural Infor- mation Processing Systems, 37:10414–10441, 2024

    Yuezhu Xu and S Sivaranjani. Eclipse: Effi- cient compositional lipschitz constant estimation for deep neural networks.Advances in Neural Infor- mation Processing Systems, 37:10414–10441, 2024

    2024

  42. [50]

    Diego Manzanas Lopez, Sung Woo Choi, Hoang- Dung Tran, and Taylor T. Johnson. NNV 2.0: The Neural Network Verification Tool. In Constantin Enea and Akash Lal, editors, International Con- ference on Computer Aided Verification , volume 13965, pages 397–412. Springer, 2023

    2023

  43. [51]

    Automatic Perturba- tion Analysis for Scalable Certified Robustness and Beyond

    Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic Perturba- tion Analysis for Scalable Certified Robustness and Beyond. Advances in Neural Information Process- ing Systems, 33:1129–1141, 2020

    2020

  44. [52]

    Lomuscio

    Patrick Henriksen and Alessio R. Lomuscio. Ef- ficient Neural Network Verification via Adap- tive Refinement and Adversarial Search. In Giuseppe De Giacomo, Alejandro Catal´ a, Bistra Dilkina, Michela Milano, Sen´ en Barro, Alberto Bugar ´ ın, and J´ erˆ ome Lang, editors,Euro...

    2020

  45. [53]

    Input convex neural networks

    Brandon Amos, Lei Xu, and J Zico Kolter. Input convex neural networks. InInternational conference on machine learning, pages 146–155. PMLR, 2017

    2017

  46. [54]

    Full ve- locity difference model for a car-following theory

    Rui Jiang, Qingsong Wu, and Zuojin Zhu. Full ve- locity difference model for a car-following theory. Physical Review E, 64(1):017101, 2001

    2001

  47. [55]

    A compendium of compar- ison function results

    Christopher M Kellett. A compendium of compar- ison function results. Mathematics of Control, Sig- nals, and Systems, 26(3):339–374, 2014

    2014

  48. [56]

    Contemporary abstract algebra

    Joseph Gallian. Contemporary abstract algebra . Chapman and Hall/CRC, 2021

    2021

  49. [57]

    The quickhull algorithm for convex hulls

    C Bradford Barber, David P Dobkin, and Hannu Huhdanpaa. The quickhull algorithm for convex hulls. ACM Transactions on Mathematical Software (TOMS), 22(4):469–483, 1996. A Proofs A.1 Proof of Theorem 1 Proof. Define the composite Lyapunov function: V (k) = max i∈N Vi(xi,k). (A....

    1996

  50. [58]

    There exists α1, α2 ∈ K∞ such that ∀i ∈ eN α1(|xτ (i),k|2) ≤ Vτ (i)(xτ (i),k) ≤ α2(|xτ (i),k|2), (A.17)

  51. [59]

    Then, the small-gain condition is satisfied, and by Eq

    There exists positive gains Γ satisfying the small-gain condition such that the decremental inequality holds Vτ (i) xτ (i),k+1 − γτ (i),τ (i)Vτ (i)(xτ (i),k) − X j∈Ei γτ (i),τ (j)Vτ (j)(xτ (j),k) − ψ|dτ (i),k|2 ≤ 0 (A.18) Define gains for system eI as eγi,j := γτ (i),τ (j) and...

Pith tools

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