# Relational Differential Dynamic Logic

## TL;DR

This paper extends differential dynamic logic (dL) with relational capabilities to compare different system states over time, enabling formal proofs of properties like the impact of early emergency brake deployment.

## Contribution

It introduces a theory of simulations and time stretching for relational dL, providing new inference rules and practical techniques for hybrid system verification.

## Key findings

- Developed a relational extension of dL with simulation and time stretching
- Derived new inference rules for relational properties in dL
- Validated methods on automotive case studies

## 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.