Differential Dynamic Logic for Hybrid Systems

>> >>

Overview

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 φ. Using other propositional connectives, one can state the following dL formula

φ -> [α]ψ which expresses that, if system α 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 α, the property z≤m always holds true when starting in a state where v²≤2b(m-z) is true: v²≤2b(m-z) -> [α]z≤m

Syntax

Note that the syntax of the logic dL given here uses slightly simplified notationally in comparison to the full syntax of dL 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
	`α ++ β`	Non-deterministic choice following either `α` or `β`
	`α^*`	Non-deterministic 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

We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and first-order definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system.

Keywords: dynamic logic, sequent calculus, verification of parametric hybrid systems, quantifier elimination

Publications

[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,, LNCS, Springer-Verlag, 2008. (c) Springer Verlag
[bib]
[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.