Quantitative Monitoring of Signal First-Order Logic

• URL: http://arxiv.org/abs/2603.00728v2
• Date: Tue, 03 Mar 2026 14:12:01 GMT
• Title: Quantitative Monitoring of Signal First-Order Logic
• Authors: Marek Chalupa, Thomas A. Henzinger, N. Ege Saraç, Emily Yu,
• Abstract summary: We provide the first robustness-based quantitative semantics for Signal First-Order Logic (SFO)<n>SFO offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support.<n>This is the first publicly available prototype for online quantitative monitoring of full SFO.
• Score: 11.310581148639088
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.

Related papers

• Order-Aware Test-Time Adaptation: Leveraging Temporal Dynamics for Robust Streaming Inference [18.524636088926425]
  Test-Time Adaptation (TTA) enables pre-trained models to adjust to distribution shift by learning from unlabeled test-time streams.<n>To address this, we introduce Order-Aware Test-Time Adaptation (OATTA)<n>OATTA consistently boosts established baselines, improving accuracy by up to 6.35%.
  arXiv  Detail & Related papers  (2026-01-28T20:07:40Z)
• Interpretable Early Failure Detection via Machine Learning and Trace Checking-based Monitoring [9.565145785280452]
  We develop a framework for interpretable early failure detection based on vectorized trace checking.<n>The framework shows a 2-10% net improvement in key performance metrics compared to the state-of-the-art methods.
  arXiv  Detail & Related papers  (2025-08-25T08:30:01Z)
• 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)
• Scalable Learning of Latent Language Structure With Logical Offline Cycle Consistency [71.42261918225773]
  Conceptually, LOCCO can be viewed as a form of self-learning where the semantic being trained is used to generate annotations for unlabeled text. As an added bonus, the annotations produced by LOCCO can be trivially repurposed to train a neural text generation model.
  arXiv  Detail & Related papers  (2023-05-31T16:47:20Z)
• Time-to-Green predictions for fully-actuated signal control systems with supervised learning [56.66331540599836]
  This paper proposes a time series prediction framework using aggregated traffic signal and loop detector data. We utilize state-of-the-art machine learning models to predict future signal phases' duration. Results based on an empirical data set from a fully-actuated signal control system in Zurich, Switzerland, show that machine learning models outperform conventional prediction methods.
  arXiv  Detail & Related papers  (2022-08-24T07:50:43Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Real-Time Scene Text Detection with Differentiable Binarization and Adaptive Scale Fusion [62.269219152425556]
  segmentation-based scene text detection methods have drawn extensive attention in the scene text detection field. We propose a Differentiable Binarization (DB) module that integrates the binarization process into a segmentation network. An efficient Adaptive Scale Fusion (ASF) module is proposed to improve the scale robustness by fusing features of different scales adaptively.
  arXiv  Detail & Related papers  (2022-02-21T15:30:14Z)
• Sequential convolutional network for behavioral pattern extraction in gait recognition [0.7874708385247353]
  We propose a sequential convolutional network (SCN) to learn the walking pattern of individuals. In SCN, behavioral information extractors (BIE) are constructed to comprehend intermediate feature maps in time series. A multi-frame aggregator in SCN performs feature integration on a sequence whose length is uncertain, via a mobile 3D convolutional layer.
  arXiv  Detail & Related papers  (2021-04-23T08:44:10Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• Unsupervised Online Anomaly Detection On Irregularly Sampled Or Missing Valued Time-Series Data Using LSTM Networks [0.0]
  We study anomaly detection and introduce an algorithm that processes variable length, irregularly sampled sequences or sequences with missing values. Our algorithm is fully unsupervised, however, can be readily extended to supervised or semisupervised cases.
  arXiv  Detail & Related papers  (2020-05-25T09:41:04Z)

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.