Applications related to the specification and verification of business processes have recently pointed out the need of reasoning about a variant of LTL, named LTLf , where formulas are interpreted over finite traces. Satisfiability for LTL and LTLf is an intractable problem, formally PSPACE-complete. However, while several efforts have been spent in the literature to identify LTL fragments enjoying more favorable computational properties (such as NP-complete or even tractable classes of formulas), little was know so far about the complexity of fragments of LTLf .
We addressed this question by focusing on all possible LTLf fragments defined in terms of restrictions on the temporal operators and on the Boolean connectives being allowed. In addition, we studied another variant, again of interest in the above application domains, where exactly 1 distinct propositional variable must evaluate true at each time instant.
We developed a reasoner, called LTL2SAT, for LTLf and LTLf,s formulas, which we have implemented on the basis of our theoretical findings. For the classes on which satisfiability is feasible in polynomial time, LTL2SAT implements the algorithms we developed. For the other classes, LTL2SAT rewrites the input formula into an equivalent Boolean formula and uses minisat to compute a model.
LTL2SAT 