Metraipolis › archive › dc_f9b00a708482

Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification — arXiv:2609.17625

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.17625
License (as archived): CC0-1.0
Archived: 2026-10-15T16:55:34.018Z
SHA-256 of the archived text: d42c0ced21940dd42e776b5427282402e1c4433467ca36efbbfb3f89d806006f
Stable URL of this page: https://metraipolis.com/documento/dc_f9b00a708482

How to cite

Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification — arXiv:2609.17625 — arXiv (en), https://arxiv.org/abs/2609.17625 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_f9b00a708482 (Metraipolis archive dc_f9b00a708482, sha256 d42c0ced21940dd42e776b5427282402e1c4433467ca36efbbfb3f89d806006f)

BibTeX

@misc{dcf9b00a708482,
  title = {Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification — arXiv:2609.17625},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.17625},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_f9b00a708482; sha256 d42c0ced21940dd42e776b5427282402e1c4433467ca36efbbfb3f89d806006f},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.17625. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: statistica e scienza dei dati (retro-catalogo arXiv: annunci del 2026-09-17 in cs.RO).
Categorie arXiv: Robotics (cs.RO).
Pagina del lavoro: https://arxiv.org/abs/2609.17625 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-15T16:13:27.225Z dalla pagina https://arxiv.org/catchup/cs.RO/2026-09-17?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).