Distributed Monitoring of Timed Properties

• URL: http://arxiv.org/abs/2410.00465v1
• Date: Tue, 1 Oct 2024 07:46:59 GMT
• Title: Distributed Monitoring of Timed Properties
• Authors: Léo Henry, Thierry Jéron, Nicolas Markey, Victor Roussanaly,
• Abstract summary: runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. We propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components.
• Score: 0.22499166814992436
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In formal verification, runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. In such a setting, the system is made of several components, each equipped with its own local clock and monitor. The monitors observe events occurring on their associated component, and receive timestamped events from other monitors through FIFO channels. Since clocks are local, they cannot be perfectly synchronized, resulting in imprecise timestamps. Consequently, they must be seen as intervals, leading monitors to consider possible reorderings of events. In this context, each monitor aims to provide, as early as possible, a verdict on the property it is monitoring, based on its potentially incomplete and imprecise knowledge of the current execution. In this paper, we propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components. We first identify the date at which a monitor can safely compute a verdict based on received events. We then propose a monitoring algorithm that updates this date when new information arrives, maintains the current set of states in which the property can reside, and updates its verdict accordingly.

Related papers

• Tooling Offline Runtime Verification against Interaction Models : recognizing sliced behaviors using parameterized simulation [0.4199844472131921]
  offline runtime verification involves the static analysis of executions of a system against a specification. For distributed systems, it is generally not possible to characterize executions in the form of global traces, given the absence of a global clock. We propose an algorithm that verifies the conformity of such traces against formal specifications called Interactions.
  arXiv  Detail & Related papers  (2024-03-05T16:09:55Z)
• Sound Concurrent Traces for Online Monitoring Technical Report [0.0]
  concurrent programs typically rely on collecting traces to abstract program executions. We first define the notion of when a trace is representative of a concurrent execution. We then present a non-blocking vector clock algorithm to collect sound concurrent traces on the fly.
  arXiv  Detail & Related papers  (2024-02-28T15:11:39Z)
• 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)
• Runtime Monitoring of Dynamic Fairness Properties [3.372200852710289]
  A machine-learned system that is fair in static decision-making tasks may have biased societal impacts in the long-run. While existing works try to identify and mitigate long-run biases through smart system design, we introduce techniques for monitoring fairness in real time. Our goal is to build and deploy a monitor that will continuously observe a long sequence of events generated by the system in the wild.
  arXiv  Detail & Related papers  (2023-05-08T13:32:23Z)
• 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)
• A Generalized & Robust Framework For Timestamp Supervision in Temporal Action Segmentation [79.436224998992]
  In temporal action segmentation, Timestamp supervision requires only a handful of labelled frames per video sequence. We propose a novel Expectation-Maximization based approach that leverages the label uncertainty of unlabelled frames. Our proposed method produces SOTA results and even exceeds the fully-supervised setup in several metrics and datasets.
  arXiv  Detail & Related papers  (2022-07-20T18:30:48Z)
• Towards Partial Monitoring: It is Always too Soon to Give Up [0.0]
  This paper revises the notion of monitorability from a practical perspective. We show how non-monitorable properties can still be used to generate partial monitors, which can partially check the properties.
  arXiv  Detail & Related papers  (2021-10-25T01:55:05Z)
• Content-Based Detection of Temporal Metadata Manipulation [91.34308819261905]
  We propose an end-to-end approach to verify whether the purported time of capture of an image is consistent with its content and geographic location. The central idea is the use of supervised consistency verification, in which we predict the probability that the image content, capture time, and geographical location are consistent. Our approach improves upon previous work on a large benchmark dataset, increasing the classification accuracy from 59.03% to 81.07%.
  arXiv  Detail & Related papers  (2021-03-08T13:16:19Z)
• Predicting Temporal Sets with Deep Neural Networks [50.53727580527024]
  We propose an integrated solution based on the deep neural networks for temporal sets prediction. A unique perspective is to learn element relationship by constructing set-level co-occurrence graph. We design an attention-based module to adaptively learn the temporal dependency of elements and sets.
  arXiv  Detail & Related papers  (2020-06-20T03:29:02Z)
• Towards Streaming Perception [70.68520310095155]
  We present an approach that coherently integrates latency and accuracy into a single metric for real-time online perception. The key insight behind this metric is to jointly evaluate the output of the entire perception stack at every time instant. We focus on the illustrative tasks of object detection and instance segmentation in urban video streams, and contribute a novel dataset with high-quality and temporally-dense annotations.
  arXiv  Detail & Related papers  (2020-05-21T01:51:35Z)
• Convergence of Update Aware Device Scheduling for Federated Learning at the Wireless Edge [84.55126371346452]
  We study federated learning at the wireless edge, where power-limited devices with local datasets collaboratively train a joint model with the help of a remote parameter server (PS) We design novel scheduling and resource allocation policies that decide on the subset of the devices to transmit at each round. The results of numerical experiments show that the proposed scheduling policy, based on both the channel conditions and the significance of the local model updates, provides a better long-term performance than scheduling policies based only on either of the two metrics individually.
  arXiv  Detail & Related papers  (2020-01-28T15:15:22Z)

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.