Differential Dynamic Logic for Hybrid Systems

Table of Contents
Overview Syntax Verification Details and Extensions Abstract Selected Publications

Download or
Launch
KeYmaera

Overview

The differential dynamic logic (dL) [15][13] is a logic for specifying and verifying hybrid systems [15][13]. The logic dL can be used to specify correctness properties for hybrid systems given operationally as hybrid programs [15][13]. These correctness properties can be verified using the dL verification calculus. The logic dL and its verification calculus are the basis of the deductive verification tool KeYmaera for hybrid systems [8]. In addition, the hybrid systems and correctness properties formulated in dL can even include symbolic parameters, which can be free or quantified to discover the required parametric safety constraints.

The basic idea for dL formulas is to have formulas of the form [α]φ to specify that the hybrid system α always remains within region φ, i.e., all states reachable by following the transitions of hybrid system α statisfy the formula φ. Dually, the dL formula <α>φ expresses that the hybrid system α is able to reach region φ, i.e., there is a state reachable by following the transitions of hybrid system α that statisfies the formula φ. In either case, the hybrid system α is given as a full operational model in terms of a hybrid program. Using other propositional connectives, one can state the following dL formula

φ -> [α]ψ which expresses that, if hybrid program α initially starts in a state satisfying φ, then it always remains in the region characterised by ψ. For instance, the following formula expresses that for the state of a train controller train, the property z≤m always holds true when starting in a state where v²≤2b(m-z) is true: v²≤2b(m-z) -> [train]z≤m

Case Study: European Train Control System

In much the same way as finite automata can be represented as while-programs, or timed automata have a notation as real-time programs, we use a hybrid program notation for hybrid automata. Essentially, hybrid programs are what you get when you add continuous evolutions as a primitive operation to conventional discrete programs or, in fact, your favorite programming language.

Syntax

Note that the syntax of the differential dynamic logic dL given here uses slightly simplified notationally in comparison to the full syntax in KeYmaera verification tool. The notation in KeYmaera uses more escaping of mathematical characters.

Formulas of dL, with typical names `φ` and `ψ`, are defined by the following syntax
φ ::=	`\forall x φ`	Universal quantifier: for all real values of `x`, formula `φ` holds
	`\exists x φ`	Existential quantifier: for some real value of `x`, formula `φ` holds
	`[α] φ`	After all runs of hybrid program `α`, formula `φ` holds (safety)
	`<α> φ`	There is at least one run of hybrid program `α`, after which formula `φ` holds (liveness)
	`!φ`	Negation (not)
	`φ & ψ`	Conjunction (and)
	`φ \| ψ`	Disjunction (or)
	`φ -> ψ`	Implication (implication)
	`φ <-> ψ`	Biimplication (equivalence)
	pred	Real arithmetic predicate expression

The behaviour of the hybrid system α is specified as a hybrid program, which is, essentially, a program notation for hybrid systems.

Hybrid programs, with typical names `α` and `β`, are defined by the following syntax
α ::=	`α; β`	Sequential composition following `β` after `α` has finished
	`α ++ β`	Nondeterministic choice following either `α` or `β`
	`α^*`	Nondeterministic repetition, repeating `α` arbitrarily often including 0 times
	`x:=t`	Discrete assignment/jump assigning the value of `t` to `x`
	`{x'=t,y'=s, F}`	Continuous evolution along differential equation system with terms `t,s`, optionally with domain of maximum evolution or invariant region `F`. Systems of differential equations, differential-algebraic equations, and differential equations with disturbances are possible as well.
	`?F`	State assertion testing whether formula `F` is true in current state (otherwise abort)
where `F` is a formula of (possibly non-linear) real arithmetic.

Verification

Verifying correct functioning of hybrid systems amounts to proving validity of corresponding formulas in differential dynamic logic dL [15][13]. These dL formulas state the desired correctness properties of the hybrid systems under consideration, including safety, liveness, reactivity, and controllability properties. For showing that these systems operate as expected, André Platzer has devised a logical verification calculus [15][13].

Advanced verification technology for differential dynamic logics is further based on differential invariants [15][10][7], which are formulas that remain true along the dynamics of the hybrid system and its differential equations. Differential invariants and differential induction are essentially a generalization of discrete induction to differential equations. This verification technology for differential dynamic logic has been implemented in the KeYmaera theorem prover for hybrid systems [8].

Case studies for using differential dynamic logic to verify complex physical systems include studies for the European Train Control System (ETCS) [4] and verification of collision avoidance in aircraft collision avoidance maneuvers [5].

