Publikation
Counterfactual Explanations for MITL Violations
Bernd Finkbeiner; Felix Jahn; Julian Siber
In: Siddharth Barman; Slawomir Lasota (Hrsg.). 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS-2024), December 16-18, Pages 22:1-22:25, Leibniz International Proceedings in Informatics (LIPIcs), Vol. 323, ISBN 978-3-95977-355-3, Schloss Dagstuhl -- Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 12/2024.
Zusammenfassung
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.