LTL on Weighted Finite Traces: Formal Foundations and Algorithms

LTL on Weighted Finite Traces: Formal Foundations and Algorithms

Carmine Dodaro, Valeria Fionda, Gianluigi Greco

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 2606-2612. https://doi.org/10.24963/ijcai.2022/361

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.
Keywords:
Knowledge Representation and Reasoning: Knowledge Representation Languages
Knowledge Representation and Reasoning: Learning and reasoning