Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification
Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro · N/A · 2026
Framework
N/A
License
N/A
Stars
N/A
Summary
Runtime Verification is well suited to autonomous and robotic systems because it checks the behaviour that is actually observed during execution. Its main limitation, however, is that it is usually reactive: the monitor detects a violation only after the system has already performed a bad event.
Abstract Summary
Key Points
- Runtime Verification is well suited to autonomous and robotic systems because it checks the behaviour that is actually observed during execution.
- Its main limitation, however, is that it is usually reactive: the monitor detects a violation only after the system has already performed a bad event.
- This can be too late in domains where failures are costly or unsafe
- In this paper we present PREDICTIVE VARANUS, a two-stage verification pipeline that combines VARANUS, a runtime verifier that uses models written in the process algebra Communicating Sequential Processes (CSP), with predictive runtime verification for LTL.
- A CSP model is first used as a conformance gate over the observed event trace; the same model is then translated into a Buchi automaton that constrains the futures explored by a predictive LTL monitor.
Predictive Varanus
Figure 1 shows the components in the Predictive Varanus pipeline. The SUA emits a trace of events. Each event is checked by Varanus for validity with the CSP model, if it is a valid event then it is passed to the Predictive LTL Monitor. The predictive monitor projects the event into the propositional alphabet, and uses the Büchi automaton (translated from the CSP model) to perform PRV .
In this way, the predictive component never reasons about futures for events that Varanus has already rejected as invalid.
Case Study
To evaluate Predictive Varanus , we reuse the example of an autonomous rover patrolling a simulated nuclear waste store, and reuse the CSP model of the rover, that we used in our earlier Varanus work [ 7 ] . The rover’s mission is to inspect the radiation levels at various waypoints.
The radiation readings are categorised into Green , Orange , or Red ; if the radiation is Green then the mission can continue, but Orange , or Red mean that the rover should return to the entry point and abort the mission.
Evaluation
This section presents two evaluations of Predictive Varanus 1 1 1 Predictive Varanus available at: https://github.com/AngeloFerrando/PredictiveVaranus . . First, we study the rover mission from Sect. IV to validate the verdicts and quantify the practical benefit of the approach.
Second, we conduct a quantitative stress test on synthetic CSP models to assess computational overhead and scalability under controlled variations of model size, branching structure, and termination depth.
Sources and Demonstrations
Figures are reproduced from Ferrando et al. See the full paper for experimental details and the project page, when the paper links one, for demonstrations and videos.
Related Papers
3DThinkVLA: Endowing Vision-Language-Action Models with Latent 3D Priors via 3D-Thinking-Guided Co-training
Jiaxin Shi, Xidong Zhang, Fucai Zhu et al.
We propose a 3D-thinking-guided co-training framework that enables vision-language-action (VLA) models to perform 3D spatial reasoning implicitly during action prediction.
4D Radar Perception Algorithms for Autonomous Driving: A Review
Xumin Wu, Jun Zhou, Jilin Mei et al.
Research on 4D millimeter-wave radar perception algorithms has flourished in recent years, extending from signal processing and object detection to semantic segmentation, motion estimation, occupancy prediction, and dynamic scene reconstruction.
A Balanced Data Diet: Addressing the Exploration Bottleneck in Mega-Scale RL for Robot Control
Octi Zhang, Mateo Guaman Castro, Patrick Yin et al.
General-purpose robots must perform a wide range of tasks from agile locomotion to dexterous manipulation.
A Browser-Native Digital Test Range for Benchmarking 4D Ocean-Glider Planning Algorithms
Edward Holmberg, Elias Ioup, Mahdi Abdelguerfi
Repeated in-situ evaluation of ocean-glider planners requires scarce vehicles, operators, deployment and recovery resources, and ocean conditions that cannot be reset for competing algorithms.