pith. sign in

arxiv: 2606.18685 · v1 · pith:DEIVN5PInew · submitted 2026-06-17 · 💻 cs.LO · math.LO

Differential Equation Inductive Robustness Axiomatization

Andr\'e Platzer , Long Qian This is my paper

Pith reviewed 2026-06-26 19:19 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords robust safetypolynomial differential equationsaxiomatizationpolynomial invariantssubanalytic geometryhybrid dynamical systemsinductive safetyapproximate decidability
0
0 comments X

The pith

Robust safety of polynomial differential equation systems reduces completely to polynomial invariant proofs on bounded time horizons.

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

The paper establishes completeness for an axiomatization of robust safety in dynamical systems governed by polynomial differential equations over bounded time. It shows that safety properties for robust systems reduce uniformly to a sound axiomatization of polynomial invariants, which yields reliable logical proofs of correctness. This reduction holds for arbitrary bounded semialgebraic initial and post conditions even without positive separation at topological boundaries, by drawing on subanalytic geometry. The work also supplies approximate decidability: a computable procedure that, for any perturbation level delta, either outputs a symbolic proof or correctly identifies that the system fails to be robustly safe at that level. These results support inductive safety proofs for general hybrid dynamical systems.

Core claim

The axiomatization for robust safety is complete because safety properties of robust systems are uniformly reduced to a sound axiomatization of polynomial invariants, resulting in reliable logical proofs of correctness for dynamical systems with polynomial differential equations on bounded time horizons.

What carries the argument

The uniform reduction from robust safety properties to the sound axiomatization of polynomial invariants, supported by subanalytic geometry to handle general semialgebraic sets.

If this is right

  • Logical proofs of robust safety become available for general hybrid dynamical systems on bounded horizons.
  • Approximate decidability follows: for any perturbation parameter delta the procedure either produces a symbolic proof or decides the system is not robustly safe at level delta.
  • Inductive safety proofs extend beyond finite time horizons for hybrid systems.

Where Pith is reading between the lines

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

  • The completeness result may allow automated tools to generate proofs for a wider class of initial and post conditions than previously possible.
  • Similar reductions could be explored for other temporal properties such as reachability or liveness if analogous invariant axiomatizations exist.
  • Practical implementations might combine the axiomatization with real-algebraic decision procedures to produce concrete proof certificates.

Load-bearing premise

The reduction from robust safety properties to polynomial invariant axioms remains valid for arbitrary bounded semialgebraic initial and post conditions even without positive separation at their topological boundaries.

What would settle it

A concrete polynomial differential equation system on a bounded time horizon whose robust safety holds for given semialgebraic sets without boundary separation yet cannot be proved by the axiomatization, or where the approximate decision procedure fails to output a proof or a correct negative verdict for some delta.

Figures

Figures reproduced from arXiv: 2606.18685 by Andr\'e Platzer, Long Qian.

