Towards Partial Monitoring: It is Always too Soon to Give Up
- URL: http://arxiv.org/abs/2110.12585v1
- Date: Mon, 25 Oct 2021 01:55:05 GMT
- Title: Towards Partial Monitoring: It is Always too Soon to Give Up
- Authors: Angelo Ferrando (University of Genova), Rafael C. Cardoso (The
University of Manchester)
- Abstract summary: 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.
- Score: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Runtime Verification is a lightweight formal verification technique. It is
used to verify at runtime whether the system under analysis behaves as
expected. The expected behaviour is usually formally specified by means of
properties, which are used to automatically synthesise monitors. A monitor is a
device that, given a sequence of events representing a system execution,
returns a verdict symbolising the satisfaction or violation of the formal
property. Properties that can (resp. cannot) be verified at runtime by a
monitor are called monitorable and non-monitorable, respectively. In this
paper, we revise the notion of monitorability from a practical perspective,
where we show how non-monitorable properties can still be used to generate
partial monitors, which can partially check the properties. Finally, we present
the implications both from a theoretical and practical perspectives.
Related papers
- Distributed Monitoring of Timed Properties [0.22499166814992436]
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.
arXiv Detail & Related papers (2024-10-01T07:46:59Z) - Configuration Monitor Synthesis [1.9977040198878984]
We introduce configuration monitoring to determine an unknown configuration of a running system.
We develop a modular and generic pipeline to synthesize automata-theoretic configuration monitors.
We show that our approach also generalizes and unifies existing work on runtime monitoring and fault diagnosis.
arXiv Detail & Related papers (2024-08-30T15:57:35Z) - Third-Party Language Model Performance Prediction from Instruction [59.574169249307054]
Language model-based instruction-following systems have lately shown increasing performance on many benchmark tasks.
A user may easily prompt a model with an instruction without any idea of whether the responses should be expected to be accurate.
We propose a third party performance prediction framework, where a separate model is trained to predict the metric resulting from evaluating an instruction-following system on a task.
arXiv Detail & Related papers (2024-03-19T03:53:47Z) - 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) - Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language.
Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool.
arXiv Detail & Related papers (2022-09-28T12:19:13Z) - Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAI bridges the gap between interpretable formal verification and scalability.
We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
arXiv Detail & Related papers (2021-09-25T22:53:24Z) - No Need to Know Physics: Resilience of Process-based Model-free Anomaly
Detection for Industrial Control Systems [95.54151664013011]
We present a novel framework to generate adversarial spoofing signals that violate physical properties of the system.
We analyze four anomaly detectors published at top security conferences.
arXiv Detail & Related papers (2020-12-07T11:02:44Z) - A Background-Agnostic Framework with Adversarial Training for Abnormal
Event Detection in Video [120.18562044084678]
Abnormal event detection in video is a complex computer vision problem that has attracted significant attention in recent years.
We propose a background-agnostic framework that learns from training videos containing only normal events.
arXiv Detail & Related papers (2020-08-27T18:39:24Z) - SeCo: Exploring Sequence Supervision for Unsupervised Representation
Learning [114.58986229852489]
In this paper, we explore the basic and generic supervision in the sequence from spatial, sequential and temporal perspectives.
We derive a particular form named Contrastive Learning (SeCo)
SeCo shows superior results under the linear protocol on action recognition, untrimmed activity recognition and object tracking.
arXiv Detail & Related papers (2020-08-03T15:51:35Z)
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.