Differential Dynamic Logic for Hybrid Systems

By André Platzer. Journal of automated reasoning, 2008

449 citations recorded by the source corpus.

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 a dynamic logic for hybrid programs, which is a program notation for hybrid systems. 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 programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/5ceefe2ee075bdc4d48f81fef091e1ac6bf9af94

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Formal verification of hybrid systems (2011, methodology): “The tool KeYmaera offers support to prove correctness of hybrid systems using deductive verification [43,44].”
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System (2015, methodology): “We model our system using Differential Dynamic Logic dL [17,18,19], a logic for reasoning about hybrid programs.”
Towards Formal Verification of Freeway Traffic Control (2012, methodology): “b) Verification: We verify the safety of the speed limit choice as modeled above using the formal proof calculus for differential dynamic logic [25], [26].”
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) (2008, methodology): “As the central concept, our tool implements an axiomatization of the transition behavior of hybrid systems in the form of the sequent calculus for the differential dynamic logic dL [12, 13].”