# A Unified Framework for Runtime Verification and Model-Based Diagnosis in LOLA

arXiv: https://arxiv.org/abs/2606.23720 · HTML: https://mlsanity.com/paper/2606.23720/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 39 references that are in the map.
- First posted on arXiv 18 Jun 2026.

## Builds on (most cited first, 4 of 4)

- [Interactive Debugging of Knowledge Bases](https://mlsanity.com/paper/1605.05950/) (2016)
- [DynamicHS: Streamlining Reiter's Hitting-Set Tree for Sequential Diagnosis](https://mlsanity.com/paper/2012.11078/) (2020)
- [How should I compute my candidates? A taxonomy and classification of diagnosis computation algorithms](https://mlsanity.com/paper/2207.12583/) (2022)
- [Symbolic Runtime Verification for Monitoring under Uncertainties and Assumptions](https://mlsanity.com/paper/2207.05678/) (2022)

## Abstract (arXiv)

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.