LTL on finite traces (LTLf) is a logic that attracted much attention in recent literature, due to 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 LTLf on weighted traces is presented, and its performance are assessed on benchmark data.
LTL on Weighted Finite Traces: Formal Foundations and Algorithms
Dodaro C.;Fionda V.;Greco G.
2022-01-01
Abstract
LTL on finite traces (LTLf) is a logic that attracted much attention in recent literature, due to 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 LTLf on weighted traces is presented, and its performance are assessed on benchmark data.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
