PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro

arXiv:2609.17625v1cs.RO

TL;DR

Because reactive runtime monitors report violations only after bad events, PREDICTIVE VARANUS combines CSP conformance checking with predictive LTL over CSP-admitted futures. Rover experiments report earlier operational verdicts, while synthetic benchmarks expose higher predictive overhead on larger models.

  • Problem

    Standard Runtime Verification is reactive, so violations are reported only after the relevant event has occurred.

    Source: §I · p. 1

  • Method

    PREDICTIVE VARANUS uses VARANUS as a CSP conformance gate and applies predictive LTL monitoring to futures admitted by the CSP model.

    Source: §I · p. 1, §III · p. 2

  • Results

    Eight events before mission completion, the rover monitor concludes coverage; after hazardous radiation, it detects completion and coverage failure two events before abort.

    Source: 4) Discussion · p. 6

  • Takeaways & Limitations

    The experiments show that PREDICTIVE VARANUS preserves VARANUS’s conformance guarantees while adding useful predictive verdicts.

    Source: 4) Discussion · p. 7

    The predictive component is the main scalability bottleneck, with higher overhead on larger models.

    Source: 4) Discussion · pp. 6–7

Abstract

from arXiv · show

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. In this way, out-of-model behaviour is rejected immediately, while model-consistent prefixes can be classified as already guaranteeing satisfaction, already forcing violation, or still being inconclusive for the monitored temporal property. We formalise the combined monitor, explain its implementation, and illustrate the approach on a robotic rover for nuclear-store inspection. The case study shows how the combination of CSP validation and predictive LTL can provide earlier verdicts than standard runtime monitoring while reusing an existing design-time CSP model.

I. INTRODUCTION

The introduction motivates predictive monitoring as a complement to reactive Runtime Verification, then presents PREDICTIVE VARANUS as a CSP conformance gate combined with predictive LTL. The CSP model also provides the trace semantics used to check observed events.

I. INTRODUCTION

  • Standard Runtime Verification is reactive, reporting violations only after the relevant event unless paired with enforcement or mitigation.Predictive Runtime Verification examines model-allowed continuations to identify outcomes that are already inevitable.Source: §I · p. 1
  • VARANUS uses a CSP model as its oracle and can reuse an existing design-time model, but it detects misbehaviour only after an invalid event.The model is assumed to represent correct behaviour deterministically.Source: §I · p. 1
  • PREDICTIVE VARANUS rejects events that violate the CSP model and predicts inevitable LTL satisfaction or violation for model-conformant traces.The pipeline uses the CSP model both as VARANUS’s conformance oracle and as the source of futures for predictive reasoning.Source: §I · p. 1

A. CSP and VARANUS

  • CSP represents systems as processes whose finite event traces can be compared with the SUA’s observed execution.VARANUS uses the model’s LTS representation; in this pipeline, only events consistent with the CSP model pass to predictive monitoring.Source: A. CSP and VARANUS · p. 2
  • A trace admitted by the CSP model is checked predictively; a rejected trace has performed an invalid event and does not need predictive checking.CSP trace semantics are prefix-closed, so an admitted observed prefix remains compatible with the specification.Source: A. CSP and VARANUS · p. 2

B. Predictive Runtime Verification for LTL

Predictive Runtime Verification evaluates whether the futures permitted by a model force an LTL property to hold or fail. This paper uses three verdicts, merging two intermediate outcomes into inconclusive.

B. Predictive Runtime Verification for LTL

  • A finite prefix is conclusive when every model-allowed continuation satisfies the LTL property or every continuation violates it; otherwise, the verdict is inconclusive.The predictive verdict depends on the system model’s allowed futures, not only on whether the observed prefix itself satisfies or violates the property.Source: B. Predictive Runtime Verification for… · p. 2
  • The adopted semantics returns conclusive satisfaction (⊤), conclusive violation (⊥), or inconclusive (?).The paper merges “possibly true” and “possibly false” into one inconclusive verdict because VARANUS rejects invalid prefixes.Source: B. Predictive Runtime Verification for… · p. 2
  • To apply standard LTL semantics, the finite trace is extended with an infinite suffix of skip propositions after termination.Events produced by the SUA satisfy ¬skip, while the post-termination suffix consists of skip.Source: B. Predictive Runtime Verification for… · p. 2

III. PREDICTIVE VARANUS

PREDICTIVE VARANUS checks each observed event against the CSP model before predictive LTL monitoring. It translates that model into an automaton whose admitted futures constrain the monitor’s predictions.

III. PREDICTIVE VARANUS

  • Each event first passes VARANUS’s CSP validity check; accepted events are projected to propositions for predictive monitoring over the CSP-derived B¨uchi automaton.The predictive component therefore does not reason about futures for events already rejected by VARANUS.Source: §III · p. 2, Figure 1 · p. 3

