Runtime Verification via Rational Monitor with Imperfect Information

• URL: http://arxiv.org/abs/2408.11627v1
• Date: Wed, 21 Aug 2024 13:56:06 GMT
• Title: Runtime Verification via Rational Monitor with Imperfect Information
• Authors: Angelo Ferrando, Vadim Malvone,
• Abstract summary: Traditional verification assumes perfect information, meaning the monitoring component perceives everything accurately. This assumption often fails, especially with autonomous systems operating in real-world environments. We extend standard RV of Linear Temporal Logic properties to accommodate scenarios where the monitor has imperfect information and behaves rationally.
• Score: 2.7323347531070974
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Trusting software systems, particularly autonomous ones, is challenging. To address this, formal verification techniques can ensure these systems behave as expected. Runtime Verification (RV) is a leading, lightweight method for verifying system behaviour during execution. However, traditional RV assumes perfect information, meaning the monitoring component perceives everything accurately. This assumption often fails, especially with autonomous systems operating in real-world environments where sensors might be faulty. Additionally, traditional RV considers the monitor to be passive, lacking the capability to interpret the system's information and thus unable to address incomplete data. In this work, we extend standard RV of Linear Temporal Logic properties to accommodate scenarios where the monitor has imperfect information and behaves rationally. We outline the necessary engineering steps to update the verification pipeline and demonstrate our implementation in a case study involving robotic systems.

Related papers

• Mind the Interference: Retaining Pre-trained Knowledge in Parameter Efficient Continual Learning of Vision-Language Models [79.28821338925947]
  Domain-Class Incremental Learning is a realistic but challenging continual learning scenario. To handle these diverse tasks, pre-trained Vision-Language Models (VLMs) are introduced for their strong generalizability. This incurs a new problem: the knowledge encoded in the pre-trained VLMs may be disturbed when adapting to new tasks, compromising their inherent zero-shot ability. Existing methods tackle it by tuning VLMs with knowledge distillation on extra datasets, which demands heavy overhead. We propose the Distribution-aware Interference-free Knowledge Integration (DIKI) framework, retaining pre-trained knowledge of
  arXiv  Detail & Related papers  (2024-07-07T12:19:37Z)
• Certified Control for Train Sign Classification [0.0]
  The KI-LOK research project is involved in developing new methods for certifying such AI-based systems. Here we explore the utility of a certified control architecture for a runtime monitor that prevents false positive detection of traffic signs.
  arXiv  Detail & Related papers  (2023-11-16T11:02:10Z)
• A Requirements-Driven Platform for Validating Field Operations of Small Uncrewed Aerial Vehicles [48.67061953896227]
  DroneReqValidator (DRV) allows sUAS developers to define the operating context, configure multi-sUAS mission requirements, specify safety properties, and deploy their own custom sUAS applications in a high-fidelity 3D environment. The DRV Monitoring system collects runtime data from sUAS and the environment, analyzes compliance with safety properties, and captures violations.
  arXiv  Detail & Related papers  (2023-07-01T02:03:49Z)
• Interpretable Self-Aware Neural Networks for Robust Trajectory Prediction [50.79827516897913]
  We introduce an interpretable paradigm for trajectory prediction that distributes the uncertainty among semantic concepts. We validate our approach on real-world autonomous driving data, demonstrating superior performance over state-of-the-art baselines.
  arXiv  Detail & Related papers  (2022-11-16T06:28:20Z)
• 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)
• Lightweight Automated Feature Monitoring for Data Streams [1.4658400971135652]
  We propose a flexible system, Feature Monitoring (FM), that detects data drifts in such data sets. It monitors all features that are used by the system, while providing an interpretable features ranking whenever an alarm occurs. This illustrates how FM eliminates the need to add custom signals to detect specific types of problems and that monitoring the available space of features is often enough.
  arXiv  Detail & Related papers  (2022-07-18T14:38:11Z)
• Formalizing and Evaluating Requirements of Perception Systems for Automated Vehicles using Spatio-Temporal Perception Logic [25.070876549371693]
  We present a logic that enables reasoning over perception data using spatial and temporal operators. One major advantage ofSTPL is that it facilitates basic sanity checks on the functional performance of the perception system.
  arXiv  Detail & Related papers  (2022-06-29T02:36:53Z)
• Monitoring of Perception Systems: Deterministic, Probabilistic, and Learning-based Fault Detection and Identification [21.25149064251918]
  We formalize the problem of runtime fault detection and identification in perception systems. We provide a set of deterministic, probabilistic, and learning-based algorithms that use diagnostic graphs to perform fault detection and identification. We conclude the paper with an experimental evaluation, which recreates several realistic failure modes in the LGSVL open-source autonomous driving simulator.
  arXiv  Detail & Related papers  (2022-05-22T19:08:45Z)
• Controlling nonlinear dynamical systems into arbitrary states using machine learning [77.34726150561087]
  We propose a novel and fully data driven control scheme which relies on machine learning (ML) Exploiting recently developed ML-based prediction capabilities of complex systems, we demonstrate that nonlinear systems can be forced to stay in arbitrary dynamical target states coming from any initial state. Having this highly flexible control scheme with little demands on the amount of required data on hand, we briefly discuss possible applications that range from engineering to medicine.
  arXiv  Detail & Related papers  (2021-02-23T16:58:26Z)
• Monitoring and Diagnosability of Perception Systems [21.25149064251918]
  We propose a mathematical model for runtime monitoring and fault detection and identification in perception systems. We demonstrate our monitoring system, dubbed PerSyS, in realistic simulations using the LGSVL self-driving simulator and the Apollo Auto autonomy software stack.
  arXiv  Detail & Related papers  (2020-11-11T23:03:14Z)
• Training-free Monocular 3D Event Detection System for Traffic Surveillance [93.65240041833319]
  Existing event detection systems are mostly learning-based and have achieved convincing performance when a large amount of training data is available. In real-world scenarios, collecting sufficient labeled training data is expensive and sometimes impossible. We propose a training-free monocular 3D event detection system for traffic surveillance.
  arXiv  Detail & Related papers  (2020-02-01T04:42:57Z)

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.