Counterfactual Explanations for MITL Violations

TL;DR

This paper introduces an automatic explanation method for MITL violations in timed automata networks, leveraging counterfactual causality to identify root causes, thereby reducing manual effort in diagnosing real-time system failures.

Contribution

It develops a novel counterfactual causality-based approach tailored for timed automata networks to explain MITL violations automatically.

Findings

Effective on multiple benchmark cases

Reduces manual effort in root cause analysis

Demonstrates practical applicability with a prototype

Abstract

MITL is a temporal logic that facilitates the verification of real-time systems by expressing the critical timing constraints placed on these systems. MITL specifications can be checked against system models expressed as networks of timed automata. A violation of an MITL specification is then witnessed by a timed trace of the network, i.e., an execution consisting of both discrete actions and real-valued delays between these actions. Finding and fixing the root cause of such a violation requires significant manual effort since both discrete actions and real-time delays have to be considered. In this paper, we present an automatic explanation method that eases this process by computing the root causes for the violation of an MITL specification on the execution of a network of timed automata. This method is based on newly developed definitions of counterfactual causality tailored to networks of timed automata in the style of Halpern and Pearl's actual causality. We present and evaluate a prototype implementation that demonstrates the efficacy of our method on several benchmarks from the literature.