Pith. sign in

REVIEW 4 major objections 6 minor 49 references

Neural Control and Certificate Repair via Runtime Monitoring

T0 review · 4 major / 6 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read The same certificate functions that prove safety in classical control can be repurposed as runtime monitors to repair neural policies in the black-box setting.

desk verdict A useful monitor-retrain loop for black-box control repair, but the certificate-repair claim rests on an unvalidated finite-difference proxy that is used to monitor, train, and evaluate, so the reported BR/NDR gains may be self-fulfilling. read the letter →

arxiv 2412.12996 v1 pith:VCFOLTMN submitted 2024-12-17 cs.LG cs.AI

Emily Yu , {DJ}or{j̣e Žikelić , Thomas A. Henzinger This is my paper · ORCID
classification cs.LGcs.AI
keywords runtimemonitoringneuralnetworkcontrolcertificatefunctionsbarrierLyapunovblack-boxdynamicspolicyrepairsafety
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

This paper tries to establish that a runtime-monitoring loop can repair neural network control policies and their certificate functions in the black-box setting, where the system dynamics are unknown. The authors propose watching trajectories with a monitor that checks both the property and the defining conditions of a barrier or Lyapunov function, then feeding the flagged states back into the certificate-condition loss to retrain the networks. On a drone delivery task and a ship navigation task, the repaired policies lift the safety rate from 93.99% to at least 98.67%, with the best configuration reaching 99.13%, and the barrier's non-decreasing condition satisfaction rising from 45.38% to over 90%. The paper claims empirical repair and improvement, not formal guarantees, in the black-box setting.

What carries the argument

The load-bearing object is the monitor-learner loop, built on certificate functions: a barrier function certifies that a safe set is never left, and a Lyapunov function certifies convergence to a goal. A runtime monitor observes discrete states along a trajectory and emits a verdict on either the property or the certificate conditions: CertPM checks them directly, approximating the Lie derivative of the certificate by the finite difference $(B(x_{n+1})-B(x_n))/(t_{n+1}-t_n)$, while PredPM estimates time-to-violation by solving a minimal-time reach problem with bounded acceleration. Flagged states are partitioned into the three certificate-condition training sets and fed into the standard certificate loss, so retraining is guided by the certificate's own proof obligations rather than by post-hoc property violations alone.

What would settle it

Run the same repair loop on several black-box control tasks whose dynamics are secretly known, compare every monitor verdict with an exact white-box certificate check at the same states, and check whether any repaired policy ends with a lower safety rate or certificate satisfaction rate than the initial policy; a case with frequent false monitor verdicts or a performance drop after repair would falsify the paper's central claim.

Watch

Extended reading notes

Core claim

The central claim is that certificate functions intended to prove safety and stability can double as runtime monitors in the black-box setting, and that the behaviors they flag provide enough training signal to repair both the policy and the certificate. The paper introduces CertPM, which checks the initial, safety, and non-decreasing conditions of a barrier function (and the analogous Lyapunov conditions) on observed states, and PredPM, which estimates the remaining time until each condition is violated and warns before the violation occurs. The repaired networks are retrained with the same loss terms used in learning-based control, but on data collected only from monitored violations. The reported experiments show a repaired drone policy reaching a 99.13% safety rate and 100% time inside the barrier's safe region, and a ship benchmark where a fixed policy's barrier function has far fewer certificate violations after repair.

Load-bearing premise

The finite-difference estimate of the Lie derivative is only a reliable violation signal if the sampling interval is small enough relative to the unknown smoothness of the dynamics and the certificate, so the monitor's training labels could be noisy when that balance is not met.

Editorial extensions

If this is right

  • Using either CertPM or PredPM for repair improves the drone policy's safety rate from 93.99% to at least 98.67%, with the best configuration reaching 99.13%.
  • Barrier condition satisfaction improves to 100% for the time spent inside the safe region and to about 91.67% for the non-decreasing condition, up from 87.03% and 45.38% respectively.
  • When the control policy is kept fixed, the certificate can still be repaired, and the number of barrier-condition violations on the ship benchmark drops sharply after one and two rounds of repair.
  • PredPM's estimate of time until the safety-condition violation becomes negative before the estimate of time until reaching the unsafe set, so it can issue warnings before a violation occurs.
  • The paper reports no observed case where repaired performance was worse than the initial policy, while noting that no formal correctness guarantee is provided.

Reading between the lines

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

  • Extension: the finite-difference error bound used by CertPM depends on Lipschitz constants that are unknown to the black-box user, so a natural improvement would be adaptive sampling that shrinks the time step when successive verdicts are unstable.
  • Extension: the same monitor-learner pattern should transfer to other trajectory-checkable certificate families, such as contraction metrics or control barrier functions with input limits, because the repair only needs a loss term for each certificate condition.
  • Extension: PredPM's predictive value could be quantified against a white-box simulator with known dynamics, comparing its time-to-violation estimates with true violation times to measure false-warning rates the paper does not report.
  • Extension: the loop naturally acts as a hard-example data filter, which may make retraining data-efficient relative to replaying all visited states; this could be tested by comparing repair with random state sampling against monitor-selected states at equal data budgets.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

Summary. The paper proposes a monitor-learner framework for repairing neural network control policies and certificate functions (barrier and Lyapunov) when the system dynamics are unknown. Two monitors are presented: CertPM checks property and certificate conditions on observed trajectories using a finite-difference approximation of the Lie derivative, and PredPM predicts time-to-violation using a simplified kinematic model. Violating states are collected as counterexamples and used to retrain the policy and certificate with a standard certificate-condition loss. Experiments on drone and ship benchmarks report improved safety rates and certificate condition satisfaction rates after repair, with an additional comparison against a policy-only baseline.

Significance. The framework addresses a real gap: repairing certificates in black-box settings, where no prior method appears to combine runtime monitoring with certificate-aware retraining. The idea of using certificate conditions as runtime monitors is natural but useful, and the reported safety-rate improvements on the two benchmarks are promising. The paper honestly notes that no formal correctness guarantees are provided. However, the certificate-repair claims rely on an unvalidated finite-difference proxy for the Lie derivative, and the statistical support for the headline numbers is weak. If the proxy issue is addressed and the experiments are properly quantified, the framework could be a practical tool for improving learned controllers without access to the dynamics.

major comments (4)
  1. [Runtime Monitoring Policies and Certificates (Non-decreasing condition); eq. (1); Table 1] The finite-difference approximation of the Lie derivative, LfB(x_n) ≈ (B(x_{n+1}) - B(x_n))/(t_{n+1} - t_n), has an error bound that depends on the unknown dynamics' Lipschitz constant, and the experiments fix Δt = 0.1 without validating that the bound is small. Because the same approximation is used in the monitor, in the retraining loss (eq. 1), and in the NDR metric of Table 1, the reported improvements in BR and NDR may reflect fitting to the proxy rather than satisfaction of a genuine certificate condition. The independent SR improvement is encouraging, but it does not by itself establish that the repaired barrier function is a valid certificate. Please validate the proxy against the true dynamics on a subset, or provide conservative margins based on data-driven Lipschitz estimates.
  2. [Experimental Evaluation (Table 1)] All results are averages over 50 executions, but the paper reports no error bars, confidence intervals, or significance tests. The claims that CertPM and PredPM lead to 'significantly higher safety rates' are therefore not statistically supported. Report per-run distributions and paired comparisons (e.g., bootstrap or permutation tests) for SR, BR, and NDR.
  3. [Results: RQ3 / Figure 3] The predictive power of PredPM is evaluated only by plotting the estimates v_U, v_S, v_N for two executions. No quantitative metric such as precision/recall of warnings before actual violations, or lead-time accuracy, is provided. Moreover, the prediction model (dx/dt=v, dv/dt=a with |a|≤a_max) is an unvalidated simplification of the actual, unknown dynamics. Thus the claim that PredPM 'can predict safety violations before they happen' is not established.
  4. [Predictive Policy Monitor] The verdict rule is internally inconsistent: the text first states that PredPM issues a verdict based on whether estimated remaining times are 'below' the predefined thresholds, then defines the verdict as vU > ξU or vS > ξS or vN > ξN. The Appendix's statement that zero thresholds make PredPM equivalent to CertPM is only consistent with the 'below' reading. This contradiction makes it unclear how the threshold configurations in Table 1 should be interpreted. Please correct the decision rule and clarify the sign convention for vU, vS, and vN.
minor comments (6)
  1. [Preliminaries] The word 'asympotically' should be 'asymptotically'.
  2. [Benchmarks] In the description of the drone state, 'row and pitch angles' should be 'roll and pitch angles'.
  3. [Appendix (Additional Experiments)] The words 'incoperating' and 'signiciant' are misspellings of 'incorporating' and 'significant'.
  4. [Algorithm 1] The text describes a loop executed until the monitor finds no more violations, but the pseudocode shows a single pass over D trajectories; please specify the outer-loop termination condition or revise the surrounding description.
  5. [Table 1] The baseline row leaves BR and NDR empty; clarify whether these values were not measured, not applicable, or intentionally omitted.
  6. [Figure 2] The y-axis label is unclear; please state whether the values are per-execution violation counts, aggregate counts, or rates, and label the axes accordingly.

Circularity Check

1 steps flagged · score 6.0 of 10

Certificate-repair claim is evaluated with the same finite-difference certificate predicate used as the training objective; safety-rate gains remain independent evidence.

  1. fitted input called prediction [Certificate Policy Monitor; Neural Policy and Certificate Repair (Algorithm 1, eq. 1); Table 1 (RQ1)]
    "The certificate violation verdict for the Non-decreasing condition in Proposition 1 is issued if B(xn) ≥ 0 but ‘Lf B(xn) + B(xn) < 0 (with ‘Lf B approximated by (B(x_{n+1})−B(x_n))/(t_{n+1}−t_n)). Algorithm 1 forms Drepair_Non-dec = DNew-data ∩ {x | B(x) ≥ 0} and retrains with LNon-dec = 1/|DNon-dec| Σ max(−‘Lfθ Bν(x) − Bν(x), 0). Table 1: “NDR is the proportion of time during which the barrier function satisfies the non-decreasing condition.”"

    The monitor's verdict, the repair loss, and the reported NDR metric are the same predicate evaluated with the same finite-difference approximation of the Lie derivative. Retraining B on states flagged by that predicate directly minimizes the quantity that NDR measures; hence the reported improvement in NDR (and similarly BR via LSafe) is a fit to the evaluation criterion, not independent evidence that B is a valid barrier under the true dynamics. The safety-rate SR is an independent signal, but the certificate-repair claim itself is assessed with the training objective.

full rationale

The only substantial circularity is that the certificate-repair result is measured by the same condition that the repair loss optimizes. The monitor flags states using the finite-difference approximation of the Lie derivative, Algorithm 1 retrains B with a loss containing exactly that predicate, and Table 1's NDR reports the frequency of that same predicate; thus the BR/NDR improvements are largely a report of the training objective. This is not a fully circular derivation, because the safety rate SR is an independent metric and the framework is counterexample-guided retraining rather than a proof that assumes its conclusion; also, the finite-difference error bound is cited from external work (Nejati et al.), and the authors' self-citation to Zikelic et al. 2022 appears only in a limitation remark and is not load-bearing. The black-box choice of Δt=0.1 without known Lipschitz constants is a correctness risk, not a circularity. Overall, the policy-repair claim has independent support, but the certificate-repair claim reduces in part to fitting its own evaluation metric, so a partial-circularity score of 6 is appropriate.

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

The method rests on standard certificate definitions and the SABLAS training loss, plus the assumption that finite-difference monitoring with unknown Lipschitz constants and PredPM's simplified kinematics produce useful training data. No new physical entities are postulated.

free parameters (3)
  • PredPM thresholds ξ_U, ξ_S, ξ_N = 0,0,-1 / 0,1,-5 / 2,2,0 (three configurations)
    User-provided sensitivity thresholds in PredPM; the paper selects three configurations based on observed numbers of detected violations, which makes the reported D_NEW partly outcome-dependent.
  • Maximum acceleration a_max = not specified
    Physical bound assumed for the simplified kinematics in PredPM's time-to-violation estimates; value is not measured or reported.
  • Time step Δt and observation count N = 0.1 s; 1200 (DroneEnv) and 2000 (ShipEnv)
    Discretization choices that determine the accuracy of the finite-difference Lie derivative approximation and the monitoring frequency; the error bound depends on them.
assumptions (4)
  • domain assumption System dynamics f is Lipschitz continuous with bounded constants C_f and C_B.
    Stated in Preliminaries; used for the finite-difference error bound in CertPM.
  • domain assumption Finite-difference approximation with error bound from (Nejati et al. 2023) is accurate enough to detect true certificate violations at the chosen Δt.
    The monitor's non-decreasing/decreasing condition verdicts rely on this approximation; the bound depends on Lipschitz constants that are unknown in the black-box setting.
  • ad hoc to paper PredPM's simplified kinematics dx/dt=v, dv/dt=a with |a|≤a_max adequately models the actual system for prediction.
    The time-to-violation estimates for v_U, v_S, v_N are computed under constant-acceleration kinematics, not the unknown true dynamics.
  • domain assumption Retraining the policy and certificate on the original SABLAS loss with newly collected violating states improves their correctness.
    This is the core repair premise; it is empirically evaluated but not proven, and the paper acknowledges no correctness guarantees.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Neural Control and Certificate Repair via Runtime Monitoring." pith.science (2026). https://pith.science/paper/VCFOLTMN

@misc{pith2026241212996,
  author       = {Pith},
  title        = {Pith review of: Neural Control and Certificate Repair via Runtime Monitoring},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VCFOLTMN}},
  note         = {Machine review of arXiv:2412.12996}
}
read the original abstract

