Linear logic method proves safety in differential equations
Linear Axiomatization of Linear Differential Equations
Logic in Computer Science
Summary
Proving that certain behaviors happen or don’t happen in systems described by differential equations can be very hard, especially when using complicated math. The authors found a way to simplify these proofs for linear differential equations by turning them into problems that only involve simple arithmetic. Their method works well for systems that start in a limited range and are observed over a set time, avoiding tricky nonlinear math. They also extended their approach to help check more complex systems by verifying computer-generated results with easy-to-check logical steps.
What this means in practice
- •For control system engineers: Verify safety properties of linear system models efficiently using a logic-based arithmetic approach.
- •For software verification teams: Certify results from external reachability tools with machine-checkable proofs using the extended logic framework.
A theory result. No direct application yet.
Authors
Long Qian, André Platzer
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.