cs.SE · 2606.23720 Copy arXiv ID · Jun 18, 2026 Save A Unified Framework for Runtime Verification and Model-Based Diagnosis in LOLA Authors: Raik Hipler , Martin Leucker , Patrick Rodler
Organizations: University of Luebeck, Luebeck, Germany · University of Klagenfurt, Klagenfurt, Austria
Abstract We present an integrated framework that unifies runtime verification and model-based diagnosis within the stream specification language LOLA. By encoding system descriptions, component health states, and observations into a single stream-based formalism, the approach enables continuous, online fault localization directly alongside fault detection, without requiring separate toolchains. The framework supports both time-invariant and transient faults, and naturally accommodates nondeterministic observations.
Explore similar work Sep 15, 2026 · Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro Linear Temporal Logics Runtime Enforcement
Jun 3, 2026 · Yile Gu, Zhen Zhang, Shaowei Zhu +4 Errors
Aug 9, 2026 · Wenyao Cui, Huaping Zhang, Yongyi Huang +6 Large Language Model Reasoning Neuro-Symbolic Framework
Sep 15, 2026 · cs.RO J/K move · Enter open · S save
Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro
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.