REVIEW 4 major objections 3 minor 52 references
From Formal Methods to Data-Driven Safety Certificates of Unknown Large-Scale Networks
T0 review · 4 major / 3 minor · reviewed 2026-08-05 · deepseek-v4-flash
Pith's one-line read Single noisy trajectories per subsystem certify safety of unknown networks
desk verdict The abstract promises a genuinely useful extension of compositional barrier certificates to noisy single-trajectory data, but the supplied manuscript body is an unrelated business-process paper, so the core content is unevaluable as submitted. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The control sub-barrier certificate (CSBC) is the central object: a function computed for a subsystem from a single noisy trajectory, along with a local safe controller, verifying the subsystem's safety condition. The composition step uses a small-gain condition on the interconnection gains to combine local CSBCs into a global control barrier certificate (CBC) for the network. The data-dependent sum-of-squares (SOS) optimization program is the computational engine that turns noisy trajectory data into certificates.
What would settle it
Build a two-subsystem interconnection with unknown (but simulated) dynamics, generate one noise-corrupted input-state trajectory per subsystem that satisfies the stated rank condition, and run the proposed SOS program to obtain a CBC. If a subsequent simulation finds a trajectory that leaves the safe set within the time horizon while the local CSBCs and small-gain condition hold, the composition claim is false.
Extended reading notes
Core claim
The central claim is that composing control sub-barrier certificates, each computed from a single noise-corrupted input-state trajectory of an unknown subsystem satisfying a rank condition, yields a control barrier certificate for the entire network, guaranteeing safety over an infinite time horizon. The composition is made valid under a small-gain compositional reasoning, and the local certificates plus controllers are computed by a data-dependent sum-of-squares optimization program. The computational complexity of the compositional design grows linearly with the number of subsystems, whereas a monolithic SOS design grows polynomially with network dimension.
Load-bearing premise
The whole-network guarantee depends on the unverified premise that the unknown network satisfies the small-gain condition needed for composing the local certificates.
Editorial extensions
If this is right
- Safety certificates for unknown large-scale networks can be built from per-subsystem data alone, without a global model or centralized computation.
- The per-subsystem design makes the computational cost grow linearly with the number of subsystems, enabling certification of networks too large for monolithic SOS approaches.
- The certificates come with correctness guarantees, so the resulting local controllers keep the network safe over an infinite horizon despite unknown dynamics and noise.
- The approach applies to a range of interconnection topologies, as demonstrated on physical network examples.
Reading between the lines
- The small-gain condition is a global property that the paper's method does not verify from the noisy data; an immediate testable extension is to derive a data-driven condition that certifies the small-gain bound from the same trajectories.
- If the rank condition holds for generic noise and sufficiently rich inputs, the method could be extended to active exploration, where the controller deliberately excites the subsystem to make the condition hold.
- The composition framework suggests a modular route to safety-critical control of heterogeneous networks where subsystems have different dynamics but share a common certificate interface.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. This submission (arXiv:2508.09520) is, according to its abstract, a data-driven compositional framework for designing safety controllers for unknown large-scale interconnected networks. The proposed method treats the network as a composition of subsystems, collects one noise-corrupted input-state trajectory from each subsystem up to a finite horizon, and, under a rank condition, computes a control sub-barrier certificate (CSBC) and local controller via a data-dependent sum-of-squares (SOS) program. A small-gain compositional argument is then used to combine local CSBCs into a control barrier certificate (CBC) for the full network, guaranteeing safety over an infinite time horizon. The abstract claims correctness guarantees and linear computational scaling in the number of subsystems. However, the supplied full text is not this paper: it is arXiv:2508.09527, a paper on graph neural networks for predictive business process monitoring. None of the formal-methods content—definitions, theorems, SOS programs, noise models, rank conditions, small-gain details, or numerical experiments—is present in the provided manuscript.
Significance. If the claimed results were established, the contribution would be significant: a compositional, data-driven method for control barrier certificates of unknown large-scale networks using only a single noisy trajectory per subsystem, with only linear growth in the number of subsystems, would be a meaningful advance for decentralized safety-critical control. The abstract also promises explicit correctness guarantees, which are valuable in this area. However, because the manuscript body is a different, unrelated paper, no technical content is available to evaluate. The claimed contribution cannot be credited from the abstract alone, and the significance of the work remains an unverified assertion.
major comments (4)
- [Full text (supplied as arXiv:2508.09527)] The body of the manuscript under review is not the paper described in the abstract. The provided full text is 'Time-Aware and Transition-Semantic Graph Neural Networks for Interpretable Predictive Business Process Monitoring' (arXiv:2508.09527). It contains no definition of control sub-barrier certificates, no data-dependent SOS program, no composition theorem, no noise model, no rank condition, and no experiments on physical networks. The central claim of the abstract therefore cannot be checked, and the manuscript is unevaluable in its present form.
- [Abstract, 'certain rank condition'] The abstract conditions the entire method on each subsystem providing a single noise-corrupted input-state trajectory 'satisfying a certain rank condition,' but the rank condition is never stated. A rank condition alone does not identify a nonlinear system from one trajectory unless accompanied by a formal identifiability or excitation theorem. Without such a theorem, the CSBC is merely fitted to the observed trajectory and cannot be claimed to hold for the unknown subsystem. This is a load-bearing gap.
- [Abstract, 'under a small-gain compositional reasoning'] The global CBC is claimed to follow 'under a small-gain compositional reasoning.' The small-gain condition is a property of the unknown interconnection, and the abstract does not state how it is verified from the same noisy data, what quantitative margin is required, or how the margin interacts with the noise bound and finite horizon. Since local CSBCs can all be individually valid while the composition fails if this condition is not met, this premise must be made explicit and checkable.
- [Abstract, 'infinite time horizon'] The safety guarantee is stated over an infinite time horizon, yet the data consist of a single trajectory up to a finite horizon. Extrapolation from finite noisy data to an infinite-horizon certificate requires a strict Lyapunov-like decrease condition with a known positive margin and a noise model that permits robust forward propagation. Neither the margin nor the noise model is specified in the abstract or the provided text. This is essential for ruling out certificates that are valid only over the observed time window.
minor comments (3)
- [Abstract] The phrase 'specified time horizon' and 'certain rank condition' are undefined in the abstract. If the correct full text is supplied, these should be precisely defined in the introduction.
- [Abstract, complexity claim] The paper contrasts polynomial complexity with 'linear scale concerning the number of subsystems,' but the complexity measure is not specified—e.g., number of SOS decision variables, polynomial degree, or number of subsystems. The complexity model should be stated precisely.
- [Abstract, 'correctness guarantees'] The nature of the claimed correctness guarantees is unclear from the abstract: are they deterministic, probabilistic, or asymptotic? The full text should clarify the guarantee type and the role of the noise bound.
Circularity Check
No circularity established: the full text supplied is an unrelated PBPM paper (arXiv 2508.09527), not the target formal-methods paper (arXiv 2508.09520). The abstract alone provides no equations, rank condition, or composition theorem to exhibit a reduction-to-input.
full rationale
The circularity audit requires quoting the paper's equations/definitions and exhibiting that a 'prediction' is identical to an input by construction or is a renamed fitted parameter. The only target content available is the abstract of arXiv:2508.09520. The supplied full-text body is arXiv:2508.09527v2, 'Time-Aware and Transition-Semantic Graph Neural Networks for Interpretable Predictive Business Process Monitoring' by Wang and Damiani. That paper contains no CSBC, no control barrier certificates, no sum-of-squares programs, no noise model, no small-gain theorem, and no safety experiments; it is about next-event prediction in business process logs. Consequently, none of the load-bearing steps of the target derivation chain can be checked: (i) the 'certain rank condition' on a single noise-corrupted trajectory is not stated, so it cannot be shown whether it identifies the subsystem dynamics or merely fits the observed trajectory; (ii) the 'small-gain compositional reasoning' is asserted as a premise, but an assumption is not circular unless the paper defines it in terms of the conclusion; (iii) the step from finite-length noisy data to an infinite-horizon CBC is not presented, so no self-definitional or fitted-input-as-prediction pattern can be exhibited. Per the review rules, absence of evidence is not circularity, and inventing a circularity would require speculation about unprovided definitions. Thus the honest non-finding is score 0. This should not be read as endorsement: the target paper's claims are unevaluable from the material provided, and the mismatch itself is a serious evidence/attribution problem, but it is not a circularity defect.
Assumptions & free parameters
free parameters (4)
- Data collection horizon T =
not stated
- Noise bound =
not stated
- SOS relaxation parameters =
not stated
- Small-gain margin =
not stated
assumptions (4)
- domain assumption Small-gain theorem for interconnected systems
- domain assumption Rank/persistence-of-excitation condition on the single trajectory
- domain assumption Bounded noise assumption
- ad hoc to paper Existence of polynomial control sub-barrier certificates
invented entities (1)
-
Control sub-barrier certificate (CSBC)
Cite this review
Pith. "Pith review of From Formal Methods to Data-Driven Safety Certificates of Unknown Large-Scale Networks." pith.science (2026). https://pith.science/paper/U4ZCIM3R
@misc{pith2026250809520,
author = {Pith},
title = {Pith review of: From Formal Methods to Data-Driven Safety Certificates of Unknown Large-Scale Networks},
year = {2026},
howpublished = {\url{https://pith.science/paper/U4ZCIM3R}},
note = {Machine review of arXiv:2508.09520}
}
read the original abstract
In this work, we propose a data-driven scheme within a compositional framework with noisy data to design robust safety controllers in a fully decentralized fashion for large-scale interconnected networks with unknown mathematical dynamics. Despite the network's high dimensionality and the inherent complexity of its unknown model, which make it intractable, our approach effectively addresses these challenges by (i) treating the network as a composition of smaller subsystems, and (ii) collecting noisy data from each subsystem's trajectory to design a control sub-barrier certificate (CSBC) and its corresponding local controller. To achieve this, our proposed scheme only requires a noise-corrupted single input-state trajectory from each unknown subsystem up to a specified time horizon, satisfying a certain rank condition. Subsequently, under a small-gain compositional reasoning, we compose those CSBC, derived from noisy data, and formulate a control barrier certificate (CBC) for the unknown network, ensuring its safety over an infinite time horizon, while providing correctness guarantees. We offer a data-dependent sum-of-squares (SOS) optimization program for computing CSBC alongside local controllers of subsystems. We illustrate that while the computational complexity of designing a CBC and its safety controller grows polynomially with network dimension using SOS optimization, our compositional data-driven approach significantly reduces it to a linear scale concerning the number of subsystems. We demonstrate the capability of our data-driven approach on multiple physical networks involving unknown models and a range of interconnection topologies.
Reference graph
Works this paper leans on
-
[1]
C. Baier and J.-P. Katoen, Principles of model checking. 1em plus 0.5em minus 0.4em MIT press, 2008
work page 2008
-
[2]
Tabuada, Verification and control of hybrid systems: A symbolic approach
P. Tabuada, Verification and control of hybrid systems: A symbolic approach . 1em plus 0.5em minus 0.4em Springer Science & Business Media, 2009
work page 2009
- [3]
-
[4]
A. Girard and G. J. Pappas, ``Approximation M etrics for D iscrete and C ontinuous S ystems,'' IEEE Transactions on Automatic Control, vol. 52, no. 5, pp. 782--798, 2007
work page 2007
-
[5]
A. A. Julius and G. J. Pappas, ``Approximations of stochastic hybrid systems,'' IEEE Transactions on Automatic Control, vol. 54, no. 6, pp. 1193--1203, 2009
work page 2009
- [6]
- [7]
-
[8]
A. D. Ames, S. Coogan, M. Egerstedt, G. Notomista, K. Sreenath, and P. Tabuada, ``Control barrier functions: Theory and applications,'' in Proceedings of the 18th European Control Conference (ECC), 2019, pp. 3420--3431
work page 2019
Show all 52 references
-
[9]
Wieland and F
P. Wieland and F. Allg \"o wer, ``Constructive safety using control barrier functions,'' IFAC Proceedings Volumes, vol. 40, no. 12, pp. 462--467, 2007
2007
-
[10]
W. Xiao, C. G. Cassandras, and C. Belta, Safe Autonomy with Control Barrier Functions: Theory and Applications. 1em plus 0.5em minus 0.4em Springer, 2023
2023
-
[11]
W. Luo, W. Sun, and A. Kapoor, ``Multi- R obot C ollision A voidance under U ncertainty with P robabilistic S afety B arrier C ertificates,'' in Advances in N eural I nformation P rocessing S ystems , vol. 33, 2020, pp. 372--383
2020
-
[12]
Luo and T
Y. Luo and T. Ma, ``Learning barrier certificates: Towards safe reinforcement learning with zero training-time violations,'' in Advances in N eural I nformation P rocessing S ystems , vol. 34, 2021, pp. 25\,621--25\,632
2021
-
[13]
Lavaei and E
A. Lavaei and E. Frazzoli, ``Compositional controller synthesis for interconnected stochastic systems with markovian switching,'' in 2022 American Control Conference (ACC), 2022, pp. 4838--4843
2022
-
[14]
Wooding, V
B. Wooding, V. Horbanov, and A. Lavaei, `` PRoTECT : Parallelized construction of safety barrier certificates for nonlinear polynomial systems,'' arXiv:2404.14804, 2024
2024 arXiv
-
[15]
Lavaei and E
A. Lavaei and E. Frazzoli, ``Scalable synthesis of safety barrier certificates for networks of stochastic switched systems,'' IEEE Transactions on Automatic Control, vol. 69, no. 11, pp. 7294--7309, 2024
2024
-
[16]
Zaker, O
M. Zaker, O. Akbarzadeh, B. Samari, and A. Lavaei, ``Compositional design of safety controllers for large-scale stochastic hybrid systems,'' arXiv: 2409.10018, 2024
2024 arXiv
-
[17]
Lavaei, S
A. Lavaei, S. Soudjani, A. Abate, and M. Zamani, ``Automated verification and synthesis of stochastic hybrid systems: A survey,'' Automatica, vol. 146, 2022
2022
-
[18]
Swikir and M
A. Swikir and M. Zamani, ``Compositional synthesis of finite abstractions for networks of systems: A small-gain approach,'' Automatica, vol. 107, pp. 551--561, 2019
2019
-
[19]
Nejati and M
A. Nejati and M. Zamani, ``Compositional C onstruction of F inite MDP s for C ontinuous- T ime S tochastic S ystems: A D issipativity A pproach,'' IFAC-PapersOnLine, vol. 53, no. 2, pp. 1962--1967, 2020
1962
-
[20]
Lavaei, ``Automated verification and control of large-scale stochastic cyber-physical systems: Compositional techniques,'' Ph.D
A. Lavaei, ``Automated verification and control of large-scale stochastic cyber-physical systems: Compositional techniques,'' Ph.D. dissertation, PhD Thesis, Technische Universit \"a t M \"u nchen, 2019
2019
-
[21]
Nejati and M
A. Nejati and M. Zamani, ``From D issipativity T heory to C ompositional C onstruction of C ontrol B arrier C ertificates,'' Leibniz Transactions on Embedded Systems, vol. 8, no. 2, pp. 06--1, 2022
2022
-
[22]
Hou and Z
Z. Hou and Z. Wang, ``From model-based control to data-driven control: Survey, classification and perspective,'' Information Sciences, vol. 235, pp. 3--35, 2013
2013
-
[23]
D \"o rfler, F.and Coulson and I
J. D \"o rfler, F.and Coulson and I. Markovsky, ``Bridging direct and indirect data-driven control formulations via regularizations and relaxations,'' IEEE Transactions on Automatic Control, vol. 68, no. 2, pp. 883--897, 2022
2022
-
[24]
Nejati, A
A. Nejati, A. Lavaei, P. Jagtap, S. Soudjani, and M. Zamani, ``Formal verification of unknown discrete-and continuous-time systems: A data-driven approach,'' IEEE Transactions on Automatic Control, vol. 68, no. 5, pp. 3011--3024, 2023
2023
-
[25]
Rotulo, C
M. Rotulo, C. De Persis , and P. Tesi, ``Online learning of data-driven controllers for unknown switched linear systems,'' Automatica, vol. 145, 2022
2022
-
[26]
Nejati and M
A. Nejati and M. Zamani, ``Data-driven synthesis of safety controllers via multiple control barrier certificates,'' IEEE Control Systems Letters, vol. 7, pp. 2497--2502, 2023
2023
-
[27]
A. Lavaei, ``Symbolic A bstractions with G uarantees: A D ata- D riven D ivide-and- C onquer S trategy,'' in Proceedings of the 62nd IEEE Conference on Decision and Control (CDC), 2023, pp. 7994--7999
2023
-
[28]
Bisoffi, C
A. Bisoffi, C. De Persis, and P. Tesi, ``Controller design for robust invariance from noisy data,'' IEEE Transactions on Automatic Control, 2022
2022
-
[29]
Bartocci, L
E. Bartocci, L. Bortolussi, and G. Sanguinetti, ``Data- D riven S tatistical L earning of T emporal L ogic P roperties,'' in Formal Modeling and Analysis of Timed Systems, 2014, pp. 23--37
2014
-
[30]
Nejati, B
A. Nejati, B. Zhong, M. Caccamo, and M. Zamani, ``Data-driven controller synthesis of unknown nonlinear polynomial systems via control barrier certificates,'' in Learning for Dynamics and Control Conference, 2022, pp. 763--776
2022
-
[31]
Akbarzadeh, M
O. Akbarzadeh, M. Ashoori, and A. Lavaei, ``Learning robust safety controllers for uncertain input-affine polynomial systems,'' 64th IEEE Conference on Decision and Control (CDC 2025), 2025
2025
-
[32]
Samari, O
B. Samari, O. Akbarzadeh, M. Zaker, and A. Lavaei, ``From a single trajectory to safety controller synthesis of discrete-time nonlinear polynomial systems,'' IEEE Control Systems Letters, vol. 8, pp. 3123--3128, 2024
2024
-
[33]
G. C. Calafiore and M. C. Campi, ``The scenario approach to robust control design,'' IEEE Transactions on Automatic Control, vol. 51, no. 5, pp. 742--753, 2006
2006
-
[34]
Mohajerin Esfahani, T
P. Mohajerin Esfahani, T. Sutter, and J. Lygeros, ``Performance B ounds for the S cenario A pproach and an E xtension to a C lass of N on- C onvex P rograms,'' IEEE Transactions on Automatic Control, vol. 60, no. 1, pp. 46--58, 2014
2014
-
[35]
J. C. Willems, P. Rapisarda, I. Markovsky, and B. L. De Moor , ``A note on persistency of excitation,'' Systems & Control Letters, vol. 54, no. 4, pp. 325--329, 2005
2005
-
[36]
S. H. Strogatz, Nonlinear dynamics and chaos: with applications to physics, biology, chemistry, and engineering. 1em plus 0.5em minus 0.4em Chapman and Hall/CRC, 2024
2024
-
[37]
T. J. Willmore, ``The D efinition of L ie D erivative,'' Proceedings of the Edinburgh Mathematical Society, vol. 12, no. 1, p. 27–29, 1960
1960
-
[38]
H. J. Van Waarde, M. K. Camlibel, and M. Mesbahi, ``From noisy data to feedback controllers: N onconservative design via a matrix S -lemma,'' IEEE Transactions on Automatic Control, vol. 67, no. 1, pp. 162--175, 2020
2020
-
[39]
De Persis and P
C. De Persis and P. Tesi, ``Formulas for data-driven control: Stabilization, optimality, and robustness,'' IEEE Transactions on Automatic Control, vol. 65, no. 3, pp. 909--924, 2019
2019
-
[40]
Bhatia and C
R. Bhatia and C. Davis, ``A C auchy- S chwarz inequality for operators with applications,'' Linear algebra and its applications, vol. 223, pp. 119--129, 1995
1995
-
[41]
W. H. Young, ``On classes of summable functions and their F ourier series,'' Proceedings of the Royal Society of London. Series A, Containing Papers of a Mathematical and Physical Character, vol. 87, no. 594, pp. 225--229, 1912
1912
-
[42]
Ando, Matrix Y oung I nequalities
T. Ando, Matrix Y oung I nequalities . 1em plus 0.5em minus 0.4em Birkh \"a user Basel, 1995, pp. 33--38
1995
-
[43]
Zhang, The S chur C omplement and I ts A pplications
F. Zhang, The S chur C omplement and I ts A pplications . 1em plus 0.5em minus 0.4em Springer Science & Business Media, 2006, vol. 4
2006
-
[44]
Prajna, A
S. Prajna, A. Papachristodoulou, P. Seiler, and P. Parrilo, `` SOSTOOLS : control applications and new developments,'' in Proceedings of IEEE International Conference on Robotics and Automation, 2004, pp. 315--320
2004
-
[45]
ApS, The MOSEK optimization toolbox for MATLAB manual
M. ApS, The MOSEK optimization toolbox for MATLAB manual. Version 10.1. , 2024. [Online]. Available: http://docs.mosek.com/latest/toolbox/index.html
2024
-
[46]
L \'o pez-Mancilla, G
D. L \'o pez-Mancilla, G. L \'o pez-Cahuich, C. Posadas-Castillo, C. Casta \ n eda, J. Garc \' a-L \'o pez, J. V \'a zquez-Guti \'e rrez, and E. Tlelo-Cuautle, ``Synchronization of complex networks of identical and nonidentical chaotic systems via model-matching control,'' PLO...
2019
-
[47]
H. K. Khalil, Nonlinear S ystems , 3rd ed. 1em plus 0.5em minus 0.4em Prentice Hall, 2002
2002
-
[48]
Z. Wang, J. Cao, Z. Duan, and X. Liu, ``Synchronization of coupled duffing-type oscillator dynamical networks,'' Neurocomputing, vol. 136, pp. 162--169, 2014
2014
-
[49]
H. Wang, Z. Han, W. Zhang, and Q. Xie, ``Chaotic synchronization and secure communication based on descriptor observer,'' Nonlinear Dynamics, vol. 57, no. 1, pp. 69--73, 2009
2009
-
[50]
E. N. Lorenz, ``Deterministic N onperiodic F low,'' Journal of Atmospheric Sciences, vol. 20, no. 2, pp. 130 -- 141, 1963
1963
-
[51]
J. C. Sprott, Elegant Chaos. 1em plus 0.5em minus 0.4em WORLD SCIENTIFIC, 2010
2010
-
[52]
IEEEtrantools_doc.txt
11em plus .33em minus .07em @technote 4000 4000 100 4000 4000 500 `\.=1000 = #1 #1 #1 0pt [0pt][0pt] #1 * \| ** #1 \@IEEEauthorblockNstyle \@IEEEauthorblockAstyle \@IEEEauthordefaulttextstyle \@IEEEauthorblockconfadjspace -0.25em \@IEEEauthorblockNtopspace 0.0ex \@IEEEauthorbl...
2015
Reviewed August 5, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.