Details and Extensions

Full extended syntax of differential dynamic logic dL, including additionally definable operations [2]
KeYmaera theorem prover for hybrid systems, which implements the dL calculus
There is an extension called quantified differential dynamic logic (QdL) [1], with which distributed hybrid systems can be verified. This is the first formal verification approach for (dynamic/reconfigurable) distributed hybrid systems, in which participants may appear and disappear during the system evolution.
Publications related to dL
There is an extension called differential-algebraic dynamic logic (DAL) for more general differential-algebraic programs [12]
Advanced verification technology for differential dynamic logic is based on differential invariants [12][10][7], which are formulas that remain true along the dynamics of the hybrid system and its differential equations.
There is a temporal extension called differential temporal dynamic logic (dTL) [16]. Also see further details and extensions in my book [2].

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 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.

Keywords: dynamic logic, differential equations, sequent calculus, axiomatisation, automated theorem proving, verification of hybrid systems

Selected Publications

The canonical references on this approach are [13] and [12]. Also see the publication reading guide.

André Platzer.
Quantified differential dynamic logic for distributed hybrid systems.
In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 19th EACSL Annual Conference, CSL 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of LNCS, pages 469-483. Springer, 2010. (c) Springer Verlag
[bib | pdf | doi]
André Platzer.
Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
Springer, 2010. ISBN 978-3-642-14508-7, To appear.
[bib | book | doi | web]
André Platzer.
Differential dynamic logic: Automated theorem proving for hybrid systems.
Künstliche Intelligenz, 24(1), pages 75-77, 2010.
Invited paper. (c) Springer Verlag
[bib | doi]
André Platzer and Jan-David Quesel.
European Train Control System: A case study in formal verification.
In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pages 246-265. Springer, 2009. (c) Springer Verlag
[bib | pdf | doi | slides | study]
André Platzer and Edmund M. Clarke.
Formal verification of curved flight collision avoidance maneuvers: A case study.
In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pages 547-562. Springer, 2009. (c) Springer Verlag
This paper was awarded the FM Best Paper Award.
[bib | pdf | doi | slides]
André Platzer.
Verification of cyberphysical transportation systems.
IEEE Intelligent Systems, 24(4), pages 10-13, Jul/Aug, 2009. (c) IEEE.
Invited paper.
[bib | doi]
André Platzer and Edmund M. Clarke.
Computing differential invariants of hybrid systems as fixedpoints.
Formal Methods in System Design, 35(1), pages 98-120, 2009. (c) Springer Verlag
[bib | pdf | doi]
André Platzer and Jan-David Quesel.
KeYmaera: A hybrid theorem prover for hybrid systems.
In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pages 171-178. Springer, 2008. (c) Springer Verlag
[bib | pdf | doi | slides]
André Platzer.
Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems.
PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
To appear with Springer as Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
[bib]
André Platzer and Edmund M. Clarke.
Computing differential invariants of hybrid systems as fixedpoints.
In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pages 176-189, Springer, 2008. (c) Springer Verlag
[bib | pdf | doi]
André Platzer and Edmund M. Clarke.
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
School of Computer Science, Carnegie Mellon University, CMU-CS-08-103, Feb, 2008.
[bib | pdf]
André Platzer.
Differential-algebraic dynamic logic for differential-algebraic programs.
Journal of Logic and Computation, 20(1), pages 309-352, 2010. Advance Access published on November 18, 2008 by Oxford University Press.
[bib | pdf | doi]
André Platzer.
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning, 41(2), pages 143-189, 2008. (c) Springer Verlag
[bib | pdf | doi]
André Platzer.
Combining deduction and algebraic constraints for hybrid system analysis.
In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, CEUR Workshop Proceedings, 259:164-178, 2007.
[bib | pdf]
André Platzer.
Differential dynamic logic for verifying parametric hybrid systems.
In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pages 216-232. Springer, 2007. (c) Springer Verlag
This paper was awarded the TABLEAUX Best Paper Award.
[bib | pdf | doi | slides]
André Platzer.
A temporal dynamic logic for verifying hybrid system invariants.
In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pages 457-471. Springer, 2007. (c) Springer Verlag
[bib | pdf | doi | slides]
André Platzer.
Differential logic for reasoning about hybrid systems.
In Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 746-749. Springer, 2007. (c) Springer Verlag
[bib | pdf | doi]

For full details, please see my List of Publications.

There also is a verification tool implementation of dL in a theorem prover, which is called KeYmaera [8].