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
• 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

• On the Time and Frequency Domain Representations of Signals for CPS Specification [1.59594089941013]
  We investigate the use of time-frequency representations to specify Cyber-Physical Systems (CPSs) requirements.<n>We derive the desiderata for a specification language that uses time-frequency representations and propose Signal-Spectrum Temporal Logic (S2TL)<n>We operationalise the S2TL semantics for monitoring CPS traces, and implement a monitor.
  arXiv  Detail & Related papers  (2026-08-21T14:38:34Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• Monitoring Data-aware Temporal Properties (Extended Version) [56.386411908764494]
  We consider anticipatory monitoring of linear-time properties enriched with an arbitrary SMT theory over finite traces.<n>Anticipatory monitoring in this setting is highly challenging, as the monitoring state depends on both the trace prefix seen so far and all its possible finite continuations.<n>We present and formally prove the correctness of a novel foundational framework for monitoring properties in an expressive fragment offMT.
  arXiv  Detail & Related papers  (2026-05-14T10:23:11Z)
• ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning [5.961092142323502]
  textscReasonSTL is a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation.<n>textscReasonSTL decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction.<n>Experiments show that a 4B model trained with textscReasonSTL achieves state-of-the-art performance in both automatic metrics and human evaluations.
  arXiv  Detail & Related papers  (2026-05-07T16:07:30Z)
• IMPACT: A Dataset for Multi-Granularity Human Procedural Action Understanding in Industrial Assembly [79.737814043505]
  IMPACT is a synchronized five-view RGB-D dataset for deployment-oriented industrial procedural understanding.<n>It is built around real assembly and disassembly of a commercial angle grinder with professional-grade tools.
  arXiv  Detail & Related papers  (2026-04-12T02:09:19Z)
• CLAIRE: Compressed Latent Autoencoder for Industrial Representation and Evaluation -- A Deep Learning Framework for Smart Manufacturing [51.56484100374058]
  CLAIRE is a hybrid end-to-end learning framework that integrates unsupervised deep representation learning with supervised classification for intelligent quality control in smart manufacturing systems.<n>It employs an optimized deep autoencoder to transform raw input into a compact latent space, effectively capturing the intrinsic data structure while suppressing irrelevant or noisy features.<n>The proposed framework highlights the potential of integrating explainable AI with feature-aware regularization for robust fault detection.
  arXiv  Detail & Related papers  (2026-03-06T15:11:58Z)
• LSRIF: Logic-Structured Reinforcement Learning for Instruction Following [56.517329105764475]
  We propose a logic-structured training framework LSRIF that explicitly models instruction logic.<n> Experiments show LSRIF brings significant improvements in instruction-following and general reasoning.
  arXiv  Detail & Related papers  (2026-01-10T05:11:38Z)
• FAIM: Frequency-Aware Interactive Mamba for Time Series Classification [87.84511960413715]
  Time series classification (TSC) is crucial in numerous real-world applications, such as environmental monitoring, medical diagnosis, and posture recognition.<n>We propose FAIM, a lightweight Frequency-Aware Interactive Mamba model.<n>We show that FAIM consistently outperforms existing state-of-the-art (SOTA) methods, achieving a superior trade-off between accuracy and efficiency.
  arXiv  Detail & Related papers  (2025-11-26T08:36:33Z)
• On the Loss of Context-awareness in General Instruction Fine-tuning [101.03941308894191]
  We investigate the loss of context awareness after supervised fine-tuning. We find that the performance decline is associated with a bias toward different roles learned during conversational instruction fine-tuning. We propose a metric to identify context-dependent examples from general instruction fine-tuning datasets.
  arXiv  Detail & Related papers  (2024-11-05T00:16:01Z)
• 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.