Learning temporal formulas from examples is hard
Corto Mascle Nathanaël Fijalkow Guillaume Lagarde
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. In this paper we
initiate the study of the computational complexity of the problem. Our main
results are hardness results: we show that the LTL learning problem is
NP-complete, both for the full logic and for almost all of its fragments. This
motivates the search for efficient heuristics, and highlights the complexity of
expressing separating properties in concise natural language.