💻 computer science

Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification

This paper introduces Predictive Varanus, a two-stage runtime verification pipeline that combines CSP-based conformance monitoring with predictive LTL analysis to enable earlier detection of safety violations in autonomous systems by leveraging existing design-time models.

Original authors: Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro

Published 2026-09-17

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Autonomous robots, from the rovers exploring Mars to the drones delivering packages, operate in a world that is never fully predictable. Even the most carefully designed machine can encounter a sensor glitch, an unexpected obstacle, or a situation the engineers never imagined. To keep these systems safe, scientists use a technique called runtime verification. Think of it as a vigilant co-pilot that watches the robot's every move in real time, checking its actions against a set of rules written before the mission began. If the robot tries to do something forbidden, the co-pilot sounds an alarm. However, this traditional approach has a critical flaw: it is reactive. It only raises the alarm after the bad event has already happened. In high-stakes environments, such as a nuclear facility or a deep-space mission, waiting for a mistake to occur before reacting can be too late. The goal for researchers is to build a system that doesn't just watch for errors, but anticipates them, predicting a failure before the robot even takes the first step toward it.

This is the challenge tackled by a team of researchers who have developed a new monitoring system called Predictive Varanus. The system is designed for autonomous robots, specifically tested on a simulated rover tasked with inspecting a nuclear waste store. The researchers combined two existing technologies to create a pipeline that is both strict about what the robot is allowed to do and smart enough to foresee what will happen next. The first part of the system acts as a gatekeeper. It uses a detailed map of the robot's intended behavior, written in a formal language called Communicating Sequential Processes, to check every single event the robot performs. If the robot tries to move to a location it wasn't supposed to visit, or ignores a safety command, the gatekeeper immediately rejects that action as invalid. This ensures the robot stays within the boundaries of its design.

The second part of the system is where the prediction happens. Once the gatekeeper confirms that the robot's current actions are valid, the system looks ahead. It asks a simple but powerful question: given that the robot is behaving correctly right now, what are the only possible futures it can take? By analyzing the remaining paths allowed by the robot's design map, the system can determine if a specific outcome is now inevitable. It does not guess at random possibilities; it only considers the futures that are consistent with the robot's own rules. If the robot has encountered a high radiation level, the system knows that the only allowed future path is to turn back and abort the mission. Therefore, even before the robot actually turns around, the system can predict with certainty that the mission will fail. Similarly, if the robot has successfully visited all its required checkpoints, the system can predict that the mission will succeed, even if the robot still has a few more moves to make before it officially stops.

The researchers tested this approach on their nuclear-inspection rover, which was programmed to visit five different waypoints and check radiation levels. The levels were categorized as green, orange, or red. If the rover saw orange or red, the rules dictated it must return to the start and abort. In standard monitoring, the system would only know the mission was doomed after the rover actually turned back. With Predictive Varanus, the system could declare the mission a failure two events before the rover even began its return journey. In other scenarios, it could predict a successful completion eight events before the rover finished its final task. This early warning gives human operators or the robot's own control software valuable time to react, perhaps by re-planning a route or preparing for a safe shutdown, rather than simply watching a failure unfold.

The study also measured how much computing power this extra layer of thinking required. The gatekeeping part of the system remained very fast, taking less than a millisecond per event even as the robot's behavior map grew larger. The predictive part, which does the heavy lifting of looking ahead, took more time, especially as the robot's possible behaviors became more complex. For a model with 200 different states, the predictive check took about 700 milliseconds per event. While this is slower, the researchers found that the benefit of knowing the outcome early was worth the cost in many situations. The system successfully identified inevitable failures and inevitable successes in scenarios where the robot was still following the rules, proving that it is possible to look into the future without breaking the laws of the present.

What makes this work significant is not just that it predicts the future, but how it does so. It does not rely on a separate, abstract model for prediction. Instead, it reuses the exact same design map that was used to verify the robot's behavior in the first place. This means the system is not making assumptions about how the robot might behave; it is strictly following the logic the engineers already built into the machine. The researchers showed that by combining a strict check for current validity with a forward-looking check for future inevitability, they could provide earlier, more useful verdicts than standard monitoring. The system does not predict random failures or sensor glitches that were never modeled; it predicts the logical consequences of the robot's own design. In the complex, uncertain world of autonomous robotics, this ability to see the inevitable outcome of a correct path offers a new kind of safety, turning a reactive alarm into a proactive guide.

Technical Summary: Predictive Varanus

Problem Statement
Runtime Verification (RV) is a critical technique for autonomous and robotic systems, offering online assurance by checking observed execution traces against formal specifications without requiring access to source code or internal states. However, standard RV is inherently reactive; it can only detect violations after a bad event has already occurred. In safety-critical domains where failures are costly, this latency is insufficient. While Predictive Runtime Verification (PRV) addresses this by analyzing possible future continuations to determine inevitable satisfaction or violation of properties, existing approaches often rely on models that are distinct from the system's design-time specifications. Furthermore, standard PRV does not inherently distinguish between a system behaving according to its model but violating a temporal property, versus a system behaving in a way that is entirely unmodelled (out-of-spec).

