A Program Logic to Verify Signal Temporal Logic Specifications of Hybrid Systems: Extended Technical Report

TL;DR

This paper introduces signal temporal dynamic logic (STdL), bridging STL and dL, enabling deductive verification of hybrid systems with temporal properties, supported by semantics, proof calculus, and soundness proofs.

Contribution

It presents STdL, a novel logic that combines STL and dL, allowing for temporal reasoning in hybrid system verification, with formal semantics and proof system.

Findings

STdL extends dL with temporal reasoning capabilities.

The paper proves soundness and relative completeness of STdL.

STdL enables deductive verification of hybrid systems using STL specifications.

Abstract

Signal temporal logic (STL) was introduced for monitoring temporal properties of continuous-time signals for continuous and hybrid systems. Differential dynamic logic (dL) was introduced to reason about the end states of a hybrid program. Over the past decade, STL and its variants have significantly gained in popularity in the industry for monitoring purposes, while dL has gained in popularity for verification of hybrid systems. In this paper, we bridge the gap between the two different logics by introducing signal temporal dynamic logic (STdL) -- a dynamic logic that reasons about a subset of STL specifications over executions of hybrid systems. Our work demonstrates that STL can be used for deductive verification of hybrid systems. STdL significantly augments the expressiveness of dL by allowing reasoning about temporal properties in given time intervals. We provide a semantics and a proof calculus for STdL, along with a proof of soundness and relative completeness.