# Causality for General LTL-definable Properties

## TL;DR

This paper extends causality analysis to infinite counterexamples in LTL properties, enabling better understanding of violations in complex temporal logic specifications.

## Contribution

It introduces a causality notion for infinite LTL counterexamples, building on previous finite-trace approaches, and aims for implementation in a causality checking tool.

## Key findings

- Causality for infinite LTL counterexamples is characterized.
- Loop unfolding in lasso-shaped traces reveals causal event sequences.
- Framework is designed for integration with LTL model checking tools.

## Abstract

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.