Logic for Distributed Hybrid Systems

Overview

Quantified differential dynamic logic (QdL) [2,3] is a logic for specifying and verifying distributed hybrid systems.

Many safety-critical computers are embedded in cyber-physical systems like cars or aircraft. Safety-critical systems in automotive, aviation, railway, and power grids combine communication, computation, and control. Combining computation and control leads to hybrid systems, whose behavior involves both discrete and continuous dynamics originating, e.g., from discrete control decisions and differential equations of movement. Combining communication and computation leads to distributed systems, whose dynamics are discrete transitions of system parts that communicate with each other. Several of these systems form dynamic distributed systems, where the structure of the system is not fixed but evolves over time and agents may appear or disappear during the system evolution.

Combinations of all three aspects (communication, computation, and control) are used in sophisticated applications, e.g., cooperative distributed car control. These systems are (dynamic) distributed hybrid systems. They cannot be considered just as a distributed system (because, e.g., the continuous evolution of positions and velocities matters for collision freedom in car control) nor just as a hybrid system (because the evolving system structure and appearance of new agents can make an otherwise collision-free system unsafe).

Distributed car control applications are good examples for distributed hybrid systems, because:

Cars move continuously on the street (continuous dynamics)
Their behavior is subject to discrete control from various digital controllers and control decisions (discrete dynamics).
The structure of the system may change over time, because participants may appear and disappear, e.g., new cars may appear on the road or leave it.

In this work, we present the first formal verification approach for (dynamic/reconfigurable) distributed hybrid systems [2,3].

This verification technology for quantified differential dynamic logic has been implemented in the KeYmaeraD distributed theorem prover for distributed hybrid systems . Quantified differential dynamic logic has also been implemented in part in the KeYmaera theorem prover.

Note: The proper typesetting of the name QdL for quantified differential dynamic logic is Qdℒ. In LaTeX, I use the following for typesetting Qdℒ:

\text{Q}\textsf{d{\kern-0.1em}$\mathcal{L}$}

Syntax

Note that the syntax of the quantified differential dynamic logic QdL given here uses slightly simplified notationally in comparison to the full syntax in KeYmaera verification tool and the full syntax in KeYmaeraD, which use more escaping of mathematical characters.

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

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

Quantified 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
	`\forall C i . x(i):=t(i)`	Quantified discrete assignment assigning the values of the terms `t(i)` to the `x(i)` for all `i` of type `C`.
	`\forall C i . x(i):=*`	Quantified nondeterministic assignment assigning any value to the `x(i)` for all `i` of type `C`. The values are chosen nondeterministically and independently for each `i`.
	`\forall C i . {x(i)'=t(i), y(i)'=s(i), H(i)}`	Quantified continuous evolution along quantified differential equation system evolving `x(i)` and `y(i)` simultaneously with rates described by terms `t(i),s(i)` for all `i` of type `C`, optionally with evolution domain constraint `H(i)`. This domain constraint `H(i)` needs to be true for all `i` at every time during the evolution, otherwise the system needs to stop following this continuous mode and move on.
	`?H`	State assertion testing whether formula `H` is true in current state (otherwise abort)
where `H` and `H(i)` are formulas of first-order logic including real arithmetic.

Quantified Differential Invariants

Advanced verification technology for quantified differential dynamic logic is based on quantified differential invariants that have been introduced in 2011 [4] as an extension of differential invariants [1] to distributed hybrid systems. Quantified differential invariants are implemented in the KeYmaeraD theorem prover for distributed hybrid systems.

Abstract

We address a fundamental mismatch between the combinations of dynamics that occur in complex physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic networks, where neither structure nor dimension stay the same while the system follows mixed discrete and continuous dynamics.

We provide the logical foundations for closing this analytic gap. We develop a system model for distributed hybrid systems that combines quantified differential equations with quantified assignments and dynamic dimensionality-changes. We introduce a dynamic logic for verifying distributed hybrid systems and present a proof calculus for it. We prove that this calculus is a sound and complete axiomatization of the behavior of distributed hybrid systems relative to quantified differential equations. In our calculus we have proven collision freedom in distributed car control even when new cars may appear dynamically on the road.

Keywords: Dynamic logic, Distributed hybrid systems, Axiomatization, Theorem proving, Quantified differential equations

Selected Publications

The canonical references on this approach are [2,3]. Quantified differential invariants have been introduced in [4]. There is a recent survey in [7]. Also see publications on distributed hybrid systems logic and the publication reading guide.

Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer.
Formal verification of obstacle avoidance and navigation of ground robots.
International Journal of Robotics Research 36(12), pp. 1312-1340, 2017. © The authors
[bib | ⧉ | pdf | doi | kyx | arXiv | abstract]
Yanni Kouskoulas, David W. Renshaw, André Platzer and Peter Kazanzides.
Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pp. 263-272. ACM, 2013. © ACM
[bib | ⧉ | pdf | doi | slides | study | abstract]
Sarah M. Loos, David W. Renshaw and André Platzer.
Formal verification of distributed aircraft controllers.
In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pp. 125-130. ACM, 2013. © ACM
[bib | ⧉ | pdf | doi | slides | poster | study | TR | abstract]
David W. Renshaw, Sarah M. Loos and André Platzer.
Distributed theorem proving for distributed hybrid systems.
In Shengchao Qin and Zongyan Qiu, editors, International Conference on Formal Engineering Methods, ICFEM'11, Durham, UK, Proceedings, volume 6991 of LNCS, pp. 356-371. Springer, 2011. © Springer
[bib | ⧉ | pdf | doi | tool | study | errata | abstract]
André Platzer.
Dynamic logics of dynamical systems.
arXiv:1205.4788, May 2012. Long version of LICS'12 invited tutorial.
[bib | ⧉ | pdf | arXiv | LICS'12 | abstract]
Sarah M. Loos, André Platzer and Ligia Nistor.
Adaptive cruise control:
Hybrid, distributed, and now formally verified.
In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods, FM, Limerick, Ireland, Proceedings, volume 6664 of LNCS, pp. 42-56. Springer, 2011. © Springer
[bib | ⧉ | pdf | doi | slides | study | TR | abstract]
Sarah M. Loos, André Platzer and Ligia Nistor.
Adaptive Cruise Control:
Hybrid, Distributed, and Now Formally Verified.
School of Computer Science, Carnegie Mellon University, CMU-CS-11-107, 2011.
[bib | ⧉ | pdf | FM'10]
André Platzer.
Quantified differential invariants.
In Emilio Frazzoli and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12-14, pp. 63-72. ACM, 2011. © ACM
[bib | ⧉ | pdf | doi | slides | abstract]
André Platzer.
A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
Logical Methods in Computer Science 8(4), pp. 1-44, 2012.
Special issue for selected papers from CSL'10. © The author
[bib | ⧉ | pdf | doi | arXiv | CSL'10 | abstract]
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, pp. 469-483. Springer, 2010. © Springer
[bib | ⧉ | pdf | doi | slides | TR | LMCS'12 | abstract]
André Platzer.
Differential-algebraic dynamic logic for differential-algebraic programs.
Journal of Logic and Computation 20(1), pp. 309-352, 2010.
Special issue for selected papers from TABLEAUX'07. © The author
[bib | ⧉ | pdf | doi | eprint | study | errata | TABLEAUX'07 | abstract]

Supported by the National Science Foundation (NSF)

Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.