A. From CSP to a proposition-based model

  • The CSP-to-proposition construction targets predictive LTL over model-admitted futures, rather than safety monitoring of traces and refusals.The projection also reuses automata-based LTL tooling without changing the CSP model and separates event validation from prediction.Source: A. From CSP to a proposition-based model · pp. 2, 4
  • The construction derives a finite transition system from the finite-state CSP process and uses it to build an ω-automaton in HOA format.In the implementation, FDR supplies the reachable transition system, which VARANUS materialises explicitly for runtime use.Source: A. From CSP to a proposition-based model · pp. 2–3
  • The automaton adds a skip self-loop to each terminal state, turning maximal finite CSP executions into infinite words for standard LTL semantics.Every state is accepting under the stated terminal-stuttering convention.Source: A. From CSP to a proposition-based model · p. 3
  • Each structured CSP event maps to its own atomic proposition, preserving distinctions such as move.0 and move.1 while abstracting their parameterised event structure.VARANUS validates the original structured event; the predictive monitor consumes its propositional encoding.Source: A. From CSP to a proposition-based model · pp. 3–4

B. Predictive monitoring construction

The predictive monitor combines CSP-admitted futures with automata for an LTL property and its negation. Emptiness of the corresponding continuation languages determines whether satisfaction, violation, or neither is conclusive.

B. Predictive monitoring construction

  • The reachable states in the two products represent model-consistent futures that still admit satisfaction or violation, respectively.The monitor computes those state sets after reading the projected observed trace.Source: B. Predictive monitoring construction · p. 4
  • The verdict rule checks whether any accepting continuation remains in the product automata for φ and ¬φ; it is standard PRV integrated with CSP-derived futures.An empty φ-product language means violation is inevitable, while an empty ¬φ-product language means satisfaction is inevitable; otherwise the verdict is inconclusive.Source: B. Predictive monitoring construction · p. 4
  • The verdict criterion follows standard automata-theoretic PRV; the paper’s integration extracts admissible futures from CSP and validates the observed execution online.The paper identifies integration with the CSP behavioural model—not a new predictive verdict rule—as its contribution.Source: B. Predictive monitoring construction · p. 4

C. Combined semantics

PREDICTIVE VARANUS runs CSP conformance checking before predictive LTL monitoring. Rejected traces indicate departure from the CSP model, whereas LTL verdicts concern only traces that remain model-conformant.

C. Combined semantics

  • The pipeline sequentially composes a CSP conformance check with a predictive LTL monitor.The combined monitor returns rejection when the CSP check rejects; otherwise it returns the predictive LTL monitor’s verdict.Source: C. Combined semantics · p. 4
  • A rejection means the trace left CSP-admitted behaviour, not that the monitored LTL property was violated.Predictive violation applies to a trace that remains model-conformant, where remaining model-consistent futures force the outcome.Source: C. Combined semantics · p. 4

IV. CASE STUDY

The case study reuses a CSP model of a rover inspecting radiation at waypoints in a simulated nuclear waste store. Predictive LTL checks whether mission completion, abort, and coverage properties have become inevitable or impossible along model-consistent traces.

IV. CASE STUDY

  • The study reuses a CSP model of a rover inspecting radiation at waypoints in a simulated nuclear waste store.Green readings allow the mission to continue; Orange or Red readings mean the rover should return to the entry point and abort.Source: §IV · p. 4
  • The monitored properties cover successful mission completion, eventual abortion after hazardous radiation, and inspection of all five nominal-case waypoints.The passage defines propositions for mission completion, mission abort, radiation levels, and waypoint moves.Source: §IV · pp. 4–5
  • After hazardous radiation, completion can become predictively false before abort occurs because every model-consistent continuation returns to the entry point and aborts.Successful mission completion is then no longer compatible with the model.Source: §IV · p. 4
  • For hazardous radiation, the abort property can become predictively true before the mission-abort event is observed because every model-consistent future contains that event.While readings remain Green, the coverage property is inconclusive; after hazardous radiation with unvisited waypoints, it becomes predictively false if the rover obeys the model.Source: §IV · pp. 4–5
  • The CSP model constrains predictive reasoning to compatible continuations rather than every event combination the rover could perform.The same model is used both to recognize bad events and to predict future events.Source: §IV · p. 5

V. EVALUATION

The evaluation combines a rover mission study with a controlled stress test on synthetic CSP models. It measures prediction’s incremental cost over CSP validation and its timing benefit relative to when the same conclusion would otherwise become explicit.

V. EVALUATION

  • The evaluation uses the rover mission to validate verdicts and quantify practical benefit, then stress-tests computational overhead and scalability on synthetic CSP models.The stress test varies model size, branching structure, and termination depth.Source: §V · p. 5
  • Because VARANUS and PREDICTIVE VARANUS perform different monitoring tasks, the evaluation does not compare them directly.Instead, it measures prediction’s incremental cost on top of CSP validation and its benefit as the difference between predictive and later explicit verdict positions.Source: §V · p. 5

A. Rover Evaluation

The rover evaluation examines invalid traces and conformant traces whose LTL properties become predictively false or true. CSP conformance rejection occurs at the first illegal event, while prediction anticipates inevitable outcomes on conformant prefixes.

A. Rover Evaluation

