Nathanaël Fijalkow and Guillaume Lagarde
Video:
Link to the paper: here
Abstract: In this paper we initiate the study of the computational complexity of learning linear temporal logic (LTL) formulas from examples. We construct approximation algorithms for fragments of LTL and prove hardness results; in particular we obtain tight bounds for the fragment containing only the next operator and conjunctions, and prove NP-hardness results for many fragments
Any question or comment can be made using the comment section of the page below.
Thanks for your very clear talk. In the motivation you mention that learning DFAs from examples is hard and that perhaps learning a formula instead could circumvent that (and also give a more readable object). Would it then also make sense to learn a regular expression directly? Do you expect the same complexity as LTL?
Thanks for this very nice question!
I would say that regular expressions are harder to learn than LTL formulas, especially simple fragments of LTL as we consider in this work. One of the reason may be that LTL formulas reads words process words from left to right; this simple property implies that finding small LTL formulas can somehow be attacked with dynamic programming. Concretely: as shown in the paper, we can characterise the smallest LTL separating formula of the LTL(X, and) fragment, which is combinatorially way too difficult for regular expressions.