Varanus: Runtime Verification for CSP

• URL: http://arxiv.org/abs/2506.14426v1
• Date: Tue, 17 Jun 2025 11:42:14 GMT
• Title: Varanus: Runtime Verification for CSP
• Abstract summary: This paper presents Varanus, an RV tool that monitors a system against an oracle built from a CSP specification.<n>We describe the tool, apply it to a simulated autonomous robotic rover inspecting a nuclear waste store, empirically comparing its performance to two other RV tools using different languages.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Autonomous systems are often used in changeable and unknown environments, where traditional verification may not be suitable. Runtime Verification (RV) checks events performed by a system against a formal specification of its intended behaviour, making it highly suitable for ensuring that an autonomous system is obeying its specification at runtime. Communicating Sequential Processes (CSP) is a process algebra usually used in static verification, which captures behaviour as a trace of events, making it useful for RV as well. Further, CSP has more recently been used to specify autonomous and robotic systems. Though CSP is supported by two extant model checkers, so far it has no RV tool. This paper presents Varanus, an RV tool that monitors a system against an oracle built from a CSP specification. This approach enables the reuse without modifications of a specification that was built, e.g during the system's design. We describe the tool, apply it to a simulated autonomous robotic rover inspecting a nuclear waste store, empirically comparing its performance to two other RV tools using different languages, and demonstrate how it can detect violations of the specification. Varanus can synthesise a monitor from a CSP process in roughly linear time, with respect to the number of states and transitions in the model; and checks each event in roughly constant time.

Related papers

• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  We present PhyAgentOS, a foundation delivering scheduling, verification, memory, benchmarking, and safety as system-level services.<n>Its Session-Centered treats a session, not an action, as the minimum unit of scheduling, compatibility, supervised execution, evidence collection, and acceptance.<n>SessionVerifier distinguishes execution termination from semantic task completion via evidence-grounded verdicts of success, failure, or replan.<n> Benchmarking reuses the deployment session and verification path, so results trace to real execution.
  arXiv  Detail & Related papers  (2026-07-18T04:46:53Z)
• ReactSim-Bench: Benchmarking Reactive Behavior World Model Simulation in Autonomous Driving [56.96697737229895]
  Reactive capability is a key property of data-driven behavior world model simulators for autonomous driving simulation systems.<n>We introduce ReactSim-Bench for evaluating the reactive capability of behavior world model simulation in autonomous driving.
  arXiv  Detail & Related papers  (2026-06-12T03:11:06Z)
• Explainable Runtime Dependency Tracking for AI-RAN Conflict Monitoring [0.0]
  Future AI-integrated Radio Access Networks (AI-RAN) will combine open programmability with learning-enabled xApps, rApps, and control functions that act on shared parameters and key performance indicators (KPIs)<n>For conflict monitoring, it is not enough to know which applications are deployed; the system must also know whether the parameter--KPI dependencies assumed by runtime diagnosis remain valid under the current operating regime.<n>This paper studies a lightweight monitoring primitive for that purpose: tracking an interpretable dependency representation from streaming telemetry events.
  arXiv  Detail & Related papers  (2026-06-04T19:21:32Z)
• In Perfect Harmony: Orchestrating Causality in Actor-Based Systems [0.0]
  Actor-based systems present significant challenges for runtime verification.<n>ACTORCHESTRA is a runtime verification framework for Erlang that automatically tracks causality across multi-actor interactions.<n>Three case studies demonstrate ACTORCHESTRA's effectiveness in detecting complex behavioral violations in real-world actor systems.
  arXiv  Detail & Related papers  (2026-03-18T16:47:25Z)
• Architecture and evaluation protocol for transformer-based visual object tracking in UAV applications [0.0]
  Existing visual trackers either lack robustness in complex scenarios or are too computationally demanding for real-time embedded use.<n>We propose an Modular Asynchronous Tracking Architecture (MATA) that combines a transformer-based tracker with an Extended Kalman Filter.<n>We introduce a hardware-independent, embedded oriented evaluation protocol and a new metric called Normalized time to Failure (NT2F) to quantify how long a tracker can sustain a tracking sequence without external help.
  arXiv  Detail & Related papers  (2026-03-04T10:12:12Z)
• Online Generation of Collision-Free Trajectories in Dynamic Environments [0.9596789853473943]
  We present an online method for converting an arbitrary geometric path represented by a sequence of states into a corresponding kinematically feasible trajectory.<n>The method generates a sequence of quintic/quartic splines that can be discretized at a user-specified control rate, and then streamed to a low-level robot controller.<n> Experiments on a real robot demonstrate that the proposed approach can be used in real-world scenarios including human presence.
  arXiv  Detail & Related papers  (2026-02-28T18:04:50Z)
