Technical Report: Property-Directed Verified Monitoring of Signal Temporal Logic

TL;DR

This paper presents an exact and efficient method for monitoring Signal Temporal Logic properties over numerical simulation traces, integrating symbolic flowpipe representations and property-directed refinements to improve verification accuracy and performance.

Contribution

It introduces a novel property-directed refinement technique using masks, enhancing the precision and efficiency of STL monitoring with verified flowpipe representations.

Findings

Enhanced monitoring precision through integration with Flow*'s symbolic flowpipes

Significant performance improvements using property-directed masks

Successful verification of complex continuous system properties

Abstract

Signal Temporal Logic monitoring over numerical simulation traces has emerged as an effective approach to approximate verification of continuous and hybrid systems. In this report we explore an exact verification procedure for STL properties based on monitoring verified traces in the form of Taylor model flowpipes as produced by the Flow* verified integrator. We explore how tight integration with Flow*'s symbolic flowpipe representation can lead to more precise and more efficient monitoring. We then show how the performance of monitoring can be increased substantially by introducing masks, a property-directed refinement of our method which restricts flowpipe monitoring to the time regions relevant to the overall truth of a complex proposition. Finally, we apply our implementation of these methods to verifying properties of a challenging continuous system, evaluating the impact of each aspect of our procedure on monitoring performance.