Automated Theorem Proving for Hybrid Systems
Abstract
Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce differential dynamic logic as a new logic with which correctness properties of hybrid systems with parameterized system dynamics can be specified and verified naturally. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid systems successively to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. Systematically, we develop automated theorem proving techniques for our calculus and present proof procedures to tackle the complexities of integrating decision procedures for real arithmetic. For our logic, we further complement discrete induction with differential induction as a new continuous generalization of induction, with which hybrid systems can be verified by exploiting their differential constraints algebraically without having to solve them. Finally, we develop a fixedpoint algorithm for computing the differential invariants required for differential induction, and we introduce a differential saturation procedure that refines the system dynamics successively with differential invariants until correctness becomes provable. As a systematic combination of logic-based techniques, we obtain a sound verification procedure that is particularly suitable for parametric hybrid systems. We demonstrate our approach by verifying safety, controllability, liveness, and collision avoidance properties in case studies ranging from train control applications in the European Train Control System to air traffic control, where we prove collision avoidance in aircraft roundabout maneuvers. |
ACM Award |
Keywords: dynamic logic, differential equations, logic for hybrid systems, free variable calculus, sequent calculus, axiomatisation, automated theorem proving, real arithmetic, verification of hybrid systems, differential induction, fixedpoint engines, train control, air traffic control
Contents
The Ph.D. thesis can be found as an eprint at the University of Oldenburg. An extended version of my Ph.D. thesis [1] has appeared as a book with Springer [2]. |
Thesis
and Book |
-
André Platzer.
Logical Analysis of Hybrid Systems:
Proving Theorems for Complex Dynamics.
Springer, Heidelberg, 2010. 426 pages. ISBN 978-3-642-14508-7.
[bib | ⧉ | doi | book | web | errata | abstract]
-
André Platzer.
Differential Dynamic Logics:
Automated Theorem Proving for Hybrid Systems.
PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
ACM Doctoral Dissertation Honorable Mention Award in 2009.
Extended version appeared as book Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 2010.
[bib | ⧉ | pdf | eprint | slides | book | ebook | abstract]
@PHDTHESIS{Platzer08, author = {Andr{\'e} Platzer}, title = {Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems}, school = {Department of Computing Science, University of Oldenburg}, year = {2008}, pages = {299}, url = {http://oops.uni-oldenburg.de/id/eprint/1403}, }