Causality for General LTL-definable Properties

Georgiana Caltais
(University of Konstanz)
Sophie Linnea Guetlein
(University of Konstanz)
Stefan Leue
(University of Konstanz)

In this paper we provide a notion of causality for the violation of general Linear Temporal Logic (LTL) properties. The current work is a natural extension of the previously proposed approach handling causality in the context of LTL-definable safety properties. The major difference is that now, counterexamples of general LTL properties are not merely finite traces, but infinite lasso-shaped traces. We analyze such infinite counterexamples and identify the relevant ordered occurrences of causal events, obtained by unfolding the looping part of the lasso shaped counterexample sufficiently many times. The focus is on LTL properties from practical considerations: the current results are to be implemented in QuantUM, a tool for causality checking, that exploits explicit state LTL model checking.

In Bernd Finkbeiner and Samantha Kleinberg: Proceedings 3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology (CREST 2018), Thessaloniki, Greece, 21st April 2018, Electronic Proceedings in Theoretical Computer Science 286, pp. 1–15.
Published: 3rd January 2019.

ArXived at: https://dx.doi.org/10.4204/EPTCS.286.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org