Diagnosis of Runtime Property Violations

Runtime verification checks, during execution, whether a system satisfies a given property. When a violation is detected, identifying the underlying causes is essential for fault recovery. However, existing approaches to model-based diagnosis do not fully address this problem. Model-Based Diagnosis (MBD) explains deviations between observed and nominal behaviors, but does not target property violations specifically. Model-Based Safety Analysis (MBSA), on the other hand, explains possible causes of a top-level event, but does not exploit runtime observations. In this work, we address the Property Violation Diagnosis (PVD) problem, which lies at the intersection of runtime verification and model-based diagnosis: given a system description, a monitored property, and a set of observations that indicate its violation, we aim to compute the set of faults that are relevant to explain the violation. We provide a formal characterization of PVD in propositional logic and propose symbolic algorithms for generating the relevant diagnoses. Our experimental evaluation demonstrates the applicability of the proposed approach.