Figure 1
Figure 1. Figure 1: 1D Cart Inductiveness. The inductiveness of topological robustness is particularly pronounced in the safety verification of CPS or hybrid dynamical systems, where the underlying continuous dynamics 𝑥 ′ = 𝑝(𝑥) is generalized to 𝑥 ′ = 𝑝(𝑥, 𝑢), 𝑢′ = 0 with 𝑢 representing the control variables from discrete assignments. Such continuous dynamics are executed over (infinitely) many discrete steps, after each exe… view at source ↗
Figure 2
Figure 2. Figure 2: Proof Strategy interval [0, 𝑠], safety is established by leveraging the symbolic nature of polynomial ODEs with sufficiently accurate Taylor approximations and the FOLR definability of 𝐼, 𝑆 to prove that the trajectory is away from the unsafe set 𝑆 𝑐 . On the interval [𝑠,𝑇 ], safety can then be established by computability-theoretic methods with sufficiently accurate numerical approximations. The primary d… view at source ↗
Figure 3
Figure 3. Figure 3: Example of robust safety - flows progress into interior of safety set [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Non-uniform local progression. The following observation is immediate by construction. Proposition 4.9. Let 𝜑( ®𝑥) ∈ FOLR be a formula and 𝜃𝜑 its truth function. Then for all 𝑧® ∈ R 𝑛 , the following hold • 𝜃𝜑 (®𝑧) > 0 =⇒ ®𝑧 ∈ J𝜑K. In particular, if 𝜑 is of the form 𝜑 = Û 𝑖 Ü 𝑗 𝑒𝑖,𝑗 > 0 then 𝜃𝜑 (®𝑧) > 0 ⇐⇒ ®𝑧 ∈ J𝜑K. • 𝜃𝜑 (®𝑧) < 0 =⇒ ®𝑧 ∉ J𝜑K. In particular, if 𝜑 is of the form 𝜑 = Û 𝑖 Ü 𝑗 𝑒𝑖,𝑗 ≥ 0 then 𝜃𝜑 … view at source ↗
read the original abstract

This article establishes the completeness of an axiomatization for the robust safety of dynamical systems with polynomial differential equations on bounded time horizons. Safety properties of robust systems are uniformly reduced to a sound axiomatization of polynomial invariants, resulting in reliable logical proofs of correctness. Approximate decidability results are also established: there is a computable algorithm such that, given any perturbation parameter $\delta$, it either produces a symbolic proof of robust safety (hence correctly decides the dynamical system to be robustly safe), or correctly decides that the system is not robustly safe under a perturbation of level $\delta$. In contrast to earlier works, this article crucially leverages results from subanalytic geometry to retain a level of exactness, thereby establishing positive results of provability/decidability allowing for arbitrary bounded (semialgebraic) initial/post conditions even without positive separation at their (topological) boundaries. This enables the generation of proofs of inductive safety beyond finite time horizons for general hybrid dynamical systems.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper claims to establish completeness of an axiomatization for robust safety of dynamical systems governed by polynomial differential equations on bounded time horizons. Robust safety properties are reduced to a sound axiomatization of polynomial invariants via results from subanalytic geometry; this reduction is asserted to hold for arbitrary bounded semialgebraic initial and post conditions even without positive separation at topological boundaries. Approximate decidability is also claimed: a computable procedure either produces a symbolic proof of robust safety or correctly identifies that the system fails to be robustly safe at a given perturbation level δ.

Significance. If the central reduction holds, the result would constitute a notable advance in the logical verification of hybrid systems by removing the positive-separation restriction present in prior work and by supplying both completeness and approximate decidability for general semialgebraic sets.

major comments (1)
  1. [reduction argument (main completeness theorem)] The reduction step that maps robust safety of polynomial flows to the polynomial-invariant axiomatization for arbitrary bounded semialgebraic sets (without positive boundary separation) is load-bearing for the completeness claim. The manuscript must explicitly verify that the image of the flow under a polynomial vector field, together with the δ-perturbation neighborhoods, remains inside the subanalytic category to which the invoked o-minimality or curve-selection results apply; otherwise the reduction fails for the general case stated in the abstract.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for identifying the need for explicit verification in the central reduction argument. We address the major comment below.

read point-by-point responses

  1. Referee: [reduction argument (main completeness theorem)] The reduction step that maps robust safety of polynomial flows to the polynomial-invariant axiomatization for arbitrary bounded semialgebraic sets (without positive boundary separation) is load-bearing for the completeness claim. The manuscript must explicitly verify that the image of the flow under a polynomial vector field, together with the δ-perturbation neighborhoods, remains inside the subanalytic category to which the invoked o-minimality or curve-selection results apply; otherwise the reduction fails for the general case stated in the abstract.

    Authors: We agree that an explicit verification of subanalyticity preservation is required for rigor. Polynomial flows on bounded intervals are subanalytic (their graphs are subanalytic sets by the o-minimality of the subanalytic structure and the fact that solutions to polynomial ODEs admit subanalytic parametrizations). δ-perturbation neighborhoods of bounded semialgebraic sets are themselves semialgebraic, hence subanalytic. In the revised version we will add a short lemma (immediately before the statement of the main completeness theorem) that invokes the relevant closure properties from subanalytic geometry (e.g., van den Dries, “Tame topology and o-minimal structures”, Thm. 3.2.5 and Cor. 3.3.8) to confirm that both the flow image and the perturbed sets remain inside the subanalytic category, thereby licensing the curve-selection and o-minimality results used in the reduction. revision: yes

Circularity Check

0 steps flagged

Minor self-citation to prior dL axiomatization; central completeness relies on external subanalytic geometry benchmarks

full rationale

The derivation reduces robust safety properties of polynomial DEs to the existing sound axiomatization of polynomial invariants, then invokes subanalytic geometry results (o-minimality/curve selection) to handle arbitrary bounded semialgebraic sets without positive boundary separation. These geometry results are external mathematical facts, not derived within the paper or from author self-citations. Self-citations to the authors' prior differential dynamic logic work support the base invariant axiomatization but are not load-bearing for the new completeness claim on robust safety. No self-definitional reductions, fitted inputs renamed as predictions, or ansatzes smuggled via citation are present. The result is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the soundness of the base polynomial invariant axiomatization and the applicability of subanalytic geometry theorems to semialgebraic sets in the dynamical systems context; no free parameters or invented entities are indicated in the abstract.

axioms (2)
  • standard math Sound axiomatization of polynomial invariants
    Invoked as the target of the uniform reduction for safety properties.
  • domain assumption Results from subanalytic geometry for exact handling of semialgebraic sets without boundary separation
    Used to establish positive provability and decidability results for arbitrary bounded initial/post conditions.

pith-pipeline@v0.9.1-grok · 5693 in / 1353 out tokens · 21680 ms · 2026-06-26T19:19:36.352560+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

34 extracted references · 25 canonical work pages · 1 internal anchor

  1. [1]

    Noah Abou El Wafa and André Platzer. 2026. Complete Robust Hybrid Systems. InIJCAR (LNCS), Armin Biere, Carsten Lutz, and Sara Negri (Eds.). Springer. , Vol. 1, No. 1, Article . Publication date: June 20yy. Differential Equation Inductive Robustness Axiomatization 29

    2026

  2. [2]

    2015.Principles of Cyber-Physical Systems

    Rajeev Alur. 2015.Principles of Cyber-Physical Systems. The MIT Press

    2015

  3. [3]

    Bell, Jean-Charles Delvenne, Raphaël M

    Paul C. Bell, Jean-Charles Delvenne, Raphaël M. Jungers, and Vincent D. Blondel. 2010. The continuous Skolem-Pisot problem.Theor. Comput. Sci.411, 40-42 (2010), 3625–3634. https://doi.org/10.1016/J.TCS.2010.06.005

    work page doi:10.1016/j.tcs.2010.06.005 2010

  4. [4]

    Edward Bierstone and Pierre D. Milman. 1988. Semianalytic and subanalytic sets.Inst. Hautes Études Sci. Publ. Math. 67 (1988), 5–42. http://www.numdam.org/item?id=PMIHES_1988__67__5_0

    1988

  5. [5]

    Manon Blanc and Olivier Bournez. 2024. Quantifiying the Robustness of Dynamical Systems. Relating Time and Space to Length and Precision. In32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, February 19-23, 2024, Naples, Italy (LIPIcs, Vol. 288), Aniello Murano and Alexandra Silva (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1...

    work page doi:10.4230/lipics.csl.2024.17 2024

  6. [6]

    2013.Real Algebraic Geometry

    Jacek Bochnak, Michel Coste, and Marie-Francoise Roy. 2013.Real Algebraic Geometry. Springer Science & Business Media

    2013

  7. [7]

    Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013. Flow*: An Analyzer for Non-linear Hybrid Systems. InComputer Aided Verification - 25th International Conference, CA V 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (LNCS, Vol. 8044), Natasha Sharygina and Helmut Veith (Eds.). Springer, 258–263. https://doi.org/10.1007/ 978-3-642-3...

    2013

  8. [8]

    Katherine Cordwell and André Platzer. 2019. Towards Physical Hybrid Systems. InAutomated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11716), Pascal Fontaine (Ed.). Springer, 216–232. https://doi.org/10.1007/978-3-030-29436-6_13

    work page doi:10.1007/978-3-030-29436-6_13 2019

  9. [9]

    2008.Ensembles sous-analytiques à la polonaise: avec une introduction aux fonctions

    Sophia Denkowska, Jacek Stasica, and Maciej P Denkowski. 2008.Ensembles sous-analytiques à la polonaise: avec une introduction aux fonctions. Editions Hermann

    2008

  10. [10]

    Peter Franek, Stefan Ratschan, and Piotr Zgliczynski. 2016. Quasi-decidability of a Fragment of the First-Order Theory of Real Numbers.Journal of Automated Reasoning57, 2 (Aug. 2016), 157–185. https://doi.org/10.1007/s10817-015-9351-3

    work page doi:10.1007/s10817-015-9351-3 2016

  11. [11]

    Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable Verification of Hybrid Systems. InComputer Aided Verification - 23rd International Conference, CA V 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (LNCS, Vol. 6806), Ganes...

    work page doi:10.1007/978-3-642-22110-1_30 2011

  12. [12]

    Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. 2015. KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. InAutomated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings (LNCS, Vol. 9195), Amy P. Felty and Aart Middeldorp (Eds.). Springe...

    work page doi:10.1007/978-3-319-21401-6_36 2015

  13. [13]

    Sicun Gao, Jeremy Avigad, and Edmund M. Clarke. 2012. Delta-Decidability over the Reals. In2012 27th Annual IEEE Symposium on Logic in Computer Science. 305–314. https://doi.org/10.1109/LICS.2012.41

    work page doi:10.1109/lics.2012.41 2012

  14. [14]

    Sicun Gao, Soonho Kong, Wei Chen, and Edmund Clarke. 2014. Delta-Complete Analysis for Bounded Reachability of Hybrid Systems. arXiv:1404.7171 (Apr 2014). http://arxiv.org/abs/1404.7171 arXiv:1404.7171 [cs]

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  15. [15]

    Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. dReal: An SMT Solver for Nonlinear Theories over the Reals. InAutomated Deduction – CADE-24, Maria Paola Bonacina (Ed.). Springer, Berlin, Heidelberg, 208–214. https: //doi.org/10.1007/978-3-642-38574-2_14

    work page doi:10.1007/978-3-642-38574-2_14 2013

  16. [16]

    Graça, N

    D.S. Graça, N. Zhong, and J. Buescu. 2009. Computability, noncomputability and undecidability of maximal intervals of IVPs.Trans. Amer. Math. Soc.361, 6 (Jan 2009), 2913–2927. https://doi.org/10.1090/S0002-9947-09-04929-0

    work page doi:10.1090/s0002-9947-09-04929-0 2009

  17. [17]

    T. H. Grönwall. 1919. Note on the Derivatives with Respect to a Parameter of the Solutions of a System of Differential Equations.Annals of Mathematics20, 4 (1919), 292–296. https://doi.org/10.2307/1967124

    work page doi:10.2307/1967124 1919

  18. [18]

    2002.Ordinary Differential Equations

    Philip Hartman. 2002.Ordinary Differential Equations. Society for Industrial and Applied Mathematics. https: //doi.org/10.1137/1.9780898719222

    work page doi:10.1137/1.9780898719222 2002

  19. [19]

    Hubbard and Barbara Burke Hubbard

    John H. Hubbard and Barbara Burke Hubbard. 2015.Vector Calculus, Linear Algebra, and Differential Forms: A Unified Approach (5th edition). Matrix Editions. 818 pages pages. https://hal.science/hal-01297648

    2015

  20. [20]

    Michał Kosiba. 2025. The generalized Łojasiewicz inequality for definable and subanalytic multifunctions.J. Math. Anal. Appl.543, 2, Part 1 (2025), 128977. https://doi.org/10.1016/j.jmaa.2024.128977

    work page doi:10.1016/j.jmaa.2024.128977 2025

  21. [21]

    Jiang Liu, Naijun Zhan, and Hengjun Zhao. 2011. Computing semi-algebraic invariants for polynomial dynamical systems. InProceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, October 9-14, 2011, Samarjit Chakraborty, Ahmed Jerraya, Sanjoy K. Baruah, and Se...

    work page doi:10.1145/2038642.2038659 2011

  22. [22]

    Anil Nerode and Wolf Kohn. 1992. Models for Hybrid Systems: Automata, Topologies, Controllability, Observability. InHybrid Systems. Berlin, 317–356. https://doi.org/10.1007/3-540-57318-6_35

    work page doi:10.1007/3-540-57318-6_35 1992

  23. [23]

    André Platzer. 2008. Differential Dynamic Logic for Hybrid Systems.J. Autom. Reason.41, 2 (2008), 143–189. https://doi.org/10.1007/S10817-008-9103-8

    work page doi:10.1007/s10817-008-9103-8 2008

  24. [24]

    André Platzer. 2012. The Complete Proof Theory of Hybrid Systems. InProceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. IEEE Computer Society, 541–550. , Vol. 1, No. 1, Article . Publication date: June 20yy. 30 André Platzer and Long Qian https://doi.org/10.1109/LICS.2012.64

    work page doi:10.1109/lics.2012.64 2012

  25. [25]

    André Platzer. 2012. Logics of Dynamical Systems. InProceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. IEEE Computer Society, 13–24. https://doi.org/10. 1109/LICS.2012.13

    2012

  26. [26]

    André Platzer. 2017. A Complete Uniform Substitution Calculus for Differential Dynamic Logic.J. Autom. Reason.59, 2 (2017), 219–265. https://doi.org/10.1007/S10817-016-9385-1

    work page doi:10.1007/s10817-016-9385-1 2017

  27. [27]

    2018.Logical Foundations of Cyber-Physical Systems

    André Platzer. 2018.Logical Foundations of Cyber-Physical Systems. Springer. https://doi.org/10.1007/978-3-319-63588-0

    work page doi:10.1007/978-3-319-63588-0 2018

  28. [28]

    André Platzer and Long Qian. 2025. Axiomatization of Compact Initial Value Problems: Open Properties.J. ACM72, 6, Article 41 (2025), 51 pages. https://doi.org/10.1145/3763228

    work page doi:10.1145/3763228 2025

  29. [29]

    André Platzer and Yong Kiam Tan. 2020. Differential Equation Invariance Axiomatization.J. ACM67, 1 (2020), 6:1–6:66. https://doi.org/10.1145/3380825

    work page doi:10.1145/3380825 2020

  30. [30]

    Stefan Ratschan. 2002. Quantified Constraints Under Perturbation.J. Symb. Comput.33, 4 (2002), 493–505. https: //doi.org/10.1006/JSCO.2001.0519

    work page doi:10.1006/jsco.2001.0519 2002

  31. [31]

    Stefan Ratschan. 2018. Converse Theorems for Safety and Barrier Certificates.IEEE Trans. Autom. Control.63, 8 (2018), 2628–2632. https://doi.org/10.1109/TAC.2018.2792325

    work page doi:10.1109/tac.2018.2792325 2018

  32. [32]

    Yong Kiam Tan and André Platzer. 2021. An axiomatic approach to existence and liveness for differential equations. Formal Aspects Comput.33, 4-5 (2021), 461–518. https://doi.org/10.1007/S00165-020-00525-0

    work page doi:10.1007/s00165-020-00525-0 2021

  33. [33]

    1948.A Decision Method for Elementary Algebra and Geometry

    Alfred Tarski. 1948.A Decision Method for Elementary Algebra and Geometry. The Rand Corporation, Santa Monica, Calif

    1948

  34. [34]

    In: European Conference on Com- puter Vision

    Klaus Weihrauch. 2000.Computable Analysis: An Introduction. Springer, Heidelberg. https://doi.org/10.1007/978-3- 642-56999-9 , Vol. 1, No. 1, Article . Publication date: June 20yy. Differential Equation Inductive Robustness Axiomatization 31 Appendix A dL Axiomatization The following sound axioms ofdLare used in this article. Theorem A.1 ([25, 29, 32]).Th...

    work page doi:10.1007/978-3- 2000