Differential Dynamic Logic for Hybrid Systems

>> >>

Table of Contents
Overview Syntax More Information Abstract Selected Publications

Overview

Download
or
Launch
KeYmaera

The differential dynamic logic (dL) is a a logic for specifying and verifying hybrid systems. The logic dL can be used to specify correctness properties for hybrid systems given operationally as hybrid programs. 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. 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

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 favourite programming language.

Syntax

Note that the syntax of the 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 automata.

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, optionally with domain of maximum evolution or invariant region `F`
	`?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.

More Information

Full extended syntax of differential dynamic logic dL, including additionally definable operations
KeYmaera theorem prover for hybrid systems, which supports dL

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

[Pla08]: André Platzer. Differential Dynamic Logic for Hybrid Systems. Journal of Automated Reasoning, 2008. Accepted for publication.
[bib | pdf]
[PC08]: 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]
[Pla07d]: 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]
[Pla07c]: 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 | slides]
[Pla07b]: 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 | slides]
[Pla07a]: 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-Verlag, 2007. (c) Springer Verlag
[bib | pdf]
[Pla06]: André Platzer. Towards a hybrid dynamic logic for hybrid dynamic systems. In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva, and Jørgen Villadsen, editors, Proc., LICS International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, Electr. Notes Theor. Comput. Sci. 174(6):63-77, 2007.
[bib | pdf]

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.