Tuesday, May 24, 2022 - 9:00am to 11:00am
Location:In Person and Virtual - ET Traffic21 Classroom, Gates Hillman 6501 and Zoom
Speaker:YONG KIAM TAN, Ph.D. StudentComputer Science DepartmentCarnegie Mellon University https://www.cs.cmu.edu/~yongkiat/
Deductive Verification for Ordinary Differential Equations: Safety, Liveness, and Stability
This thesis studies deductive verification for ordinary differential equations (ODEs) with a focus on proofs of their safety, liveness, and stability properties. These proofs are compositionally extended to obtain proofs of stability for hybrid (switched) systems. The combination of safety, liveness, and stability is crucial for comprehensive correctness of real-world systems: safety of a system model ensures that it always stays within a prescribed set of safe states throughout its operation, liveness ensures that the modeled system will eventually achieve its specified goal, and stability ensures that conclusions drawn about idealized ODE or hybrid system models are robust to real-world perturbations. 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, yielding identification, buildup, and generalization of the deductive building blocks underlying proof methods for the properties studied in each chapter. 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) In Person and Zoom Participation. See announcement.