Monitoring Second-Order Hyperproperties

• URL: http://arxiv.org/abs/2404.09652v1
• Date: Mon, 15 Apr 2024 10:33:39 GMT
• Title: Monitoring Second-Order Hyperproperties
• Authors: Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger,
• Abstract summary: We study the monitoring of complex hyperproperties at runtime. We present the first monitoring algorithm for the much more expressive class of second-order hyperproperties. We show that the monitoring of the second-order hyperproperties of Hyper$2$LTL$_f$ can be reduced to monitoring first-order hyperproperties.
• Score: 4.099848175176399
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Hyperproperties express the relationship between multiple executions of a system. This is needed in many AI-related fields, such as knowledge representation and planning, to capture system properties related to knowledge, information flow, and privacy. In this paper, we study the monitoring of complex hyperproperties at runtime. Previous work in this area has either focused on the simpler problem of monitoring trace properties (which are sets of traces, while hyperproperties are sets of sets of traces) or on monitoring first-order hyperproperties, which are expressible in temporal logics with first-order quantification over traces, such as HyperLTL. We present the first monitoring algorithm for the much more expressive class of second-order hyperproperties. Second-order hyperproperties include system properties like common knowledge, which cannot be expressed in first-order logics like HyperLTL. We introduce Hyper$^2$LTL$_f$, a temporal logic over finite traces that allows for second-order quantification over sets of traces. We study the monitoring problem in two fundamental execution models: (1) the parallel model, where a fixed number of traces is monitored in parallel, and (2) the sequential model, where an unbounded number of traces is observed sequentially, one trace after the other. For the parallel model, we show that the monitoring of the second-order hyperproperties of Hyper$^2$LTL$_f$ can be reduced to monitoring first-order hyperproperties. For the sequential model, we present a monitoring algorithm that handles second-order quantification efficiently, exploiting optimizations based on the monotonicity of subformulas, graph-based storing of executions, and fixpoint hashing. We present experimental results from a range of benchmarks, including examples from common knowledge and planning.

Related papers

• UniT: Unified Multimodal Chain-of-Thought Test-time Scaling [85.590774707406]
  Unified models can handle both multimodal understanding and generation within a single architecture, yet they typically operate in a single pass without iteratively refining their outputs.<n>We introduce UniT, a framework for multimodal test-time scaling that enables a single unified model to reason, verify, and refine across multiple rounds.
  arXiv  Detail & Related papers  (2026-02-12T18:59:49Z)
• 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)
• Higher-order Linear Attention [59.92962330635185]
  quadratic cost of scaled dot-product attention is a central obstacle to scaling autoregressive language models to long contexts.<n>We introduce Higher-order Linear Attention (HLA), a causal, streaming mechanism that realizes higher interactions via compact prefix sufficient statistics.
  arXiv  Detail & Related papers  (2025-10-31T07:54:37Z)
• Sequential-Parallel Duality in Prefix Scannable Models [68.39855814099997]
  Recent developments have given rise to various models, such as Gated Linear Attention (GLA) and Mamba.<n>This raises a natural question: can we characterize the full class of neural sequence models that support near-constant-time parallel evaluation and linear-time, constant-space sequential inference?
  arXiv  Detail & Related papers  (2025-06-12T17:32:02Z)
• Exploring Microstructural Dynamics in Cryptocurrency Limit Order Books: Better Inputs Matter More Than Stacking Another Hidden Layer [9.2463347238923]
  We aim to examine whether adding extra hidden layers or parameters to "blackbox ish" neural networks genuinely enhances short term price forecasting.<n>We benchmark a spectrum of models from interpretable baselines, logistic regression, XGBoost to deep architectures (DeepLOB, Conv1D+LSTM) on BTC/USDT LOB snapshots sampled at 100 ms to multi second intervals using publicly available Bybit data.
  arXiv  Detail & Related papers  (2025-06-06T05:43:30Z)
• Interaction Event Forecasting in Multi-Relational Recursive HyperGraphs: A Temporal Point Process Approach [12.142292322071299]
  This work addresses the problem of forecasting higher-order interaction events in multi-relational recursive hypergraphs. The proposed model, textitRelational Recursive Hyperedge Temporal Point Process (RRHyperTPP), uses an encoder that learns a dynamic node representation based on the historical interaction patterns. We have experimentally shown that our models perform better than previous state-of-the-art methods for interaction forecasting.
  arXiv  Detail & Related papers  (2024-04-27T15:46:54Z)