1) Qualitative Measures:

  • The evaluation’s table identifies Pred. pos. as the first conclusive predictive verdict and Ref. pos. as the later position where the same conclusion happens.Compare these positions to assess how early the predictive verdict arrives.Source: Table I · p. 5
  • VARANUS rejects CSP-invalid traces at the first illegal event, preserving the original conformance semantics.Examples include continuing after hazardous radiation or moving to a waypoint the rover was not told to inspect.Source: 1) Qualitative Measures · p. 5
  • On conformant traces, hazardous radiation can make mission completion and coverage predictively false before the mission-abort event, assuming the rover obeys the model.These are properties that have become unreachable while the trace remains model-conformant.Source: 1) Qualitative Measures · p. 5
  • On conformant traces, hazardous radiation can make the abort property predictively true before abort occurs, while inspecting all waypoints can make coverage predictively true before mission completion.Both verdicts concern outcomes that have become inevitable under the model.Source: 1) Qualitative Measures · p. 5

2) Quantitative measures:

Across the rover runs, PREDICTIVE VARANUS reaches several conclusive verdicts before the corresponding outcome becomes explicit, while invalid traces are rejected without prediction gain. The evaluation also measures runtime overhead and describes synthetic tests of cost scaling and predictive benefit.

2) Quantitative measures:

  • Eight events of gain for φcover on the nominal trace; after hazardous radiation, φcomplete and φcover become false two events before abort, while φabort becomes true one event earlier.Invalid traces show zero gain because VARANUS rejects them at the first illegal action.Source: 2) Quantitative measures · pp. 5–6
  • 1.84 ms/event is the overall monitoring time across 27 runs, comprising 0.19 ms/event for VARANUS and 1.64 ms/event for the predictive monitor.Average per-property costs are 0.32 ms/event for φcomplete, 0.35 ms/event for φabort, and 4.84 ms/event for φcover.Source: 2) Quantitative measures · p. 6

B. Stress-Test Evaluation

  • The synthetic stress test varies dense CSP model size to measure runtime scaling and uses branching prefixes followed by forced tails to measure predictive benefit.The setup defines N as the generated model's state count and L as trace length; its decision-tail parameters are branching factor B, depth D, and forced-tail length T.Source: B. Stress-Test Evaluation · p. 6, 1) Experimental setup · p. 6

2) Cost Metrics:

The dense-model benchmark shows predictive monitoring, rather than CSP validation, drives the prototype's scaling costs; decision-tail tests show that anticipation grows with the forced future remaining after commitment. The discussion frames these costs alongside earlier rover verdicts and the modularity of the predictive stage.

2) Cost Metrics:

  • 702–757 ms/event for predictive monitoring at N = 200, compared with CSP validation below 1 ms/event, makes the predictive component the main online cost as models grow.Predictive cost rises from about 0.2 ms/event at N = 10 to about 7.6 ms/event at N = 50 and 65 ms/event at N = 100; per-event costs remain fairly stable across trace lengths.Source: 2) Cost Metrics · p. 6, Table II · p. 7
  • About 390–397 s of one-off preprocessing at N = 200 makes automata construction and maintenance the main scalability bottleneck of the current implementation.Preprocessing grows from about 95 ms at N = 10, to about 1.8 s at N = 50, and about 25 s at N = 100.Source: 2) Cost Metrics · p. 6, Table II · p. 7

3) Prediction Metrics:

  • Anticipation gain increases with forced-tail length T: 2 events for T = 1, 6 for T = 5, 11 for T = 10, and 21 for T = 20.Across 96 configurations, branching factor, property polarity, and trace class do not affect measured gain; depth shifts predictive and reference latencies by the same constant offset.Source: 3) Prediction Metrics · p. 6, Table III · p. 7

4) Discussion:

  • The rover case study yields useful early verdicts on CSP-conformant traces, while the decision-tail tests return a verdict at commitment and gain more anticipation with longer forced tails.The predictive monitor's high cost is a limitation of the current implementation, not the pipeline; the predictive component could use a faster automata backend, symbolic representation, or different logic.Source: 4) Discussion · pp. 6–7

VI. RELATED WORK

PREDICTIVE VARANUS combines CSP-based runtime conformance monitoring with predictive LTL reasoning, reusing one CSP model for both observed traces and admissible futures. Its conclusion reports earlier verdicts in the rover case study and identifies efficiency and broader system settings as future-work areas.

VI. RELATED WORK

  • Unlike work focused on monitoring infrastructure, safe control, or temporal-logic controller synthesis, this approach predicts outcomes while monitoring executions admitted by a CSP model.The paper describes its contribution as complementary to temporal-logic planning and synthesis for robotics.Source: §VI · p. 7
  • PREDICTIVE VARANUS reuses the same CSP model as VARANUS's conformance oracle and as the source of futures for predictive LTL monitoring.The paper positions this combination between model-based predictive runtime verification and CSP-based runtime monitoring.Source: §VI · p. 7

VII. CONCLUSIONS

  • The conclusion reports earlier verdicts for mission completion, coverage, and abort in the rover case study, with predictive overhead growing as model size increases.Future work includes improving predictive efficiency, enabling mitigation or enforcement from negative verdicts, exploring five-valued semantics, and extending to multi-component or multi-model robotic systems.Source: §VII · p. 8
Loading 2609.17625v1…