Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

Brieger, Marvin ; Mitsch, Stefan und Platzer, André (2023): Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs. 29th International Conference on Automated Deduction (CADE), Rome, Italy, 01. - 04. Juli 2023. In: Automated Deduction – CADE 29, Lecture Notes in Computer Science Bd. 14132 Cham: Springer. S. 96-115

Abstract

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

• Dokumententyp: Konferenzbeitrag (Paper)
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISBN: 978-3-031-38499-8 ; 978-3-031-38498-1
• ISSN: 0302-9743
• Ort: Cham
• Sprache: Englisch