We introduce differential refinement logic (dRL), a logic with firstclass support for refinement relations on hybrid systems, and a proof calculus for verifying such relations. dRL simultaneously solves several seemingly different challenges common in theorem proving for hybrid systems: 1. When hybrid systems are complicated, it is useful to prove properties about simpler and related subsystems before tackling the system as a whole. 2. Some models of hybrid systems can be implementation-specific. Verification can be aided by abstracting the system down to the core components necessary for safety, but only if the relations between the abstraction and the original system can be guaranteed. 3. One approach to taming the complexities of hybrid systems is to start with a simplified version of the system and iteratively expand it. However, this approach can be costly, since every iteration has to be proved safe from scratch, unless refinement relations can be leveraged in the proof. 4. When proofs become large, it is difficult to maintain a modular or comprehensible proof structure. By using a refinement relation to arrange proofs hierarchically according to the structure of natural subsystems, we can increase the readability and modularity of the resulting proof. dRL extends an existing specification and verification language for hybrid systems (differential dynamic logic, dL) by adding a refinement relation to directly compare hybrid systems. This paper gives a syntax, semantics, and proof calculus for dRL. We demonstrate its usefulness with examples where using refinement results in easier and better-structured proofs.

pages

Return to: SCS Technical Report Collection
School of Computer Science