The Complexity of Learning Linear Temporal Formulas from Examples
This addresses the challenge of automated reasoning and verification in computer science, providing foundational insights into the complexity of learning temporal logic, though it is incremental as it builds on existing LTL frameworks.
The paper tackles the problem of learning linear temporal logic formulas from examples by analyzing computational complexity, constructing approximation algorithms for fragments, and proving tight bounds and NP-completeness results for specific fragments.
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 approximation of the fragment containing only the next operator and conjunctions, and prove NP-completeness results for many fragments.