Overview
Quantified differential dynamic logic (QdL) [2,3] is a logic for specifying and verifying distributed hybrid systems.
Many safetycritical computers are embedded in cyberphysical systems like cars or aircraft. Safetycritical 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 collisionfree 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ℒ:
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 firstorder 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 dimensionalitychanges. 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.
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 813, 2013, pp. 263272. 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 813, 2013, pp. 125130. 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. 356371. Springer, 2011. © SpringerVerlag
[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  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. 4256. Springer, 2011. © SpringerVerlag
[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, CMUCS11107, 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 1214, pp. 6372. 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. 144, 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 2327, 2010. Proceedings, volume 6247 of LNCS, pp. 469483. Springer, 2010. © SpringerVerlag
[bib  ✂  pdf  doi  slides  TR  LMCS'12  abstract]

André Platzer.
Differentialalgebraic dynamic logic for differentialalgebraic programs.
Journal of Logic and Computation 20(1), pp. 309352, 2010.
Special issue for selected papers from TABLEAUX'07. © The author.
[bib  ✂  pdf  doi  eprint  study  errata  TABLEAUX'07  abstract]
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.