Retrieval-Augmented Mining of Temporal Logic Specifications from Data

• URL: http://arxiv.org/abs/2405.14355v1
• Date: Thu, 23 May 2024 09:29:00 GMT
• Title: Retrieval-Augmented Mining of Temporal Logic Specifications from Data
• Authors: Gaia Saveri, Luca Bortolussi,
• Abstract summary: This work addresses the task of learning STL requirements from observed behaviors in a data-driven manner. 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.
• Score: 0.46040036610482665
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Short-Long Convolutions Help Hardware-Efficient Linear Attention to Focus on Long Sequences [60.489682735061415]
  We propose CHELA, which replaces state space models with short-long convolutions and implements linear attention in a divide-and-conquer manner. Our experiments on the Long Range Arena benchmark and language modeling tasks demonstrate the effectiveness of the proposed method.
  arXiv  Detail & Related papers  (2024-06-12T12:12:38Z)
• Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption [3.4764840969876722]
  We propose a protocol for online monitoring that keeps arithmetic data concealed from the server. We build on this protocol to allow operations over encrypted values, e.g., to compute a safety measurement combining distance, velocity, and so forth. Overall, our protocol enables oblivious online monitoring of discrete-time real-valued signals against signal temporal logic (STL) formulas.
  arXiv  Detail & Related papers  (2024-05-27T02:32:16Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  We consider the problem of automatically synthesizing formal specifications from system executions. Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead.
  arXiv  Detail & Related papers  (2023-10-26T14:13:15Z)
• State Sequences Prediction via Fourier Transform for Representation Learning [111.82376793413746]
  We propose State Sequences Prediction via Fourier Transform (SPF), a novel method for learning expressive representations efficiently. We theoretically analyze the existence of structural information in state sequences, which is closely related to policy performance and signal regularity. Experiments demonstrate that the proposed method outperforms several state-of-the-art algorithms in terms of both sample efficiency and performance.
  arXiv  Detail & Related papers  (2023-10-24T14:47:02Z)
• STL-Based Synthesis of Feedback Controllers Using Reinforcement Learning [8.680676599607125]
  Deep Reinforcement Learning (DRL) has the potential to be used for synthesizing feedback controllers (agents) for various complex systems with unknown dynamics. In RL, the reward function plays a crucial role in specifying the desired behaviour of these agents. We provide a systematic way of generating rewards in real-time by using the quantitative semantics of Signal Temporal Logic (STL) We evaluate our STL-based reinforcement learning mechanism on several complex continuous control benchmarks and compare our STL semantics with those available in the literature in terms of their efficacy in synthesizing the controller agent.
  arXiv  Detail & Related papers  (2022-12-02T08:31:46Z)
• Learning Spatio-Temporal Specifications for Dynamical Systems [0.757024681220677]
  We propose a framework for learning-temporal (ST properties) as logic specifications from data. We introduce SVM-STL, an extension of Signal Signal Temporal Logic (STL), capable of mitigating temporal and spatial properties of a wide range of dynamical systems. Our framework utilizes machine learning techniques to learn SVM-STL specifications from system executions given by sequences of spatial patterns.
  arXiv  Detail & Related papers  (2021-12-20T18:03:01Z)
• NSL: Hybrid Interpretable Learning From Noisy Raw Data [66.15862011405882]
  This paper introduces a hybrid neural-symbolic learning framework, called NSL, that learns interpretable rules from labelled unstructured data. NSL combines pre-trained neural networks for feature extraction with FastLAS, a state-of-the-art ILP system for rule learning under the answer set semantics. We demonstrate that NSL is able to learn robust rules from MNIST data and achieve comparable or superior accuracy when compared to neural network and random forest baselines.
  arXiv  Detail & Related papers  (2020-12-09T13:02:44Z)
• Representation Learning for Sequence Data with Deep Autoencoding Predictive Components [96.42805872177067]
  We propose a self-supervised representation learning method for sequence data, based on the intuition that useful representations of sequence data should exhibit a simple structure in the latent space. We encourage this latent structure by maximizing an estimate of predictive information of latent feature sequences, which is the mutual information between past and future windows at each time step. We demonstrate that our method recovers the latent space of noisy dynamical systems, extracts predictive features for forecasting tasks, and improves automatic speech recognition when used to pretrain the encoder on large amounts of unlabeled data.
  arXiv  Detail & Related papers  (2020-10-07T03:34:01Z)
• A Trainable Optimal Transport Embedding for Feature Aggregation and its Relationship to Attention [96.77554122595578]
  We introduce a parametrized representation of fixed size, which embeds and then aggregates elements from a given input set according to the optimal transport plan between the set and a trainable reference. Our approach scales to large datasets and allows end-to-end training of the reference, while also providing a simple unsupervised learning mechanism with small computational cost.
  arXiv  Detail & Related papers  (2020-06-22T08:35:58Z)
• On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach [3.9461038686072847]
  We introduce a forgetting-based approach in Computation Tree Logic (CTL) We show that it can be used to compute the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a property under a given model and over a given signature. We also study its theoretical properties and show that our notion of forgetting satisfies existing essential postulates of knowledge forgetting.
  arXiv  Detail & Related papers  (2020-03-13T21:51:59Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.