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
• Authors: Matt Luckcuck, Angelo Ferrando, Fatma Faruq,
• 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

• 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.