References & Citations
Computer Science > Logic in Computer Science
Title: Relational Differential Dynamic Logic
(Submitted on 1 Mar 2019 (v1), last revised 12 Mar 2020 (this version, v2))
Abstract: In the field of quality assurance of hybrid systems (that combine continuous physical dynamics and discrete digital control), Platzer's differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations and sophisticated tool support. Motivated by benchmarks provided by our industry partner, we study a relational extension of dL, aiming to formally prove statements such as "an earlier deployment of the emergency brake decreases the collision speed." A main technical challenge here is to relate two states of two dynamics at different time points. Our main contribution is a theory of suitable simulations (a relational extension of differential invariants that are central proof methods in dL), and a derived technique of time stretching. The latter features particularly high applicability, since the user does not have to synthesize a simulation out of the air. We derive new inference rules for dL from these notions, and demonstrate their use over a couple of automotive case studies.
Submission history
From: Jérémy Dubut [view email][v1] Fri, 1 Mar 2019 04:42:35 GMT (176kb,D)
[v2] Thu, 12 Mar 2020 07:01:31 GMT (282kb,D)
Link back to: arXiv, form interface, contact.