Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

TL;DR

This paper develops a uniform substitution calculus for the dynamic logic of communicating hybrid programs, simplifying prover implementation and managing complex communication and parallelism reasoning.

Contribution

It introduces a uniform substitution calculus for $ extsf{dL}_ ext{CHP}$, reducing reliance on axiom schemata and isolating soundness-critical instantiation checks.

Findings

Simplifies implementation of hybrid systems provers.

Manages communication and parallelism reasoning with limited overhead.

Enables parsimonious prover kernels using axioms instead of schemata.

Abstract

This paper introduces a uniform substitution calculus for $\mathsf{dL}_\text{CHP}$, the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious prover kernels by using axioms instead of axiom schemata. Instantiations can be recovered from a single proof rule responsible for soundness-critical instantiation checks rather than being spread across axiom schemata in side conditions. Even though communication and parallelism reasoning are notorious for necessitating subtle soundness-critical side conditions, uniform substitution when generalized to $\mathsf{dL}_\text{CHP}$ manages to limit and isolate their conceptual overhead. Since uniform substitution has proven to simplify the implementation of hybrid systems provers substantially, uniform substitution for $\mathsf{dL}_\text{CHP}$ paves the way for a parsimonious implementation of theorem provers for hybrid systems with communication and parallelism.