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.

翻译：我们研究了从示例中学习线性时序逻辑（LTL）公式的问题，这是朝着以人类可理解的方式表达区分正例和反例的性质所迈出的第一步。本文首次对该问题的计算复杂度进行了研究。我们的主要结果为难度结论：我们证明LTL学习问题是NP完全的，无论是针对完整逻辑还是其几乎所有子片段。这一结果推动了对高效启发式算法的探索，并凸显了以简洁自然语言表达区分性质的复杂性。