Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

This paper introduces a uniform substitution calculus for dL(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 dL(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 dL(CHP) paves the way for a parsimonious implementation of theorem provers for hybrid systems with communication and parallelism.