• TimeGraphs: Graph-based Temporal Reasoning [64.18083371645956]
  TimeGraphs is a novel approach that characterizes dynamic interactions as a hierarchical temporal graph. Our approach models the interactions using a compact graph-based representation, enabling adaptive reasoning across diverse time scales. We evaluate TimeGraphs on multiple datasets with complex, dynamic agent interactions, including a football simulator, the Resistance game, and the MOMA human activity dataset.
  arXiv  Detail & Related papers  (2024-01-06T06:26:49Z)
• Joint Entity and Relation Extraction with Span Pruning and Hypergraph Neural Networks [58.43972540643903]
  We propose HyperGraph neural network for ERE ($hgnn$), which is built upon the PL-marker (a state-of-the-art marker-based pipleline model) To alleviate error propagation,we use a high-recall pruner mechanism to transfer the burden of entity identification and labeling from the NER module to the joint module of our model. Experiments on three widely used benchmarks for ERE task show significant improvements over the previous state-of-the-art PL-marker.
  arXiv  Detail & Related papers  (2023-10-26T08:36:39Z)
• HyperAttention: Long-context Attention in Near-Linear Time [78.33061530066185]
  We present an approximate attention mechanism named HyperAttention to address the computational challenges posed by the growing complexity of long contexts. Empirically, employing Locality Sensitive Hashing (LSH) to identify large entries, HyperAttention outperforms existing methods. We validate the empirical performance of HyperAttention on a variety of different long-context length datasets.
  arXiv  Detail & Related papers  (2023-10-09T17:05:25Z)
• From random-walks to graph-sprints: a low-latency node embedding framework on continuous-time dynamic graphs [4.372841335228306]
  We propose a framework for continuous-time-dynamic-graphs (CTDGs) that has low latency and is competitive with state-of-the-art, higher latency models. In our framework, time-aware node embeddings summarizing multi-hop information are computed using only single-hop operations on the incoming edges. We demonstrate that our graph-sprints features, combined with a machine learning, achieve competitive performance.
  arXiv  Detail & Related papers  (2023-07-17T12:25:52Z)
• Unified Sequence-to-Sequence Learning for Single- and Multi-Modal Visual Object Tracking [64.28025685503376]
  SeqTrack casts visual tracking as a sequence generation task, forecasting object bounding boxes in an autoregressive manner. SeqTrackv2 integrates a unified interface for auxiliary modalities and a set of task-prompt tokens to specify the task. This sequence learning paradigm not only simplifies the tracking framework, but also showcases superior performance across 14 challenging benchmarks.
  arXiv  Detail & Related papers  (2023-04-27T17:56:29Z)
• End-to-end Tracking with a Multi-query Transformer [96.13468602635082]
  Multiple-object tracking (MOT) is a challenging task that requires simultaneous reasoning about location, appearance, and identity of the objects in the scene over time. Our aim in this paper is to move beyond tracking-by-detection approaches, to class-agnostic tracking that performs well also for unknown object classes.
  arXiv  Detail & Related papers  (2022-10-26T10:19:37Z)
• Multivariate Time Series Forecasting with Dynamic Graph Neural ODEs [65.18780403244178]
  We propose a continuous model to forecast Multivariate Time series with dynamic Graph neural Ordinary Differential Equations (MTGODE) Specifically, we first abstract multivariate time series into dynamic graphs with time-evolving node features and unknown graph structures. Then, we design and solve a neural ODE to complement missing graph topologies and unify both spatial and temporal message passing.
  arXiv  Detail & Related papers  (2022-02-17T02:17:31Z)
• Exploiting Multiple Timescales in Hierarchical Echo State Networks [0.0]
  Echo state networks (ESNs) are a powerful form of reservoir computing that only require training of linear output weights. Here we explore the timescales in hierarchical ESNs, where the reservoir is partitioned into two smaller reservoirs linked with distinct properties.
  arXiv  Detail & Related papers  (2021-01-11T22:33:17Z)
• Analyzing Unaligned Multimodal Sequence via Graph Convolution and Graph Pooling Fusion [28.077474663199062]
  We propose a novel model, termed Multimodal Graph, to investigate the effectiveness of graph neural networks (GNN) on modeling multimodal sequential data. Our graph-based model reaches state-of-the-art performance on two benchmark datasets.
  arXiv  Detail & Related papers  (2020-11-27T06:12:14Z)

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.