Monitoring Data-aware Temporal Properties (Extended Version)

• URL: http://arxiv.org/abs/2605.14666v1
• Date: Thu, 14 May 2026 10:23:11 GMT
• Title: Monitoring Data-aware Temporal Properties (Extended Version)
• Abstract summary: 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.
• Score: 56.386411908764494
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Dynamic systems in AI are often complex and heterogeneous, so that an internal specification is not accessible and verification techniques such as model checking are not applicable. Monitoring is in such cases an attractive alternative, as it evaluates desirable properties along traces generated by an unknown dynamic system. In this work, we consider anticipatory monitoring of linear-time properties enriched with an arbitrary SMT theory over finite traces (LTLfMT). 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. Under reasonable assumptions on the background theory, we present and formally prove the correctness of a novel foundational framework for monitoring properties in an expressive fragment of LTLfMT. The framework combines automata-theoretic methods to handle the temporal aspects of the logic, with automated reasoning techniques to address the first-order dimension. Moreover, we identify for the first time decidable fragments of this monitoring problem that are practically relevant as they combine linear arithmetic with uninterpreted functions, which covers e.g. data-aware business processes and dynamic systems operating over a read-only database. Feasibility is witnessed by a prototype implementation and preliminary evaluation.

Related papers

• Embedding-Aware Feature Discovery: Bridging Latent Representations and Interpretable Features in Event Sequences [5.03287845497428]
  Industrial financial systems operate on temporal event sequences such as transactions, user actions, and system logs.<n>We introduce Embedding-Aware Feature Discovery (EAFD), a unified framework that bridges the gap between learned embeddings and feature-based pipelines.<n>EAFD iteratively discovers, evaluates, and refines features directly from raw event sequences using two complementary criteria.
  arXiv  Detail & Related papers  (2026-03-16T14:29:26Z)
• Quantitative Monitoring of Signal First-Order Logic [11.310581148639088]
  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.
  arXiv  Detail & Related papers  (2026-02-28T16:23:11Z)
• Labels Matter More Than Models: Quantifying the Benefit of Supervised Time Series Anomaly Detection [56.302586730134806]
  Time series anomaly detection (TSAD) is a critical data mining task often constrained by label scarcity.<n>Current research predominantly focuses on Unsupervised Time-series Anomaly Detection.<n>This paper challenges the premise that architectural complexity is the optimal path for TSAD.
  arXiv  Detail & Related papers  (2025-11-20T08:32:49Z)
• 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)
• A Poisson-Gamma Dynamic Factor Model with Time-Varying Transition Dynamics [51.147876395589925]
  A non-stationary PGDS is proposed to allow the underlying transition matrices to evolve over time. A fully-conjugate and efficient Gibbs sampler is developed to perform posterior simulation. Experiments show that, in comparison with related models, the proposed non-stationary PGDS achieves improved predictive performance.
  arXiv  Detail & Related papers  (2024-02-26T04:39:01Z)
• Monitoring Algorithmic Fairness under Partial Observations [3.790015813774933]
  runtime verification techniques have been introduced to monitor the algorithmic fairness of deployed systems. Previous monitoring techniques assume full observability of the states of the monitored system. We extend fairness monitoring to systems modeled as partially observed Markov chains.
  arXiv  Detail & Related papers  (2023-08-01T07:35:54Z)
• Uncovering the Missing Pattern: Unified Framework Towards Trajectory Imputation and Prediction [60.60223171143206]
  Trajectory prediction is a crucial undertaking in understanding entity movement or human behavior from observed sequences. Current methods often assume that the observed sequences are complete while ignoring the potential for missing values. This paper presents a unified framework, the Graph-based Conditional Variational Recurrent Neural Network (GC-VRNN), which can perform trajectory imputation and prediction simultaneously.
  arXiv  Detail & Related papers  (2023-03-28T14:27:27Z)
• Self-Supervised Representation Learning from Temporal Ordering of Automated Driving Sequences [49.91741677556553]
  We propose TempO, a temporal ordering pretext task for pre-training region-level feature representations for perception tasks. We embed each frame by an unordered set of proposal feature vectors, a representation that is natural for object detection or tracking systems. Extensive evaluations on the BDD100K, nuImages, and MOT17 datasets show that our TempO pre-training approach outperforms single-frame self-supervised learning methods.
  arXiv  Detail & Related papers  (2023-02-17T18:18:27Z)
• Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic [8.914271888521652]
  We introduce a new semantic property of "finite summary", which guarantees the existence of a faithful finite-state abstraction. Several decidability conditions studied in formal methods and database theory can be seen as concrete, checkable instances of this property. Our results allow us to analyze systems that were out of reach in earlier approaches.
  arXiv  Detail & Related papers  (2022-03-15T15:14:25Z)
• 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)
• Stochastically forced ensemble dynamic mode decomposition for forecasting and analysis of near-periodic systems [65.44033635330604]
  We introduce a novel load forecasting method in which observed dynamics are modeled as a forced linear system. We show that its use of intrinsic linear dynamics offers a number of desirable properties in terms of interpretability and parsimony. Results are presented for a test case using load data from an electrical grid.
  arXiv  Detail & Related papers  (2020-10-08T20:25:52Z)

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.