Learning temporal formulas from examples is hard
This addresses the challenge of expressing comprehensible separating properties in formal verification or AI, but it is incremental as it focuses on computational complexity rather than practical solutions.
The paper tackled the problem of learning linear temporal logic (LTL) formulas from examples to separate positive and negative instances for human comprehension, and found that this problem is NP-complete for the full logic and most fragments.
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.