[Submitted on 26 Dec 2023 (v1), last revised 9 Nov 2026 (this version, v2)]
Abstract:We study the problem of learning linear temporal logic (LTL) formulas from examples, as a first step towards expressing a property separating positive and negative instances in a way that is comprehensible for humans. Given positive and negative words, the goal is to find a smallest formula satisfied by the positive words and not by the negative ones. We study the computational complexity of this problem for all fragments of negation-free LTL built from the operators F (eventually), G (globally), X (next), $wedge$ (conjunction), and $vee$ (disjunction), without the until operator. We show that the problem is in NP for all fragments, that it is in polynomial time for the fragments containing none of the pairs ${X,wedge}$, ${X,vee}$, ${F,wedge}$ and ${G,vee}$, and that it is NP-complete for all other fragments, already for alphabets with two or three letters. We also show that the fragment with only X and $wedge$ has a polynomial time 3-approximation algorithm, but no polynomial time approximation scheme unless P = NP. These results motivate the search for efficient heuristics.
Submission history
From: Nathanaël Fijalkow [view email]
[v1] Tue, 26 Dec 2023 21:16:19 UTC (43 KB)
[v2] Mon, 9 Nov 2026 09:45:24 UTC (56 KB)
