Computer Science Department
School of Computer Science, Carnegie Mellon University


dLι: Definite Descriptions inDifferential Dynamic Logiic

Brandon Bohrer, Manuel Fernández, Andrá Platzer

November 2019

A version of this work appears in the
27th International Conference on Automated Deduction (CADE) 2019


Keywords: Dynamic logic, definite description, hybrid systems, theorem proving, uniform substitution, partial functions

We introduce dLι, which extends differential dynamic logic (dL) for hybrid systems with definite descriptions and tuples, thus enabling its theoretical foundations to catch up with its implementation in the theorem prover KeYmaera X. Definite descriptions enable partial, nondifferentiable, and discontinuous terms, which have many examples in applications, such as divisions, nth roots, and absolute values. Tuples enable systems of multiple differential equations, arising in almost every application. Together, definite description and tuples combine to support long-desired features such as vector arithmetic. We overcome the unique challenges posed by extending dL with these features. Unlike in vanilla dL, definite descriptions enable non-locally-Lipschitz terms, so our differential equation (ODE) axioms now make their continuity requirements explicit. Tuples are simple when considered in isolation, but in the context of hybrid systems they demand that differentials are treated in full generality. The addition of definite descriptions also makes dLι a free logic; we investigate the interaction of free logic and the ODEs of dL, showing that this combination is sound, and characterize its expressiveness. We give an example system that can be defined and verified using these extensions.

74 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by