LTL on Weighted Finite Traces: Formal Foundations and Algorithms
Abstract
LTL on finite traces (LTLf ) is a logic that attracted much attention in recent literature, for its ability to formalize the qualitative behavior of dynamical systems in several application domains. However, its practical usage is still rather limited, as LTLf cannot deal with any quantitative aspect, such as with the costs of realizing some desired behaviour. The paper fills the gap by proposing a weighting framework for LTLf encoding such quantitative aspects in the traces over which it is evaluated. The complexity of reasoning problems on weighted traces is analyzed and compared to that of standard LTLf, by considering arbitrary formulas as well as classes of formulas defined in terms of relevant syntactic restrictions. Moreover, a reasoner for LTL on weighted finite traces is presented, and its performances are assessed on benchmark data.