LTL on finite and process traces: complexity results and a practical reasoner.

*(English)*Zbl 06987101Summary: Linear temporal logic (LTL) is a modal logic where formulas are built over temporal operators relating events happening in different time instants. According to the standard semantics, LTL formulas are interpreted on traces spanning over an infinite timeline. However, applications related to the specification and verification of business processes have recently pointed out the need for defining and reasoning about a variant of LTL, which we name LTL\(_p\), whose semantics is defined over process traces, that is, over finite traces such that, at each time instant, precisely one propositional variable (standing for the execution of some given activity) evaluates true.

The paper investigates the theoretical underpinnings of LTL\(_p\) and of a related logic formalism, named LTL\(_f\), which had already attracted attention in the literature and where formulas have the same syntax as in LTL\(_p\) and are evaluated over finite traces, but without any constraint on the number of variables simultaneously evaluating true. The two formalisms are comparatively analyzed, by pointing out similarities and differences. In addition, a thorough complexity analysis has been conducted for reasoning problems about LTL\(_p\) and LTL\(_f\), by considering arbitrary formulas as well as classes of formulas defined in terms of restrictions on the temporal operators that are allowed. Finally, based on the theoretical findings of the paper, a practical reasoner specifically tailored for LTL\(_p\) and LTL\(_f\) has been developed by leveraging state-of-the-art SAT solvers. The behavior of the reasoner has been experimentally compared with other systems available in the literature.

The paper investigates the theoretical underpinnings of LTL\(_p\) and of a related logic formalism, named LTL\(_f\), which had already attracted attention in the literature and where formulas have the same syntax as in LTL\(_p\) and are evaluated over finite traces, but without any constraint on the number of variables simultaneously evaluating true. The two formalisms are comparatively analyzed, by pointing out similarities and differences. In addition, a thorough complexity analysis has been conducted for reasoning problems about LTL\(_p\) and LTL\(_f\), by considering arbitrary formulas as well as classes of formulas defined in terms of restrictions on the temporal operators that are allowed. Finally, based on the theoretical findings of the paper, a practical reasoner specifically tailored for LTL\(_p\) and LTL\(_f\) has been developed by leveraging state-of-the-art SAT solvers. The behavior of the reasoner has been experimentally compared with other systems available in the literature.