DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2024.22

Counterfactual Explanations for MITL Violations

Authors: Bernd Finkbeiner, Felix Jahn, and Julian Siber

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)

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.

Cite as

Bernd Finkbeiner, Felix Jahn, and Julian Siber. Counterfactual Explanations for MITL Violations. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 22:1-22:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:LIPIcs.FSTTCS.2024.22,
  author =	{Finkbeiner, Bernd and Jahn, Felix and Siber, Julian},
  title =	{{Counterfactual Explanations for MITL Violations}},
  booktitle =	{44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
  pages =	{22:1--22:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-355-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{323},
  editor =	{Barman, Siddharth and Lasota, S{\l}awomir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.22},
  URN =		{urn:nbn:de:0030-drops-222116},
  doi =		{10.4230/LIPIcs.FSTTCS.2024.22},
  annote =	{Keywords: Timed automata, actual causality, metric interval temporal logic}
}

Search Results

Documents authored by Siber, Julian

Counterfactual Explanations for MITL Violations

Abstract

Cite as

Thanks for your feedback!

Could not send message