Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Retrieval-Augmented Mining of Temporal Logic Specifications from Data

Gaia Saveri, Luca Bortolussi

TL;DR

This work presents a novel framework that combines Bayesian Optimization and Information Retrieval techniques to simultaneously learn both the structure and the parameters of STL formulae, without restrictions on the STL grammar, and demonstrates the effectiveness of the approach in several signal classification applications.

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.

Retrieval-Augmented Mining of Temporal Logic Specifications from Data

TL;DR

This work presents a novel framework that combines Bayesian Optimization and Information Retrieval techniques to simultaneously learn both the structure and the parameters of STL formulae, without restrictions on the STL grammar, and demonstrates the effectiveness of the approach in several signal classification applications.

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.
Paper Structure (28 sections, 6 equations, 3 figures, 2 tables, 3 algorithms)

This paper contains 28 sections, 6 equations, 3 figures, 2 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Our contribution
  3. Background
  4. Signal Temporal Logic
  5. Finding continuous representations
  6. Bayesian Optimization (BO)
  7. Retrieval-Augmented STL Requirement Mining
  8. Building and Querying the Semantic Vector Database
  9. Selecting STL Formulae
  10. Computing Formulae Embeddings
  11. Index Structure Organization
  12. Semantic Database Implementation
  13. Semantic Database Effectiveness
  14. Bayesian Optimization in the Semantic Space of Formulae
  15. Experiments
  16. ...and 13 more sections

Figures (3)

  • Figure 1: Regular and anomalous trajectories sampled from the testes datasets.
  • Figure 2: Signals sampled from $\mu_0$.
  • Figure : Sampling a trajectory over the interval $[a, b]$ according to $\mu_0$