Dynamic Logic of Communicating Hybrid Programs
Abstract
This paper presents a dynamic logic for compositional deductive verification of communicating hybrid programs (CHPs). CHPs go beyond the traditional mixed discrete and continuous dynamics of hybrid systems by adding CSP-style operators for communication and parallelism. A compositional proof calculus is presented that modularly verifies CHPs including their parallel compositions from proofs of their subprograms by assumption-commitment reasoning in dynamic logic. Unlike Hoare-style assumption-commitments, supports intuitive symbolic execution via explicit recorder variables for communication primitives. Since is a conservative extension of differential dynamic logic , it can be used soundly along with the proof calculus and 's complete axiomatization for differential equation invariants.
Cite
@article{arxiv.2302.14546,
title = {Dynamic Logic of Communicating Hybrid Programs},
author = {Marvin Brieger and Stefan Mitsch and André Platzer},
journal= {arXiv preprint arXiv:2302.14546},
year = {2023}
}