Methodology
The paper presents PREDICTIVE VARANUS, a two-stage verification pipeline that integrates the existing VARANUS tool with Predictive Runtime Verification for Linear-time Temporal Logic (LTL). The core innovation is the reuse of a single design-time Communicating Sequential Processes (CSP) model for both conformance checking and predictive reasoning.

The pipeline operates as follows:

CSP Conformance Gate (VARANUS): The system under analysis (SUA) emits an event trace. The first stage uses a CSP model as a deterministic oracle. VARANUS checks if the current trace is a valid prefix of the CSP model's language. If an event is not permitted by the model, the trace is immediately rejected (rej). This ensures that predictive reasoning is only applied to behavior that is consistent with the system's design.
Model Translation: For traces that pass the conformance gate, the CSP model is translated into a Büchi automaton (in Hanoi Omega-Automata format). This translation involves:
- Extracting the Labelled Transition System (LTS) from the CSP process.
- Mapping CSP events to atomic propositions.
- Adding skip self-loops to terminal states to convert finite traces into infinite words, enabling standard LTL semantics.
Predictive LTL Monitoring: The predictive monitor uses the translated Büchi automaton to constrain the set of admissible futures. Given an LTL property $\phi$ $ϕ$ , the monitor computes the synchronous products of the CSP-derived automaton with the automata for $\phi$ $ϕ$ and $\neg\phi$ $\neg ϕ$ .
- If all model-consistent continuations satisfy $\phi$ , the verdict is conclusive satisfaction ( $\top$ ).
- If all model-consistent continuations violate $\phi$ , the verdict is conclusive violation ( $\bot$ ).
- If both outcomes remain possible, the verdict is inconclusive ( $?$ ).
- If the trace was rejected by VARANUS, the verdict is rej.

Key Contributions

Integrated Pipeline: The paper defines a formal two-stage pipeline that combines CSP-based conformance monitoring with predictive LTL verification.
Model Reuse: It demonstrates how a single CSP model, typically used for design-time analysis (e.g., with FDR or RoboChart), can serve dual purposes: as a runtime oracle for conformance and as the source of admissible futures for prediction.
Formal Semantics: The authors provide formal definitions for the combined verdict function, distinguishing between rej (model non-conformance) and predictive $\bot$ (inevitable violation within the model).
Implementation and Translation: The work details the construction of the propositional $\omega$ -automaton from CSP processes, enabling the use of standard LTL tooling (like Spot) while preserving the structural constraints of the CSP model.

Results
The approach was evaluated using a robotic rover case study for nuclear store inspection and synthetic stress tests.

Rover Case Study: The system monitored properties regarding mission completion, coverage, and abort conditions.
- In scenarios where hazardous radiation was detected, the system predicted mission failure (violation of completion/coverage) and the inevitability of an abort 1 to 2 events earlier than the actual abort event would occur in the trace.
- For nominal missions, the coverage property was predicted as satisfied 8 events before the mission completion event.
- Invalid traces (e.g., continuing after a hazard) were rejected immediately by VARANUS, with no predictive gain, confirming the system correctly handles out-of-model behavior.
- Runtime overhead was modest for the rover (approx. 1.84 ms/event total), with the CSP check taking 0.19 ms and the predictive monitor 1.64 ms.
Synthetic Stress Tests:
- Scalability: The CSP conformance check remained lightweight (<1 ms/event) even as model size increased. However, the predictive monitor's cost scaled significantly with model size (from ~0.2 ms/event at 10 states to ~700 ms/event at 200 states), identifying automata construction and maintenance as the primary bottleneck.
- Anticipation Gain: In decision-tail benchmarks, the anticipation gain (the number of events saved by prediction) grew linearly with the length of the forced tail after a commitment point. For a tail length of 20, the system provided a verdict 21 events earlier than a reactive monitor.

Significance and Claims
The paper claims that PREDICTIVE VARANUS offers a practical method for achieving earlier verdicts in runtime verification by leveraging existing design-time CSP models. Its significance lies in:

Differentiation of Failure Modes: It clearly separates "out-of-model" behavior (detected by VARANUS) from "inevitable property violation" within the model (detected by PRV).
Operational Utility: The case study demonstrates that predictive verdicts can be generated early enough to be useful for human operators or re-planning algorithms, specifically by identifying inevitable mission aborts or failures before they physically manifest.
Modularity: The pipeline is modular; while the current implementation uses LTL, the structure allows for other predictive reasoning techniques to be integrated without altering the CSP conformance layer.

The authors acknowledge that the current implementation faces scalability challenges regarding the predictive component for large models, suggesting that future work could focus on optimizing the automata backend or exploring symbolic representations. They do not claim to solve the general problem of predicting unmodelled physical failures, but rather to anticipate outcomes that are forced by the system's own design model.

More like this