Yong Kiam Tan

Deductive Verification for Ordinary Differential Equations: Safety, Liveness, and Stability Degree Type: Ph.D. in Computer Science
Advisor(s): André Platzer
Graduated: August 2022

Abstract:

Ordinary differential equations (ODEs) are quintessential models of real-world continuous behavior in the physical and engineering sciences. They also feature prominently in hybrid system models that combine discrete and continuous dynamics, and interactions thereof. Formal verification of ODEs and hybrid systems is of increasing practical importance because the real-world systems they model, such as control systems and cyber-physical systems, are often required to operate in safety- and mission-critical settings–obtaining comprehensive and trustworthy verification results for continuous and hybrid systems gives a strong measure of confidence that the real-world systems they model operate correctly.

This thesis studies deductive verification for ordinary differential equations with a focus on proofs of their i) safety, ii) liveness, and iii) stability properties. These proofs are compositionally extended to obtain proofs of iv) stability for hybrid (switched) systems. The combination of safety, liveness, and stability is crucial for comprehensive correctness of real-world systems: i) safety of a system model ensures that it always stays within a prescribed set of safe states throughout its operation, ii) liveness ensures that the modeled system will eventually reach its specified goal or complete its mission, and iii) & iv) stability ensures that the idealized models are robust to real-world perturbations, which is important for control system designs.

The overarching thesis insight is the use of deductive reasoning as a basis for understanding the aforementioned properties and for developing their proofs. Specifically, this thesis uses differential dynamic logic (dL), a logic for deductive verification of hybrid systems, as a trustworthy logical foundation upon which all reasoning principles for safety, liveness, and stability are rigorously derived. The thesis first shows how ODE invariance, a key ingredient in proofs of ODE safety, can be completely axiomatized and reasoned about syntactically in dL. Then, ODE liveness and existence properties are formally proved through refinement-based reasoning in dL, where each refinement step is justified by proving an ODE safety property. Finally, stability properties for ODEs and hybrid systems are specified using dL's ability to nest safety and liveness modalities with first-order quantification. Proofs of those stability specifications build on ODE safety and liveness (sub-)proofs by compositionally adding dL reasoning for the first-order quantifiers and hybrid systems.

Formal dL specifications elucidate the logical relationships between the properties studied in this thesis. Indeed, these relationships are reflected in the thesis structure outlined above because they yield chapter-by-chapter identification, buildup, and generalization of the deductive building blocks underlying proof methods for the respective properties. The deductive approach enables such generalizations while retaining utmost confidence in the correctness of the resulting proofs because every step is soundly and syntactically justified using dL's parsimonious axiomatization. The derived proof principles and insights are put into practice by implementing them in the KeYmaera X theorem prover for hybrid systems based on dL.

Thesis Committee:
André Platzer (Chair)
Jeremy Avigad
Stefan Mitsch
Frank Pfenning
Joël Ouaknine (MPI-SWS, Saarland University)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Keywords:
Deductive verification, differential dynamic logic, ordinary differential equations, switched systems, safety, invariance, liveness, existence, stability