Learning-based methods provide a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. To ensure the satisfaction of a safety property, learning-based methods jointly learn a control policy together with a certificate function for the property. Popular examples include barrier functions for safety and Lyapunov functions for asymptotic stability. While there has been significant progress on learning-based control with certificate functions in the white-box setting, where the correctness of the certificate function can be formally verified, there has been little work on ensuring their reliability in the black-box setting where the system dynamics are unknown. In this work, we consider the problems of certifying and repairing neural network control policies and certificate functions in the black-box setting. We propose a novel framework that utilizes runtime monitoring to detect system behaviors that violate the property of interest under some initially trained neural network policy and certificate. These violating behaviors are used to extract new training data, that is used to re-train the neural network policy and the certificate function and to ultimately repair them. We demonstrate the effectiveness of our approach empirically by using it to repair and to boost the safety rate of neural network policies learned by a state-of-the-art method for learning-based control on two autonomous system control tasks.

Figures

Figures reproduced from arXiv: 2412.12996 by the authors.

Figure 1
Figure 1. The monitor-learner framework. interest is to compute a certificate function for that prop￾erty (Dawson, Gao, and Fan 2023). A certificate function is a mathematical object which proves that the system under the control policy indeed satisfies the property. Common ex￾amples of certificate functions include Lyapunov functions for stability (Khalil 2002) and barrier functions for safety set invariance (Prajna and Jadb… view at source ↗
Figure 2
Figure 2. The change in the number of certificate violations [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Estimates vU , vS, and vN for two different systems executions computed by the PredPM for the drone and the ship benchmarks. portance of monitoring both neural policies and certificates, we also compare our method against the baseline approach. The baseline is the simple monitor described in the Intro￾duction, which only monitors a neural policy, flags traces that reach an unsafe state and adds these states to re-tr… view at source ↗
Figures from the paper (3 more)
Figure 6
Figure 6. Figure 6: The change in the percentage of warnings over [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 4
Figure 4. Figure 4: Repairing a reference policy with a Lyapunov [PITH_FULL_IMAGE:figures/full_fig_p012_4.png]
Figure 5
Figure 5. Figure 5: Comparisons of BR and NDR for repairing the [PITH_FULL_IMAGE:figures/full_fig_p012_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

49 extracted references · 40 canonical work pages

  1. [1]

    , " * write output.state after.block = add.period write newline

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.a...

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

  3. [3]

    Abate, A.; Ahmed, D.; Edwards, A.; Giacobbe, M.; and Peruffo, A. 2021 a . FOSSIL: a software tool for the formal synthesis of lyapunov functions and barrier certificates using neural networks. In Bogomolov, S.; and Jungers, R. M., eds., HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21,...

    work page 2021

  4. [4]

    Abate, A.; Ahmed, D.; Giacobbe, M.; and Peruffo, A. 2021 b . Formal Synthesis of Lyapunov Neural Networks. IEEE Control. Syst. Lett. , 5(3): 773--778

    work page 2021

  5. [5]

    Abate, A.; Edwards, A.; Giacobbe, M.; Punchihewa, H.; and Roy, D. 2023. Quantitative Verification with Neural Networks. In P \' e rez, G. A.; and Raskin, J., eds., 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium , volume 279 of LIPIcs, 22:1--22:18. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik

    work page 2023

  6. [6]

    Achiam, J.; Held, D.; Tamar, A.; and Abbeel, P. 2017. Constrained policy optimization. In International Conference on Machine Learning, 22--31. PMLR

    work page 2017

  7. [7]

    A.; and Majumdar, A

    Ahmadi, A. A.; and Majumdar, A. 2016. Some applications of polynomial optimization in operations research and real-time decision making. Optim. Lett., 10(4): 709--729

    work page 2016

  8. [8]

    Alshiekh, M.; Bloem, R.; Ehlers, R.; K \" o nighofer, B.; Niekum, S.; and Topcu, U. 2018. Safe Reinforcement Learning via Shielding. In McIlraith, S. A.; and Weinberger, K. Q., eds., Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAA...

    work page 2018

Show all 49 references
  1. [9]

    Altman, E. 1999. Constrained Markov decision processes, volume 7. CRC Press

    1999

  2. [10]

    D.; Grizzle, J

    Ames, A. D.; Grizzle, J. W.; and Tabuada, P. 2014. Control barrier function based quadratic programs with application to adaptive cruise control. In CDC , 6271--6278. IEEE

    2014

  3. [11]

    F.; Schulman, J.; and Man \' e , D

    Amodei, D.; Olah, C.; Steinhardt, J.; Christiano, P. F.; Schulman, J.; and Man \' e , D. 2016. Concrete Problems in AI Safety. CoRR, abs/1606.06565

    2016 arXiv

  4. [12]

    A.; Lechner, M.; and Zikelic, D

    Ansaripour, M.; Chatterjee, K.; Henzinger, T. A.; Lechner, M.; and Zikelic, D. 2023. Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems. In Andr \' e , \' E .; and Sun, J., eds., Automated Technology for Verification and Analysis - 21st Inter...

    2023

  5. [13]

    Bauer - Marquart, F.; Boetius, D.; Leue, S.; and Schilling, C. 2022. SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks. In Legunsen, O.; and Rosu, G., eds., Model Checking Software - 28th International Symposium, SPIN 2022, Virtual Event, May 21, 2022, P...

    2022

  6. [14]

    o nighofer, B.; K \

    Bloem, R.; K \" o nighofer, B.; K \" o nighofer, R.; and Wang, C. 2015. Shield Synthesis: - Runtime Enforcement for Reactive Systems. In TACAS , volume 9035 of Lecture Notes in Computer Science, 533--548. Springer

    2015

  7. [15]

    Carr, S.; Jansen, N.; Junges, S.; and Topcu, U. 2023. Safe Reinforcement Learning via Shielding under Partial Observability. In AAAI , 14748--14756. AAAI Press

    2023

  8. [16]

    Chang, Y.; Roohi, N.; and Gao, S. 2019. Neural Lyapunov Control. In Wallach, H. M.; Larochelle, H.; Beygelzimer, A.; d'Alch \' e - Buc, F.; Fox, E. B.; and Garnett, R., eds., Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processi...

    2019

  9. [17]

    A.; Lechner, M.; and Zikelic, D

    Chatterjee, K.; Henzinger, T. A.; Lechner, M.; and Zikelic, D. 2023. A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems. In Sankaranarayanan, S.; and Sharygina, N., eds., Tools and Algorithms for the Construction and Analysis of ...

    2023

  10. [18]

    A.; and Ghavamzadeh, M

    Chow, Y.; Nachum, O.; Du \' e \ n ez - Guzm \' a n, E. A.; and Ghavamzadeh, M. 2018. A Lyapunov-based Approach to Safe Reinforcement Learning. In Bengio, S.; Wallach, H. M.; Larochelle, H.; Grauman, K.; Cesa - Bianchi, N.; and Garnett, R., eds., Advances in Neural Information ...

    2018

  11. [19]

    Dawson, C.; Gao, S.; and Fan, C. 2023. 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

  12. [20]

    Dawson, C.; Qin, Z.; Gao, S.; and Fan, C. 2021. Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions. In Faust, A.; Hsu, D.; and Neumann, G., eds., Conference on Robot Learning, 8-11 November 2021, London, UK , volume 164 of Proceedings of Machine Learning Res...

    2021

  13. [21]

    Falcone, Y.; and Pinisetty, S. 2019. On the Runtime Enforcement of Timed Properties. In RV , volume 11757 of Lecture Notes in Computer Science, 48--69. Springer

    2019

  14. [22]

    Fossen, T. I. 2000. A survey on nonlinear ship control: From theory to practice. IFAC Proceedings Volumes, 33(21): 1--16

    2000

  15. [23]

    Garc \' a, J.; and Fern \' a ndez, F. 2015. A comprehensive survey on safe reinforcement learning. J. Mach. Learn. Res., 16: 1437--1480

    2015

  16. [24]

    Geibel, P. 2006. Reinforcement Learning for MDPs with Constraints. In F \" u rnkranz, J.; Scheffer, T.; and Spiliopoulou, M., eds., Machine Learning: ECML 2006, 17th European Conference on Machine Learning, Berlin, Germany, September 18-22, 2006, Proceedings , volume 4212 of L...

    2006

  17. [25]

    Khalil, H. K. 2002. Control of nonlinear systems. Prentice Hall, New York, NY

    2002

  18. [26]

    P.; and Ba, J

    Kingma, D. P.; and Ba, J. 2014. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980

    2014 arXiv

  19. [27]

    K \" o nighofer, B.; Lorber, F.; Jansen, N.; and Bloem, R. 2020. Shield Synthesis for Reinforcement Learning. In ISoLA (1) , volume 12476 of Lecture Notes in Computer Science, 290--306. Springer

    2020

  20. [28]

    Lechner, M.; Zikelic, D.; Chatterjee, K.; and Henzinger, T. A. 2022. Stability Verification in Stochastic Control Systems via Neural Network Supermartingales. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applicat...

    2022

  21. [29]

    Lyu, D.; Song, J.; Zhang, Z.; Wang, Z.; Zhang, T.; Ma, L.; and Zhao, J. 2023. AutoRepair: Automated Repair for AI-Enabled Cyber-Physical Systems under Safety-Critical Conditions. CoRR, abs/2304.05617

    2023 arXiv

  22. [30]

    B.; Calvert, S

    Mathiesen, F. B.; Calvert, S. C.; and Laurenti, L. 2023. Safety Certification for Stochastic Systems via Neural Barrier Functions. IEEE Control. Syst. Lett. , 7: 973--978

    2023

  23. [31]

    Mazouz, R.; Muvvala, K.; Ratheesh, A.; Laurenti, L.; and Lahijanian, M. 2022. Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions. In Koyejo, S.; Mohamed, S.; Agarwal, A.; Belgrave, D.; Cho, K.; and Oh, A., eds., Advances in Neural Information...

    2022

  24. [32]

    A.; Veness, J.; Bellemare, M

    Mnih, V.; Kavukcuoglu, K.; Silver, D.; Rusu, A. A.; Veness, J.; Bellemare, M. G.; Graves, A.; Riedmiller, M. A.; Fidjeland, A.; Ostrovski, G.; Petersen, S.; Beattie, C.; Sadik, A.; Antonoglou, I.; King, H.; Kumaran, D.; Wierstra, D.; Legg, S.; and Hassabis, D. 2015. Human-leve...

    2015

  25. [33]

    Nejati, A.; Lavaei, A.; Jagtap, P.; Soudjani, S.; and Zamani, M. 2023. Formal Verification of Unknown Discrete- and Continuous-Time Systems: A Data-Driven Approach. IEEE Trans. Autom. Control. , 68(5): 3011--3024

    2023

  26. [34]

    Prajna, S.; and Jadbabaie, A. 2004. Safety Verification of Hybrid Systems Using Barrier Certificates. In Alur, R.; and Pappas, G. J., eds., Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings , v...

    2004

  27. [35]

    Pranger, S.; K \" o nighofer, B.; Tappler, M.; Deixelberger, M.; Jansen, N.; and Bloem, R. 2021. Adaptive Shielding under Uncertainty. In ACC , 3467--3474. IEEE

    2021

  28. [36]

    Qin, Z.; Sun, D.; and Fan, C. 2022. Sablas: Learning Safe Control for Black-Box Dynamical Systems. IEEE Robotics Autom. Lett. , 7(2): 1928--1935

    2022

  29. [37]

    Qin, Z.; Zhang, K.; Chen, Y.; Chen, J.; and Fan, C. 2021. Learning Safe Multi-agent Control with Decentralized Neural Barrier Certificates. In ICLR . OpenReview.net

    2021

  30. [38]

    Renard, M.; Falcone, Y.; Rollet, A.; J \' e ron, T.; and Marchand, H. 2019. Optimal enforcement of (timed) properties with uncontrollable events. Math. Struct. Comput. Sci., 29(1): 169--214

    2019

  31. [39]

    M.; Berkenkamp, F.; and Krause, A

    Richards, S. M.; Berkenkamp, F.; and Krause, A. 2018. The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems. In 2nd Annual Conference on Robot Learning, CoRL 2018, Z \" u rich, Switzerland, 29-31 October 2018, Proceedings , volume...

    2018

  32. [40]

    Srinivasan, M.; Abate, M.; Nilsson, G.; and Coogan, S. 2021. Extent-compatible control barrier functions. Syst. Control. Lett., 150: 104895

    2021

  33. [41]

    S.; and Barto, A

    Sutton, R. S.; and Barto, A. G. 2018. Reinforcement learning: An introduction. MIT press

    2018

  34. [42]

    Zhang, H.; Wu, J.; Vorobeychik, Y.; and Clark, A. 2023. Exact Verification of ReLU Neural Control Barrier Functions. In Oh, A.; Naumann, T.; Globerson, A.; Saenko, K.; Hardt, M.; and Levine, S., eds., Advances in Neural Information Processing Systems 36: Annual Conference on N...

    2023

  35. [43]

    Zhao, H.; Zeng, X.; Chen, T.; and Liu, Z. 2020. Synthesizing barrier certificates using neural networks. In HSCC , 25:1--25:11. ACM

    2020

  36. [44]

    L.; and Zhang, M

    Zhi, D.; Wang, P.; Liu, S.; Ong, C. L.; and Zhang, M. 2024. Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems. In Gurfinkel, A.; and Ganesh, V., eds., Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada,...

    2024

  37. [45]

    Zhou, W.; Gao, R.; Kim, B.; Kang, E.; and Li, W. 2020. Runtime-Safety-Guided Policy Repair. In RV , volume 12399 of Lecture Notes in Computer Science, 131--150. Springer

    2020

  38. [46]

    Zhu, H.; Xiong, Z.; Magill, S.; and Jagannathan, S. 2019. An inductive synthesis framework for verifiable reinforcement learning. In McKinley, K. S.; and Fisher, K., eds., Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 20...

    2019

  39. [47]

    Zikelic, D.; Lechner, M.; Chatterjee, K.; and Henzinger, T. A. 2022. Learning Stabilizing Policies in Stochastic Control Systems. CoRR, abs/2205.11991

    2022 arXiv

  40. [48]

    A.; and Chatterjee, K

    Zikelic, D.; Lechner, M.; Henzinger, T. A.; and Chatterjee, K. 2023 a . Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees. In Williams, B.; Chen, Y.; and Neville, J., eds., Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-...

    2023

  41. [49]

    Zikelic, D.; Lechner, M.; Verma, A.; Chatterjee, K.; and Henzinger, T. A. 2023 b . Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees. In Oh, A.; Naumann, T.; Globerson, A.; Saenko, K.; Hardt, M.; and Levine, S., eds., Advances in Neural Informa...

    2023

Pith tools

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