Complete Dynamic Logic of Communicating Hybrid Programs

TL;DR

This paper introduces a complete proof calculus for the dynamic logic of communicating hybrid programs, enabling rigorous reasoning about complex hybrid systems with parallel interactions and communication.

Contribution

It develops a novel proof calculus for communicating hybrid programs that combines differential dynamic logic with assumption-commitment reasoning, ensuring completeness and expressiveness.

Findings

The calculus is complete relative to the first-order logic of differential equations with communication traces.

It enables succinct and correct reasoning about parallel hybrid systems.

The proof calculus aligns fully with existing hybrid system logics, maintaining reasoning complexity.

Abstract

This article presents a relatively complete proof calculus for the dynamic logic of communicating hybrid programs dLCHP. Beyond hybrid systems, communicating hybrid programs not only feature mixed discrete and continuous dynamics but also their parallel interactions in parallel hybrid systems. This not only combines the subtleties of hybrid and discrete parallel systems, but parallel hybrid dynamics necessitates that all parallel subsystems synchronize in time and evolve truly simultaneously. To enable compositional reasoning nevertheless, dLCHP combines differential dynamic logic dL with mutual abstraction of subsystems by assumption-commitment (ac) reasoning. The resulting proof calculus preserves the essence of dynamic logic axiomatizations, while revealing-and being driven by-a new modal logic view onto ac-reasoning. The dLCHP proof calculus is shown to be complete relative to $\Omega$-FOD, the first-order logic of differential equation properties FOD augmented with communication traces. This confirms that the calculus covers all aspects of parallel hybrid systems, because it lacks no axioms to reduce all their dynamical effects to the assertion logic. Additional axioms for encoding communication traces enable a provably correct equitranslation between $\Omega$-FOD and FOD, which reveals the possibility of representational succinctness in parallel hybrid systems proofs. Transitively, this establishes a full proof-theoretical alignment of dLCHP and dL, and shows that reasoning about parallel hybrid systems is exactly as hard as reasoning about hybrid systems, continuous systems, or discrete systems.