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.

翻译：暂无翻译