Logic for Distributed Hybrid Systems

Overview

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:

1. Cars move continuously on the street (continuous dynamics)
2. Their behavior is subject to discrete control from various digital controllers and control decisions (discrete dynamics).
3. 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 [5].

This verification technology for differential dynamic logic has been implemented in the KeYmaeraD distributed 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

1. 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, pages 42-56. Springer, 2011. © Springer-Verlag
   [bib | pdf | doi | study | TR]
   
   
2. 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 | study | FM'11]
   
   
3. 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, Pages 63-72. ACM, 2011. © ACM
   [bib | pdf | doi]
   
   
4. André Platzer.
   A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
   Submitted, December 2010.
   [pdf]
   
   
5. 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. © Springer-Verlag
   [bib | pdf | doi | TR]