Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

Autor:	Brieger, Marvin, Mitsch, Stefan, Platzer, André
Rok vydání:	2023
Předmět:	Computer Science - Logic in Computer Science F.3.1 F.4.1 D.2.4 C.1.m C.2.4 D.4.7
Zdroj:	International Conference on Automated Deduction, CADE-29 2023
Druh dokumentu:	Working Paper
DOI:	10.1007/978-3-031-38499-8_6
Popis:	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. Comment: CADE 2023
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2303.17333 Zobrazit plný text záznamu View this record from Arxiv