Retrieval-Augmented Mining of Temporal Logic Specifications from Data

TL;DR

This paper introduces a novel data-driven framework combining Bayesian Optimization and Information Retrieval to learn Signal Temporal Logic specifications from observed behaviors, aiding in requirement mining and anomaly detection in cyber-physical systems.

Contribution

It presents a new method that jointly learns STL structure and parameters using a dense vector database, without STL grammar restrictions, enhancing requirement mining capabilities.

Findings

Effective in classifying system behaviors and detecting anomalies.

Extracts interpretable STL requirements from time series data.

Advances state-of-the-art in CPS requirement mining.

Abstract

The integration of cyber-physical systems (CPS) into everyday life raises the critical necessity of ensuring their safety and reliability. An important step in this direction is requirement mining, i.e. inferring formally specified system properties from observed behaviors, in order to discover knowledge about the system. Signal Temporal Logic (STL) offers a concise yet expressive language for specifying requirements, particularly suited for CPS, where behaviors are typically represented as time series data. This work addresses the task of learning STL requirements from observed behaviors in a data-driven manner, focusing on binary classification, i.e. on inferring properties of the system which are able to discriminate between regular and anomalous behaviour, and that can be used both as classifiers and as monitors of the compliance of the CPS to desirable specifications. We present a novel framework that combines Bayesian Optimization (BO) and Information Retrieval (IR) techniques to simultaneously learn both the structure and the parameters of STL formulae, without restrictions on the STL grammar. Specifically, we propose a framework that leverages a dense vector database containing semantic-preserving continuous representations of millions of formulae, queried for facilitating the mining of requirements inside a BO loop. We demonstrate the effectiveness of our approach in several signal classification applications, showing its ability to extract interpretable insights from system executions and advance the state-of-the-art in requirement mining for CPS.