Linear Axiomatization of Linear Differential Equations
Abstract
This article presents an axiomatization of linear differential equations that is complete for topologically open properties with compact initial conditions and time horizons by proving them deductively via a sound reduction to formulas of linear real arithmetic. Indeed, linearity is preserved: linear differential invariants are complete for open properties of linear differential equations and reduce with a linear number of Lie derivatives (per atom) to linear real arithmetic. In particular, this article shows that the linear fragment of differential dynamic logic (dL), a modal extension of standard first-order logic over the reals satisfies these completeness properties. By establishing completeness within decidable linear real arithmetic, the need for proving sophisticated nonlinear formulas of real arithmetic is circumvented. Furthermore, this article establishes generalizations to the nonlinear fragment of dL that enable the practical certification of reachability computations, validating the output of external computations in dL with machine-checkable proofs.
Related
- High-order fractional linear differential equations do not describe stochastic processes with finite state space
- On exponential stability of generalized linear functional differential equations
- Rational linear forms of linearizable ordinary differential equations
- Boundary value problems for linear differential-algebraic equations: solvability via the Kronecker canonical form
- Initial-boundary value problems for linear lattice differential equations
BibTeX
@misc{qian2026linear,
title = {{Linear Axiomatization of Linear Differential Equations}},
author = {Long Qian and André Platzer},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.28460},
eprint = {2610.28460},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.28460},
}
RIS
TY - UNPB
TI - Linear Axiomatization of Linear Differential Equations
AU - Long Qian
AU - André Platzer
PY - 2026
DA - 2026/10/20
PB - arXiv
DO - 10.48550/arxiv.2610.28460
UR - https://arxiv.org/abs/2610.28460
AB - This article presents an axiomatization of linear differential equations that is complete for topologically open properties with compact initial conditions and time horizons by proving them deductively via a sound reduction to formulas of linear real arithmetic. Indeed, linearity is preserved: linear differential invariants are complete for open properties of linear differential equations and reduce with a linear number of Lie derivatives (per atom) to linear real arithmetic. In particular, this article shows that the linear fragment of differential dynamic logic (dL), a modal extension of standard first-order logic over the reals satisfies these completeness properties. By establishing completeness within decidable linear real arithmetic, the need for proving sophisticated nonlinear formulas of real arithmetic is circumvented. Furthermore, this article establishes generalizations to the nonlinear fragment of dL that enable the practical certification of reachability computations, validating the output of external computations in dL with machine-checkable proofs.
ER -