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 reports@cs.cmu.edu