Linear Axiomatization of Linear Differential Equations

Overview & Synopsis

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.