• Fine-Grained Traceability for Transparent ML Pipelines [10.182692014427909]
  FG-Trac is a model-agnostic framework that establishes fine-grained sample-level traceability throughout machine learning pipelines.<n>It defines an explicit mechanism for capturing and verifying sample lifecycle events across preprocessing and training.<n>It computes contribution scores explicitly grounded in training checkpoints, and anchors these traces to tamper-evident cryptographic commitments.
  arXiv  Detail & Related papers  (2026-01-21T13:21:30Z)
• Querying Perception Streams with Spatial Regular Expressions [3.6814516646862683]
  We introduce SpREs as a novel querying language for pattern matching over streams containing spatial and temporal data. We develop the STREM tool as both an offline and online pattern matching framework for perception data. Using our matching framework, we are able to find over 20,000 matches within 296 ms making STREM applicable in runtime monitoring applications.
  arXiv  Detail & Related papers  (2024-11-08T20:15:27Z)
• Autonomous Vehicle Controllers From End-to-End Differentiable Simulation [60.05963742334746]
  We propose a differentiable simulator and design an analytic policy gradients (APG) approach to training AV controllers. Our proposed framework brings the differentiable simulator into an end-to-end training loop, where gradients of environment dynamics serve as a useful prior to help the agent learn a more grounded policy. We find significant improvements in performance and robustness to noise in the dynamics, as well as overall more intuitive human-like handling.
  arXiv  Detail & Related papers  (2024-09-12T11:50:06Z)
• Runtime Verification via Rational Monitor with Imperfect Information [2.7323347531070974]
  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.
  arXiv  Detail & Related papers  (2024-08-21T13:56:06Z)
• Multistep Inverse Is Not All You Need [87.62730694973696]
  In real-world control settings, the observation space is often unnecessarily high-dimensional and subject to time-correlated noise. It is therefore desirable to learn an encoder to map the observation space to a simpler space of control-relevant variables. We propose a new algorithm, ACDF, which combines multistep-inverse prediction with a latent forward model.
  arXiv  Detail & Related papers  (2024-03-18T16:36:01Z)
• Generative Modeling of Regular and Irregular Time Series Data via Koopman VAEs [50.25683648762602]
  We introduce Koopman VAE, a new generative framework that is based on a novel design for the model prior. Inspired by Koopman theory, we represent the latent conditional prior dynamics using a linear map. KoVAE outperforms state-of-the-art GAN and VAE methods across several challenging synthetic and real-world time series generation benchmarks.
  arXiv  Detail & Related papers  (2023-10-04T07:14:43Z)
• 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)
• On Controller Tuning with Time-Varying Bayesian Optimization [74.57758188038375]
  We will use time-varying optimization (TVBO) to tune controllers online in changing environments using appropriate prior knowledge on the control objective and its changes. We propose a novel TVBO strategy using Uncertainty-Injection (UI), which incorporates the assumption of incremental and lasting changes. Our model outperforms the state-of-the-art method in TVBO, exhibiting reduced regret and fewer unstable parameter configurations.
  arXiv  Detail & Related papers  (2022-07-22T14:54:13Z)
• PSL is Dead. Long Live PSL [3.280253526254703]
  Property Specification Language (PSL) is a form of temporal logic that has been mainly used in discrete domains. We show that by merging machine learning techniques with PSL monitors, we can extend PSL to work on continuous domains.
  arXiv  Detail & Related papers  (2022-05-27T17:55:54Z)
• DAE : Discriminatory Auto-Encoder for multivariate time-series anomaly detection in air transportation [68.8204255655161]
  We propose a novel anomaly detection model called Discriminatory Auto-Encoder (DAE) It uses the baseline of a regular LSTM-based auto-encoder but with several decoders, each getting data of a specific flight phase. Results show that the DAE achieves better results in both accuracy and speed of detection.
  arXiv  Detail & Related papers  (2021-09-08T14:07:55Z)
• SceneChecker: Boosting Scenario Verification using Symmetry Abstractions [3.8995911009078816]
  SceneChecker is a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. SceneChecker shows 20x speedup in verification time, even while using those very tools as reachability subroutines.
  arXiv  Detail & Related papers  (2020-11-21T03:18:55Z)
• A Framework for Automatic Behavior Generation in Multi-Function Swarms [1.290382979353427]
  A framework for automatic behavior generation in multi-function swarms is proposed. The framework is tested on a scenario with three simultaneous tasks. The effect of noise on the behavior characteristics in MAP-elites is investigated.
  arXiv  Detail & Related papers  (2020-07-11T20:50: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.