| ||||
| ||||
![]() Title:Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs Conference:CADE-29 Tags:Assumption-commitment reasoning, CSP, Differential dynamic logic, Parallel programs and Uniform substitution Abstract: 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. Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs ![]() Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs | ||||
Copyright © 2002 – 2025 EasyChair |