Formal Explanations for Linear Temporal Logic over Finite Traces

Valeria Fionda; Antonio Ielo; Francesco Ricca

cs.LOOct 26, 2026

Formal Explanations for Linear Temporal Logic over Finite Traces

Authors: Valeria Fionda, Antonio Ielo, Francesco Ricca

Organizations: University of Calabria, Italy

Abstract

Linear Temporal Logic over Finite Traces (LTLf) is widely used in Artificial Intelligence to specify desired temporal behavior and determine whether finite traces satisfy or violate it. Explaining these outcomes is essential for debugging and trust. However, existing approaches typically capture either sufficient reasons or counterfactual causes, without clarifying their relationship. We introduce a native characterization of abductive (AXps) and contrastive (CXps) explanations directly over finite traces, based on locking and unlocking time-indexed events. We prove its equivalence to the classifier-based formulation, and show that CXps coincide with a recently proposed temporal causality semantics for LTLf. This characterization enables an efficient implementation based on the enumeration of minimal unsatisfiable cores and minimal correction sets of ASP programs. Experiments on real-world event logs demonstrate the effectiveness of the approach.

Figures & tables

Figure 1: AXps (sufficient reasons) and CXps (minimal outcome-flipping interventions) for $\varphi$ on a compliant trace $\pi_{1}$ and a violating trace $\pi_{2}$ . Sets are listed state by state; e.g. $\{\},\{low\}$ denotes $\{low_{1}\}$ .

Per-instance counts
	$N$		AXp										CXp
			Complete					Timeout					Complete					Timeout
Log	C	T	Min	P25	P50	P75	Max	Min	P25	P50	P75	Max	Min	P25	P50	P75	Max	Min	P25	P50	P75	Max
bpi2020-domdecl	81	8	1	10	21	82	441	567	578	588	647	834	1	1	3	5	19	18	23	28	35	70
bpi2020-intdecl	181	552	6	54	83	193	621	81	186	249	344	784	4	19	38	62	220	0	9	38	91	908
bpi2020-permlog	312	1166	4	40	177	443	1087	80	294	426	597	1253	2	15	51	143	366	0	9	70	223	885

Table 1: Per-instance AXp/CXp counts (top) and AXp/CXp explanation sizes in literals (bottom), by log.

N

: instances (C=complete, T=timeout). Column

Px

refers to the

x

-th quantile of the distributions, with P50 being the median. Max., min. refers to the maximum and minimum observed statistics.

Figure 2: Time to the first and to all CXps on

P(N)

\tau_{N}

, for caupybara , our full approach, and a CXp-only variant. Dashed: first CXp; solid: all CXps. 10 seconds timeout.

Counterfactual Explanations

Counterfactual explanations show how changing an input could alter a model’s prediction, supporting model understanding, auditing, and actionable recourse.

See all 117 papers

Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+
Aug 3, 2026Christoph Weinhuber, Maximilian Prokop, Giuseppe De Giacomo +1Temporal Reasoning Formal Verification
University of Oxford · 2Technical University of Munich · 3Masaryk University Brno +1
Learning Linear Temporal Specifications from Demonstrations with Uncertainty
Jul 12, 2026Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oesFormal Verification Learning from Demonstration
School of Electrical Engineering and Computer Science at The Pennsylvania State University, State College, USA
Truth as a Trajectory: What Internal Representations Reveal About Large Language Model Reasoning
Mar 1, 2026Hamed Damirchi, Ignacio Meza De la Jara, Ehsan Abbasnejad +3LLM Interpretability Representation Geometry in Language Models
Australian Institute for Machine Learning, Adelaide University · Monash University · Concordia University

Aug 3, 2026J/K move · Enter open · S save

Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+

Christoph Weinhuber, Maximilian Prokop, Giuseppe De Giacomo, Moshe Y. Vardi

University of Oxford · 2Technical University of Munich · 3Masaryk University Brno+1

Temporal Reasoning Formal Verification Linear Temporal Logic Temporal Logic

Open paper AskPDF arXiv

Linear Temporal Logic (LTL) is one of the most widely adopted languages for specifying temporal extended objectives in AI, with applications ranging from reactive synthesis to stochastic planning in Markov decision processes and reinforcement learning. Traditionally, solving any of these problems requires translating the LTL specification to a nondeterministic automata on infinite words and then determinizing it, a step that is notoriously difficult in theory and in practice. Recent work has introduced LTLf+, which lifts the finite-trace logic LTLf to infinite traces. LTLf+ has the same expressive power as LTL, yet it retains most of the crucial advantages of its base logic LTLf. Most reasoning in LTLf+ rests on finite automata on finite words, for which we have not only a canonical minimal representation but also an efficient determinization procedure. In this work we present the first translation from LTL to LTLf+. We first normalize an LTL formula into the syntactic reactivity fragment of the Manna-Pnueli hierarchy, to create the general fragment-based shape of LTLf+. We then present linear translations for each individual component of that fragment. As a consequence of this translation, the expanding body of techniques developed for LTLf+ now becomes available to many AI problems currently formulated in LTL. We further show that this comes at no asymptotic cost, as the pipeline from LTL to automaton via LTLf+ remains doubly exponential.

Abstract

Counterfactual Explanations

Explore similar work

Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+

Learning Linear Temporal Specifications from Demonstrations with Uncertainty

Truth as a Trajectory: What Internal Representations Reveal About Large Language Model Reasoning