--- title: "LTL on Weighted Finite Traces: Formal Foundations and Algorithms" authors: - "Carmine Dodaro" - "Valeria Fionda" - "Gianluigi Greco" doi: "10.24963/ijcai.2022/361" url: "https://ijcai.org/proceedings/2022/361" pdf: "https://ijcai.org/proceedings/2022/0361.pdf" venue: "Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence" year: 2022 pages: "2606-2612" track: "Main Track" keywords: - "Knowledge Representation and Reasoning: Learning and reasoning" - "Knowledge Representation and Reasoning: Knowledge Representation Languages" --- # 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*, pages 2606-2612. DOI: [10.24963/ijcai.2022/361](https://doi.org/10.24963/ijcai.2022/361) ## 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. ## Full text ## 1 Introduction Linear Temporal Logic over finite traces (short: LTLf ) is a logic formalism based on interpreting standard LTL formulas [Pnueli, 1977] over finite, yet unbounded, successions of states (see, e.g., [De Giacomo and Vardi, 2013]). The formalism has been recently attracting much attention in the AI literature, as it fits several scenarios where the traditional interpretation over infinite traces is not appropriate. For instance, LTLf has been exploited to formalize and validate the behavior of dynamical systems (e.g., [De Giacomo et al., 2014b; De Giacomo and Vardi, 2015]), to reason about planning domains (e.g. [De Giacomo and Rubin, 2018; Zhu et al., 2020; Xiao et al., 2021]), and to declaratively specify, analyze and monitor business processes (e.g. [van der Aalst et al., 2009; Montali et al., 2010; De Giacomo et al., 2014a]). As a matter of facts, however, the usage of LTLf in realworld domains is still rather limited, despite a number of efficient reasoning engines have been already made available (see [Li et al., 2020; Fionda and Greco, 2018]). Indeed, a major limitation of LTLf is that it cannot go beyond reasoning over qualitative properties of the environment, since it misses the ability to address certain quantitative aspects that are crucial in practical applications, such as time, probabilities, or costs related to realizing some desired behavior. ∗Contact Author Clearly enough, LTLf inherits this limitation from LTL. In fact, the development of "quantitative" frameworks for LTL has been an active area of research in the last two decades. In particular, LTL extensions have been proposed within settings where constants take values from some given lattice and the semantics of Boolean and temporal operators has been recast as operations defined on that lattice [Kupferman and Lustig, 2007; Droste and Vogler, 2012]. Other works have instead studied LTL over weighted transition systems [Faella et al., 2008; de Alfaro et al., 2004; Droste and Rahonis, 2016; Baier et al., 2014]. And, finally, a number of approaches have been defined to introduce quantitative features suitedfor instance-to express a tolerance on the number of time instants where a formula that is always required to hold in the future actually does not hold [Kuperberg, 2014], to specify eventualities with a bounded wait time [Kupferman et al., 2009; Alur et al., 2001], to accommodate averaging [Bouyer et al., 2014] or discounting [Mandrali, 2012; de Alfaro et al., 2005] modalities, and to deal with propositional quality operators [Almagor et al., 2016]. Compared to the above body of literature for LTL, considerably less attention has been paid to study LTLf in quantitative settings. Indeed, even though we might adapt to LTLf some of the extensions introduced for LTL (see, e.g., [Camacho et al., 2018b]), the typical usage scenarios of LTLf call for ad-hoc solutions and approaches, which were missing in the literature so far. In the paper, we fill this gap by proposing and studying a "weighting" framework that is specific for LTLf and where quantitative aspects are encoded in the finite traces over which formulas are evaluated, rather than on the formulas themselves. Roughly, each variable is associated with a weight, and the weight of a state is given as a function of the weights of the variables evaluating true in it; the goal is, then, to compute an optimal model, i.e., such that the overall weight obtained by suitably aggregating the weights of the various (finitely many) states is minimized. In more details: - We define the concept of valuation structures as mechanisms to flexibly equip each trace with a weight, and we identify and exemplify certain monotonicity properties of that structures guaranteing that optimal models always exist for satisfiable LTLf formulas (Section 2). - We depict a clear picture of the computational costs to be paid for the rich expressiveness of the resulting framework compared to standard LTL on finite traces, by considering arbitrary formulas as well as formulas belonging to some relevant syntactic fragments (Section 3). - We illustrate the architecture of WELTL, a system prototype implemented to reason about LTLf over weighted traces exploiting our theoretical findings and a rewriting in terms of Answer Set Programming (ASP) [Brewka et al., 2011]; and, finally, we assess and discuss its performance on some benchmark data (Section 4). 1 ## 2 Formal Framework In this section, we introduce a framework for evaluating LTLf formulas on weighted finite traces, and we illustrate its salient features by discussing some example applications. ## 2.1 Basic Notions and Results LTL on finite traces. Let V be a universe of propositional variables. An LTLf formula ϕ over V is an expression 2 built according to the grammar ϕ ::= true | false | x | ¬x | (ϕ ∧ ϕ) | (ϕ ∨ ϕ) | X(ϕ) | Xw(ϕ) | (ϕ U ϕ)| (ϕ R ϕ), where: x ∈ V; "∧", "∨", and "¬" are the standard Boolean connectives; and "X" (next), "Xw" (weak next), "U" (until), and "R" (release) are temporal operators. A finite trace over V is a sequence π = π0, π1, ..., πn-1 such that πi ⊆ V, for each i ∈ {0, ..., n - 1}. We say that the formula ϕ holds in π at the instant i ∈ {0, ..., n - 1}, denoted by π, i |= ϕ, by inductively considering subformulas as follows: ``` π, i |= y iff y ∈ πi or y = true; π, i |= ¬y iff y ̸∈ πi or y = false; π, i |= (ϕ1 ∧ϕ2) iff π, i |= ϕ1 and π, i |= ϕ2; π, i |= (ϕ1 ∨ϕ2) iff π, i |= ϕ1 or π, i |= ϕ2; π, i |= X(ϕ′ ) iff i < n-1 and π, i +1 |= ϕ′ ; π, i |= Xw(ϕ′ ) iff π, i |= X(ϕ′ ) or i = n - 1; π, i |= (ϕ1 U ϕ2) iff ∃j ≥ i such that π, j |= ϕ2 and ∀k with i ≤ k < j we have π, k |= ϕ1; π, i |= (ϕ1 R ϕ2) iff ∀i ≤ j < n it holds π, j |= ϕ2; or ∃j ≥ i such that π, j |= ϕ1 and ∀i ≤ k ≤ j we have π, k |= ϕ2; ``` Example 2.1 Consider the LTLf formula ϕ = (a ∨ X(b)) ∧ (cU(d ∧ Xw(a))) defined over the set V = {a, b, c, d} of propositional variables. The finite trace π = {a, d} (consisting of one time instant only) is a model of ϕ; indeed, π, 0 |= a ∨X(b) holds because a ∈ π0, while π, 0 |= c U (d ∧Xw(a)) holds because d ∈ π0 and there is no subsequent time instant (hence, Xw(a) holds too). Other models are π′ = {c}, {b, d}, π′′ = {c}, {c, b}, {d}, and π′′′ = {c}, {c, b}, {d}, {a}. Instead, note that the trace {b, c}, {a}, {d} is not a model. ✁ Whenever π, 0 |= ϕ holds, then we say that π is a model of ϕ and we just write π |= ϕ. Valuation structures. A valuation structure v on V is a tuple v = 〈◦, ∗,w〉, where w : V ↦→ Z is a function mapping each variable x ∈ V to an integer w(x), and where ◦ and ∗ are two binary operators defined over Z, which are moreover commutative and associative. For any set {x1, ..., xm} ⊆ V, we define v({x1, ..., xm}) as the value w(x1) ◦ · · · ◦ w(xm). Moreover, for a trace π = π0, π1, ..., πn-1, its v-weight is defined as v(π) = v(π0) ∗ · · · ∗ v(πn-1). 1 WELTL, the benchmark data and details on the (theoretical/experimental) results are available as Supplementary Material. 2 W.l.o.g., we consider formulas in negated normal form, i.e., negations are in front of propositional variables only. Example 2.2 Consider again the setting of Example 2.1, and the valuation structure v = 〈+,×,w〉 where w(a) = 6, w(b) = 2, w(c) = 2, and w(d) = 1. Then, we have v(π) = v({a, d}) = w(a) + w(d) = 7. Furthermore, we have that v(π′ ) = v(π′0 ) × v(π′1 ) = 6, v(π′′ ) = v(π′′ 0 ) × v(π′′ 1 ) × v(π′′ 2 ) = 8, and v(π′′′ ) = v(π′′ ) × w(a) = 48. ✁ Valuation structures are used to single out the "best" models by just looking for minimizing their associated weights. More formally, any model π∗ of ϕ is called v-optimal if there is no model π of ϕ with v(π) < v(π∗ ). Example 2.3 In our running example, we have v(π′ ) < v(π), v(π′ ) < v(π′′ ), and v(π′ ) < v(π′′′ ) hold. In fact, π′ is an optimal model. In particular, note that the models where c holds at the first time instant, while c plus b hold at the second time instant have v-weight at least 2 × 4 = 8. ✁ Monotone valuations. Perhaps not surprisingly, optimal models are not guaranteed to exist, even ifad the LTLf formula given to hand is satisfiable (that is, if admits a model). For instance, consider the structure v = 〈+,+,-1〉 where -1 is the constant function mapping every propositional vari- able x ∈ V to -1. Then, for the formula ϕ = a and any model π (of whatever length), the trace ¯π obtained by appending the state {a} to π is again a model and v(¯π) = v(π)-1 < v(π). Motivated by the above observation, we hereinafter restrict ourselves to valuation structures v = 〈◦, ∗, w〉, which we call monotone, enjoying the following properties: - (P1) w(x) ≥ 0, for each x ∈ V; - (P3) w1 ∗ w2 ≥ max{w1, w2}, for each pair w1, w2 ≥ 0. - (P2) w1 ◦w2 ≥ max{w1, w2}, for each pair w1, w2 ≥ 0; and The following is a simple consequence of monotonicity. Lemma 2.4 Assume that v = 〈◦, ∗, w〉 is a monotone valuation structure, and let π0, ..., πn-1 be a trace. Then, for each pair 0 ≤ i < j ≤ n-1, it holds v(π0, ..., πi) ≤ v(π0, ..., πj). Theorem 2.5 If v = 〈◦, ∗, w〉 is a monotone valuation structure and ϕ is satisfiable, then ϕ admits a v-optimal model. Proof (Sketch). Let Π be the set of irreducible models of ϕ, that is, none of their prefixes is a model too. Since ϕ is satisfiable, Π ̸= ∅. Then, let π∗ be a model of minimum v-weight over all models in Π. We claim that π∗ is v-optimal. Indeed, assume by contradiction that π = π0, ..., πn-1 is a model with v(π) < v(π∗ ). By construction of π∗ , π ̸∈ Π; hence, there is a time instant i ∈ {0, ..., n - 2} such that the prefix π0, ..., πi belongs to Π, which implies v(π∗ ) ≤ v(π0, ..., πi). However, by Lemma 2.4, we know that v(π) ≥ v(π0, ..., πi), which entails v(π) ≥ v(π∗ ), which is impossible. ✷ Figure 1: The planning problem P, three models of ϕP, and their values under the valuations structures built over "+" and "max". ![Image](https://ijcai.org/proceedings/2022/fulltext/361/image_000000_e4ac7a5556f8517cd2d11ff0bd5b131f57a573aef06ee7ed4972e8cfb651ebc6.png) ## 2.2 Examples of Monotone Valuations Noticeable monotone valuations can be defined over "+" and "max", e.g. to encode cost-related planning problems. Consider for instance the planning problem P in Figure 1: a set F = {f1, ..., f8} of fluents is given and, by starting from the scenario where f1 holds, our goal is to end up with f8, by applying, possibly in parallel, some of the available actions in A = {a, b, c, d, e}. An example solution is the plan where we first execute a ("consuming" f1 and "producing" f2, f3, and f4); then, we execute in parallel actions b, c, and d; and, finally, we execute e. It is well-known (see, e.g., [De Giacomo and Vardi, 2013]) that planning problems P can be easily encoded via LTLf formulas ϕP over propositional variables in A ∪ F so that models for ϕP one-to-one correspond with plans for P-at each time instant, we just keep trace of the fluents that hold and of the actions that are executed (see again Figure 1, reporting the model corresponding to the plan discussed above, plus two further models). We next enrich ϕP with valuations suited to encode cost-related variants. 〈+,+, c〉. Assume that each action x ∈ A is associated with a cost c(x), and consider the structure 〈+,+, c〉, where c(y) = 0 holds, for each fluent y ∈ F. Then, 〈+,+, c〉- optimal models correspond to plans whose total cost is minimized over all the possible plans. For instance, by assuming that all actions cost 1, every model of ϕP is also an optimal one, since all plans reaching the goal have the same cost (namely, 5)-for they need to execute all given actions. 〈+,max, r〉. Suppose that each action x ∈ A is associated with the number r(x) of employees required for its execution. If it is necessary, in time of a pandemic, to limit the number of employees that are simultaneously in the office, then we can consider the valuation structure 〈+,max, r〉 (with r(y) = 0, for each y ∈ F). For instance, in the setting of Figure 1, by assuming that all actions require 1 employee only, except d requiring 2 employees, we get that 〈+, max, r〉-optimal models of ϕP correspond to plans where d is executed alone. 〈max,+, t〉. Consider a setting where each action x ∈ A is associated with the time t(x) required for its execution. If we are interested in minimizing the total time for plan execution, then we can consider the valuation structure 〈max, +, t〉 (with t(y) = 0, for each y ∈ F)-in particular, note that at each step, for the actions that are executed in parallel, we just consider the maximum time over all of them. In our running example, by assuming that every action requires a unit of time, the only 〈max,+, t〉-optimal model of ϕP corresponds to the plan where b, c, and d are executed in parallel. 〈max,max, t〉. Assume, finally, that we want to fix the duration of the work shift, by computing the minimum amount of time needed to complete each step. This can be modeled via the structure 〈max,max, t〉, so that the total cost is now the maximum completion time over all the steps. For instance, by assuming again that every action requires a unit of time, every model is an optimal one and its cost is 1. ## 3 Complexity of LTLf onWeighted Traces In this section, we study the computational complexity of reasoning about LTLf on weighted traces. Formally, we consider the ∃MODEL problem that, given as input an integer τ ≥ 0, an LTLf formula ϕ, and a structure v = 〈◦, ∗,w〉, asks whether there is a model π of ϕ such that v(π) ≤ τ . In the analysis, we assume a standard encoding for the input; in particular, v is given by explicitly listing all elements in its domain with their associated values, while ◦ and ∗ are polynomial-time computable and produce outputs having size polynomial w.r.t. the input size. Hereinafter, the size of ϕ, i.e., the total number of temporal operators, Boolean connectives and propositional variables it contains, is denoted by ||ϕ||. ## 3.1 Basic Results: Weighted Transition Graph To prove our basic complexity results, we introduce the notion of weighted transition graph, which we formalize in the spirt of the transition system defined by [Li et al., 2020]. An LTLf formula is in neXt Normal Form (XNF) if all occurrences of the temporal operators R and U are nested within the scope of some X or Xw operator. Note that there is a linear-time conversion from any formula ϕ into an equivalent XNF one, denoted as xnf(ϕ); indeed, we can build xnf(ϕ) from ϕ by just applying the following transformations: - ϕ1 U ϕ2 is replaced by ϕ2 ∨ (ϕ1 ∧ X(ϕ1 U ϕ2)); Given xnf(ϕ), we then define VX(ϕ) (resp., VXw (ϕ)) as the set of all its X-subformulas (resp., Xw-subformulas) that are not nested within the scope of some other X or Xw operator; moreover, let xnf(ϕ)p denote xnf(ϕ) viewed as a propositional formula over V ∪ VX(ϕ) ∪ VXw (ϕ). - ϕ1 R ϕ2 is replaced by ϕ2 ∧ (ϕ1 ∨ Xw(ϕ1 R ϕ2)). Example 3.1 For the formula ϕ of Example 2.1, we have Let σ be a model of xnf(ϕ)p . If σ ∩ VX(ϕ) = ∅, then we define σ|X = end, where end is a special symbol not occurring in V; otherwise, we define: 3 Models of the propositional formula xnf(φ)p are sets of propositional variables (or, equivalently, traces with one time instant). ![Image](https://ijcai.org/proceedings/2022/fulltext/361/image_000001_1534ae41356a797675e67a36b6411b6a1efa894f97de7f497be7a1adf6d05464.png) Intuitively, σ|X is the XNF formula that is required to hold in the next time instant (actually being end, if no further time instant is required), when σ holds at the present instant; in fact, Xw subformulas are only considered if a subsequent time instant is required to exist due to some X subformula. Then, the weighted transition graph just unfolds the formula ϕ, via XNF transformations, by looking for convergence to end. Definition 3.2 The weighted transition graph wtg(ϕ, v) is the tuple 〈N,E, λE, vE〉 where: (N,E) is a directed multigraph over XNF formulas; λE : E ↦→ 2V ; and vE : E ↦→ Z. In particular: xnf(ϕ) is in N; for each ¯ ϕ ∈ N \ {end} and minimal model σ for ¯ ϕp , σ|X is in N and the edge e = ( ¯ ϕ, σ|X ) is in E, with λE(e) = σ ∩ V and vE(e) = v(σ ∩ V); no further node (resp., edge) is in N (resp., E). ✷ As an example, consider Figure 2 and note that the minimum-weighted path from ϕ to end corresponds to the v-optimal model π′ in Example 2.3. This is not by chance. Indeed, by letting Σi be the set of all minimal models of ϕpi , the following lemma derives by observing that ϕi can be rewritten as ∨σ∈Σi (∧x∈σ∩V x ∧ f(σ|X )) , where f is such that f(end) = true and f(Ψ) = X(Ψ), for each Ψ ̸= end. Lemma 3.3 Let wtg(ϕ, v) be the weighted transition graph associated with ϕ and v = 〈◦, ∗, w〉. Then, - (2) If π∗ is a v-optimal model of ϕ, then there is a simple path ϕ0, ϕ1, ..., ϕn, such that ϕ0 = ϕ, ϕn = end, and - (1) If there is a path ϕ0, ϕ1, ..., ϕn with ϕn = end, then λE(ϕ0, ϕ1), ..., λE(ϕn-1, ϕn) is a model of ϕ0; - (2.a) λE(ϕ0, ϕ1), ..., λE(ϕn-1, ϕn) = π∗ ; Now, it is routine that we can check in PSPACE whether there is a path from ϕ to end corresponding to a model whose v-weight is τ at most: we can build the path nondeterministically (recall that NPSPACE = PSPACE), and we identify a failure when either the weight of the current path exceeds τ, or its length exceeds the overall number of nodes (with this number being at most exponential in ||ϕ|| and, therefore, requiring polynomial space for its encoding). - (2.b) vE(ϕ0, ϕ1) ∗ · · · ∗ vE(ϕn-1, ϕn) = v(π∗ ). ## Theorem 3.4 ∃MODEL is in PSPACE. However, the bound can be improved if we impose syntactic restrictions on the allowed operators. Formally, for any set T ⊆ {X, Xw,U,R}, we define 〈T〉-LTLf as the class of all LTLf formulas where only operators in T can be used. Theorem 3.5 ∃MODEL is in NP, if restricted on 〈T〉-LTLf formulas, with T ∈ {{X, Xw}, {Xw, R}}. Proof (Sketch). For a formula ϕ ∈ 〈{X, Xw}〉-LTLf , it is immediate to check that the length of the longest simple path in wtg(ϕ, v) from ϕ to end is bounded by the maximum number of nested X operators, which is clearly polynomial in ||ϕ||. For 〈{Xw,R}〉-LTLf formulas, instead, just check < l a t e x i s h 1 \_ b 6 4 = " F m N 3 K I o P j G D Q L Z z d J > A C X c n V E B 7 T O w R k S p y M W 2 g 0 U r Y 9 q f + u v 5 H / 8 < l a t e x i s h 1 \_ b 6 4 = " F m N 3 K I o P j G D Q L Z z d J > A C X c n V E B 7 T O w R k S p y M W 2 g 0 U r Y 9 q f + u v 5 H / 8 < l a t e x i s h 1 \_ b 6 4 = " D d L 3 5 K G C Y Q H 2 Z g y > A / X c n V N M E J p T w F + r I k o 0 q j U u 9 P z v m O 7 S W R B 8 f < l a t e x i s h 1 \_ b 6 4 = " D d L 3 5 K G C Y Q H 2 Z g y > A / X c n V N M E J p T w F + r I k o 0 q j U u 9 P z v m O 7 S W R B 8 f < l a t e x i s h 1 \_ b 6 4 = " 3 7 Y 8 O / X p 9 n S H V E 5 D q U I > A C G c L g M F T W + R 0 N 2 Z K J u j z P Q w o d k y v r B f m < l a t e x i s h 1 \_ b 6 4 = " 3 7 Y 8 O / X p 9 n S H V E 5 D q U I > A C G c L g M F T W + R 0 N 2 Z K J u j z P Q w o d k y v r B f m < l a t e x i s h 1 \_ b 6 4 = " 3 m o n Q A y C 5 B k P 8 J 7 u H 0 > / X c V N T E F + I L R j D p O Y d W 9 w r f G Z 2 g K z U M S q v < l a t e x i s h 1 \_ b 6 4 = " 3 m o n Q A y C 5 B k P 8 J 7 u H 0 > / X c V N T E F + I L R j D p O Y d W 9 w r f G Z 2 g K z U M S q v < l a t e x i s h 1 \_ b 6 4 = " k R J + g c f 5 D y Z m N C j M > A L X d V H S F T 7 W q 2 p K B u 0 r Q z I o 8 O G v Y 3 P 9 n E w / U < l a t e x i s h 1 \_ b 6 4 = " k R J + g c f 5 D y Z m N C j M > A L X d V H S F T 7 W q 2 p K B u 0 r Q z I o 8 O G v Y 3 P 9 n E w / U < l a t e x i s h 1 \_ b 6 4 = " 8 w p U g J q O A S u P B F c > C G 3 d V D L M T X 7 W + v R n Y k 0 r Q N z I 5 E / o 2 j H y m Z f 9 K < l a t e x i s h 1 \_ b 6 4 = " 8 w p U g J q O A S u P B F c > C G 3 d V D L M T X 7 W + v R n Y k 0 r Q N z I 5 E / o 2 j H y m Z f 9 K < l a t e x i s h 1 \_ b 6 4 = " + q D F V C f z U K P S O A r d G j > X c Z L g M I u p N 8 W J y Y T 2 o k Q 5 9 v 7 R 3 w 0 / E m B n H < l a t e x i s h 1 \_ b 6 4 = " + q D F V C f z U K P S O A r d G j > X c Z L g M I u p N 8 W J y Y T 2 o k Q 5 9 v 7 R 3 w 0 / E m B n H < l a t e x i s h 1 \_ b 6 4 = " M B 2 U X + d p 0 O Q S G L N K w q v c > A C F 3 V D g T 7 W Z R y f u 5 k 8 o r H j z n m I E / Y 9 P < l a t e x i s h 1 \_ b 6 4 = " M B 2 U X + d p 0 O Q S G L N K w q v c > A C F 3 V D g T 7 W Z R y f u 5 k 8 o r H j z n m I E / Y 9 P < l a t e x i s h 1 \_ b 6 4 = " 2 M k 3 D / w G 0 n H o J y + q Z f U K > A C c d V L S g F T X 7 W B v R Y r Q N z I 5 E j u O m p P 9 8 < l a t e x i s h 1 \_ b 6 4 = " 2 M k 3 D / w G 0 n H o J y + q Z f U K > A C c d V L S g F T X 7 W B v R Y r Q N z I 5 E j u O m p P 9 8 < l a t e x i s h 1 \_ b 6 4 = " O Z J E C 8 H q m Q 0 3 k r X o S v c > A K d V D g N B 2 W j Y I G n M P w U p 5 7 / + u F L y z R T f 9 < l a t e x i s h 1 \_ b 6 4 = " O Z J E C 8 H q m Q 0 3 k r X o S v c > A K d V D g N B 2 W j Y I G n M P w U p 5 7 / + u F L y z R T f 9 < l a t e x i s h 1 \_ b 6 4 = " v T + P m d 9 z Q U A 0 g u M y Y > C F X c V D L S 7 W q B p K Z f G k / r O 3 H 2 w o 5 j J R I n 8 E N < l a t e x i s h 1 \_ b 6 4 = " v T + P m d 9 z Q U A 0 g u M y Y > C F X c V D L S 7 W q B p K Z f G k / r O 3 H 2 w o 5 j J R I n 8 E N < l a t e x i s h 1 \_ b 6 4 = " X O Z 7 V B n w p / + f H U 8 D G I > A C F 3 c d L S g M T W q v Q z j u k P J 2 N y R K 0 9 5 o Y m E r < l a t e x i s h 1 \_ b 6 4 = " X O Z 7 V B n w p / + f H U 8 D G I > A C F 3 c d L S g M T W q v Q z j u k P J 2 N y R K 0 9 5 o Y m E r < l a t e x i s h 1 \_ b 6 4 = " + q D F V C f z U K P S O A r d G j > X c Z L g M I u p N 8 W J y Y T 2 o k Q 5 9 v 7 R 3 w 0 / E m B n H < l a t e x i s h 1 \_ b 6 4 = " + q D F V C f z U K P S O A r d G j > X c Z L g M I u p N 8 W J y Y T 2 o k Q 5 9 v 7 R 3 w 0 / E m B n H < l a t e x i s h 1 \_ b 6 4 = " M B 2 U X + d p 0 O Q S G L N K w q v c > A C F 3 V D g T 7 W Z R y f u 5 k 8 o r H j z n m I E / Y 9 P < l a t e x i s h 1 \_ b 6 4 = " M B 2 U X + d p 0 O Q S G L N K w q v c > A C F 3 V D g T 7 W Z R y f u 5 k 8 o r H j z n m I E / Y 9 P < l a t e x i s h 1 \_ b 6 4 = " q V S o N B Y w D y 9 P A I + > C 3 c L g M F T X 7 W E J Z u f d G 5 k R K U H j r 8 O v n 2 / p m Q 0 z < l a t e x i s h 1 \_ b 6 4 = " q V S o N B Y w D y 9 P A I + > C 3 c L g M F T X 7 W E J Z u f d G 5 k R K U H j r 8 O v n 2 / p m Q 0 z < l a t e x i s h 1 \_ b 6 4 = " F X H f P S o N m G L p U g R v B 3 Y J y 0 > A C c V 9 w E z M 8 q W D k j 7 d u + O T 2 n I r Q 5 K / Z < l a t e x i s h 1 \_ b 6 4 = " F X H f P S o N m G L p U g R v B 3 Y J y 0 > A C c V 9 w E z M 8 q W D k j 7 d u + O T 2 n I r Q 5 K / Z < l a t e x i s h 1 \_ b 6 4 = " y / p A 9 C G c B Q f z D k H S u > 3 V w N E J 2 L X F + R Z j r M d U v 5 7 T W n 0 o O I K q 8 P g m Y < l a t e x i s h 1 \_ b 6 4 = " y / p A 9 C G c B Q f z D k H S u > 3 V w N E J 2 L X F + R Z j r M d U v 5 7 T W n 0 o O I K q 8 P g m Y < l a t e x i s h 1 \_ b 6 4 = " o R Z w C K z 2 + N q u G d O T Y V P c > A 3 D J S g B E W j v m I n M U p 5 0 7 H k / X F L y Q r f 8 9 < l a t e x i s h 1 \_ b 6 4 = " o R Z w C K z 2 + N q u G d O T Y V P c > A 3 D J S g B E W j v m I n M U p 5 0 7 H k / X F L y Q r f 8 9 < l a t e x i s h 1 \_ b 6 4 = " / 5 N p n r E c 0 D 8 9 d 3 R L O J g > A C G V S M F T X 7 W + q B v U w Y k Q z I o 2 j H u y m Z f P K < l a t e x i s h 1 \_ b 6 4 = " / 5 N p n r E c 0 D 8 9 d 3 R L O J g > A C G V S M F T X 7 W + q B v U w Y k Q z I o 2 j H u y m Z f P K < l a t e x i s h 1 \_ b 6 4 = " 8 K c p g M + T z 7 X v U R P O q H r k > A C 3 d V L S F W 2 y Z B f u G / Q j N J 0 9 n Y m I w D 5 E o < l a t e x i s h 1 \_ b 6 4 = " 8 K c p g M + T z 7 X v U R P O q H r k > A C 3 d V L S F W 2 y Z B f u G / Q j N J 0 9 n Y m I w D 5 E o < l a t e x i s h 1 \_ b 6 4 = " C u 5 O 7 c V 3 y / L D T P f j g F 0 > A G d S M X W + q B v R n U w Y k r Q N z I E o 2 H m Z J p 9 K 8 < l a t e x i s h 1 \_ b 6 4 = " C u 5 O 7 c V 3 y / L D T P f j g F 0 > A G d S M X W + q B v R n U w Y k r Q N z I E o 2 H m Z J p 9 K 8 < l a t e x i s h 1 \_ b 6 4 = " v T + P m d 9 z Q U A 0 g u M y Y > C F X c V D L S 7 W q B p K Z f G k / r O 3 H 2 w o 5 j J R I n 8 E N < l a t e x i s h 1 \_ b 6 4 = " v T + P m d 9 z Q U A 0 g u M y Y > C F X c V D L S 7 W q B p K Z f G k / r O 3 H 2 w o 5 j J R I n 8 E N < l a t e x i s h 1 \_ b 6 4 = " X O Z 7 V B n w p / + f H U 8 D G I > A C F 3 c d L S g M T W q v Q z j u k P J 2 N y R K 0 9 5 o Y m E r < l a t e x i s h 1 \_ b 6 4 = " X O Z 7 V B n w p / + f H U 8 D G I > A C F 3 c d L S g M T W q v Q z j u k P J 2 N y R K 0 9 5 o Y m E r < l a t e x i s h 1 \_ b 6 4 = " n E v Z M X O j A u p P d g y 2 m Y > C K 3 c V H L S F T 7 W + R q B f G k U / Q r N z J 0 9 I w D 8 5 o < l a t e x i s h 1 \_ b 6 4 = " n E v Z M X O j A u p P d g y 2 m Y > C K 3 c V H L S F T 7 W + R q B f G k U / Q r N z J 0 9 I w D 8 5 o < l a t e x i s h 1 \_ b 6 4 = " 0 j m 8 + z K B C k n R Z P N W w o A T Q > G 3 c d V D L S g M F X 7 q v U Y r I 5 E / 2 H u y O J f p 9 < l a t e x i s h 1 \_ b 6 4 = " 0 j m 8 + z K B C k n R Z P N W w o A T Q > G 3 c d V D L S g M F X 7 q v U Y r I 5 E / 2 H u y O J f p 9 < l a t e x i s h 1 \_ b 6 4 = " 2 B N / K v 0 n P y d C S G U W g V Q 9 > A 3 c w E J z M 8 F r H L o p Y I 5 O m j R q 7 D X Z + u f k T < l a t e x i s h 1 \_ b 6 4 = " 2 B N / K v 0 n P y d C S G U W g V Q 9 > A 3 c w E J z M 8 F r H L o p Y I 5 O m j R q 7 D X Z + u f k T Figure 2: The weighted transition graph wtg(ϕ, v) built for the formula ϕ = (a ∨ X(b)) ∧ (c U (d ∧ Xw(a))) and v = 〈◦, ∗, w〉. ![Image](https://ijcai.org/proceedings/2022/fulltext/361/image_000002_a3484e40eb29e051ac07e7a4bea623ccd761b0bf11556a36f4640483c9a4f67e.png) that all edges outgoing from ϕ are converging into end. Therefore, on these fragments (and with monotone valuations v), v-optimal models have polynomial length. Thus, we can solve ∃MODEL by guessing a trace with a nondeterministic Turing machine and by then checking in polynomial time whether its v-value is below the given threshold. ✷ ## 3.2 ACloser Look at LTLf Fragments According to Theorem 3.4, it seems that the expressiveness of the weighted framework comes at no cost (satisfiability for LTLf is PSPACE-complete [De Giacomo and Vardi, 2013]). We next embark on a finer-grained complexity analysis, and we show that actually this is not the case. In particular, we focus on valuation structures built over the operators "+" and "max", and we consider formulas with arbitrary Boolean connectives as well as negation-free formulas. A summary of our complexity results is depicted in Figure 3. Theorem 3.6 All results in Figure 3 hold. Proof (Idea). For the case of arbitrary formulas, all hardness results that are known to hold for LTLf are clearly inherited by our more expressive setting. The corresponding membership results come from Theorem 3.4 and Theorem 3.5. For negation-free formulas, we distinguish three cases. For the polynomial-time results, we define V ′ = {x ∈ V | w(x) ≤ τ}, and we can observe that ∃MODEL has a solution if, and only if, ϕ admits a model over V ′-with this latter task being feasible in polynomial time after the results for negation-free formulas (without valuation structures). For the various NP-hardness results, we can exhibit (different kinds of) reductions from the well-known vertex cover problem on undirected graphs G = (N, E). For instance, for the case 〈+, ∗, w〉 (even without temporal operators), we can view each node in N as a propositional variable with a unitary v-weight, and define the formula ϕ = ∧(x,y)∈E (x ∨ y). Then, there is a vertex cover with cardinality k at most if, and only if, there is a model for ϕ whose v-weight is k at most. Finally, PSPACE-hardness results can be shown by exploiting the valuation structures to simulate the possibility of negating some variables. As an example, let ϕ be an arbitrary 〈T〉-LTLf formula, with {U} ⊆ T or {X, R} ⊆ T . Consider ψ = ∧x∈V (x ∨ ¯x), and the formula ¯ ϕ derived fromϕ by: (1) Figure 3: Summary of complexity results in Section 3 for weighted LTLf-the column PLAIN reports the results that were already known to hold for LTLf without weights (see [Fionda and Greco, 2018]). | OPERATORS | ARBITRARY FORMULAS - PLAIN | ARBITRARY FORMULAS - ◦, ∗ | NEGATION-FREE FORMULAS - PLAIN | NEGATION-FREE FORMULAS - +,+ | NEGATION-FREE FORMULAS - +,max | NEGATION-FREE FORMULAS - max,+ | NEGATION-FREE FORMULAS - max,max | |-------------------------------------------------------------------------|------------------------------|-----------------------------|----------------------------------|--------------------------------|----------------------------------|----------------------------------|------------------------------------| | T ⊆ {Xw, R} {X} ⊆ T ⊆ {Xw, X} {U} ⊆ T ⊆ {Xw,U,R} {X,U} ⊆ T or {X,R} ⊆ T | NP-c NP-c PSPACE-c PSPACE-c | NP-c NP-c PSPACE-c PSPACE-c | in P in P in P in P | NP-c NP-c PSPACE-c PSPACE-c | NP-c NP-c PSPACE-c PSPACE-c | in P NP-c in P PSPACE-c | in P in P in P in P | replacing every occurrence of ¬x, for each x ∈ V, with ¯x; and (2) replacing every subformula ϕs with ϕs∧ψ. Consider then the valuation v = 〈+, max, w〉 where w(x) = w(¯x) = 1, for each x ∈ V. It can be checked that ϕ is satisfiable if, and only if, ¯ ϕ admits a model π such that v(π) ≤ |V|. ✷ ## 4 SystemDesign and Implementation The notion of weighted transition graph and its properties (cf. Lemma 3.3) provided us with an immediate approach to implement a prototype for LTLf over weighted traces, which we named WELTL. At a high level, it consists of two modules: WELTLdf : The module builds in a depth-first manner the weighted transition graph, by checking for a model/path whose weight is below the desired threshold. Moreover, as we deal with monotone structures, it avoids exploring paths whose current weight exceeds that threshold. WELTLbf : The module uses a complementary breadth-first approach, which is better suited to be supported via a mechanism for implicit navigation, that we implemented in terms of a rewriting in Answer Set Programming. In our experiments, we have found that WELTLdf is more effective to identify unsatisfiable instances, while WELTLbf can be more practical to compute models of satisfiable formulas. With this observation to hand, we have coupled the two approaches. Since the design of WELTLdf poses no special challenges (indeed, we adapted the reasoner presented by [Li et al., 2020]), we next focus on the description of WELTLbf , by subsequently presenting results of experimental activity. ## 4.1 WELTLbf (and ASP in a Nutshell) The architecture of WELTLbf is depicted in Figure 4. Given a formula ϕ, it starts by computing a model π of minimum length, or immediately checks that the formula is not satisfiable-this task is delegated to the model checker made available by [Fionda and Greco, 2018]. If v(π) ≤ τ , then we are done. Otherwise, WELTLbf starts its (implicit) breadthfirst exploration by looking for a model whose length ℓ coincides with the length of π and such that the corresponding value is τ at most. This is carried out by leveraging a rewriting 4 in terms of an Answer Set Program P(ϕ, ℓ, w). For the sake of completeness, we recall that an ASP program [Brewka et al., 2011] is made of (a combination of): (i) facts of the form "head."; (ii) normal rules of the form "head :-body."; (iii) choice rules of the form "{head} :-body."; (iv) constraints of the form " :-body.", where head is an atom and body is a set of (possibly negated) 4 Details on the encoding are in the Supplementary Material. Figure 4: Conceptual architecture of WELTLbf . ![Image](https://ijcai.org/proceedings/2022/fulltext/361/image_000003_865f84a6bc64a18b6dc38cb252e6c25009955d1bdfbf225b683d96bd9f0a8286.png) atoms, also including aggregate functions, such as #sum or #max [Faber et al., 2011]. Atoms can be made over variables (strings starting with uppercase letter) or constants (nonnegative integers or strings starting with lowercase letters). The semantics is given in terms of its answer sets, that is, sets A of ground atoms such that: (i) head is in A; (ii) whenever the body is true, head is in A; (iii) head can be in Awhenever the body is true; (iv) the body must be false. The ASP rewriting P(ϕ, ℓ, τ) uses the parse tree of ϕ: a fact var(vi) is included, for each node v and instant i ∈ {0, ..., ℓ-1}. Then, a choice rule ({selected(X)}:-var(X).) is used to guess the subformulas of ϕ (represented by the nodes in the parse tree) that hold at i; and, to check that such formulas actually hold, the definitions in Section 2 are straightforwardly translated in terms of constraints. Eventually, the ASP paradigm supports cost constraints that can encode the binary operators used in the valuation structures (in particular, they support "+" and "max"), so that the program can also enforce that answer set programs are associated with traces whose v-weight is τ at most. This is next exemplified. Example 4.1 For an illustration of the rewriting, consider the formula ϕ=a ∧ X(b), and the structure v=〈+,+,w〉 where w(a)=w(b)=3. Then, the ASP program P(ϕ, 2, τ) is shown in Figure 5. The parse tree has 4 nodes, denoted as and, a, x, and b. Then, rule (1) guesses the atoms corresponding to these nodes and to the time instants 0 and 1. Rule (2) forces that selected(and0) holds, i.e., the whole formula holds at the initial time instant. Rules (3) and (4) define the semantics Figure 5: ASP encoding of Example 4.1. ![Image](https://ijcai.org/proceedings/2022/fulltext/361/image_000004_0ea2bbf2af0a4405115f856185e7e9530bb9718c508e437b4c03979c923817af.png) < l a t e x i s h 1 \_ b 6 4 = " F f M T Y C c A / n L Z U G k S 8 0 o > 3 V D N 2 p r J E u j R d y I m z P X Q g w 9 + 7 5 K B q W v O H < l a t e x i s h 1 \_ b 6 4 = " F f M T Y C c A / n L Z U G k S 8 0 o > 3 V D N 2 p r J E u j R d y I m z P X Q g w 9 + 7 5 K B q W v O H < l a t e x i s h 1 \_ b 6 4 = " f d Y R g z j F y O c T M k 2 D m / o > A C 3 V N S w E J v r 9 W q U K I H P 5 8 + Q X u B n p 0 G Z L 7 < l a t e x i s h 1 \_ b 6 4 = " f d Y R g z j F y O c T M k 2 D m / o > A C 3 V N S w E J v r 9 W q U K I H P 5 8 + Q X u B n p 0 G Z L 7 < l a t e x i s h 1 \_ b 6 4 = " g 9 y + F I j z 5 B 8 k d O m E > A C Y 3 c V H S M J 7 / W 2 X Z Q u R K U p q D v G T w L f P r o N 0 n < l a t e x i s h 1 \_ b 6 4 = " g 9 y + F I j z 5 B 8 k d O m E > A C Y 3 c V H S M J 7 / W 2 X Z Q u R K U p q D v G T w L f P r o N 0 n < l a t e x i s h 1 \_ b 6 4 = " m 2 H T u y r X 9 8 c O N A v S 0 > C P 3 V B w M E J 7 + Z U d R F K n q G p Q f o z Y I j 5 / L D g k W < l a t e x i s h 1 \_ b 6 4 = " m 2 H T u y r X 9 8 c O N A v S 0 > C P 3 V B w M E J 7 + Z U d R F K n q G p Q f o z Y I j 5 / L D g k W < l a t e x i s h 1 \_ b 6 4 = " V P O r I R K C M G k 2 p F T d 5 o S 8 > A X c B L w z W v + N j 9 y g Z U J / H Q E n q 7 f m Y u 3 0 D < l a t e x i s h 1 \_ b 6 4 = " V P O r I R K C M G k 2 p F T d 5 o S 8 > A X c B L w z W v + N j 9 y g Z U J / H Q E n q 7 f m Y u 3 0 D < l a t e x i s h 1 \_ b 6 4 = " W L J d U j B z / v H o 3 w 8 F E M Y A > C P c V N S 9 q k p I r u K 2 O D R m X f + G y n 5 T Z g 7 Q 0 < l a t e x i s h 1 \_ b 6 4 = " W L J d U j B z / v H o 3 w 8 F E M Y A > C P c V N S 9 q k p I r u K 2 O D R m X f + G y n 5 T Z g 7 Q 0 < l a t e x i s h 1 \_ b 6 4 = " 8 N w F f p R j Y 2 U I S B d J u > A C P 3 c V M E X 7 + T Z K n q G y Q v 0 o z H m 5 O / L D g r k 9 W < l a t e x i s h 1 \_ b 6 4 = " 8 N w F f p R j Y 2 U I S B d J u > A C P 3 c V M E X 7 + T Z K n q G y Q v 0 o z H m 5 O / L D g r k 9 W < l a t e x i s h 1 \_ b 6 4 = " Y u 7 z / I A o d V L c r j N K T g > C P 3 B S w M E J 9 v q k p U F W 2 O D R m H X f + 8 G y n 5 Z Q 0 < l a t e x i s h 1 \_ b 6 4 = " Y u 7 z / I A o d V L c r j N K T g > C P 3 B S w M E J 9 v q k p U F W 2 O D R m H X f + 8 G y n 5 Z Q 0 < l a t e x i s h 1 \_ b 6 4 = " 9 X S Y c u 3 H v o G O 7 U Z m / > A C E V D L g M F 2 q k w Q R B T K y W 0 J P N p z r 8 f n I 5 j d < l a t e x i s h 1 \_ b 6 4 = " 9 X S Y c u 3 H v o G O 7 U Z m / > A C E V D L g M F 2 q k w Q R B T K y W 0 J P N p z r 8 f n I 5 j d < l a t e x i s h 1 \_ b 6 4 = " 7 V I T L Y J m 0 3 H E d 9 B z O M k X w > A C c S g N F G + n W 2 5 u Z f y K v P r q / 8 o U R Q p D j < l a t e x i s h 1 \_ b 6 4 = " 7 V I T L Y J m 0 3 H E d 9 B z O M k X w > A C c S g N F G + n W 2 5 u Z f y K v P r q / 8 o U R Q p D j < l a t e x i s h 1 \_ b 6 4 = " q C + r p 5 P m X Y d H k o 9 2 A j E > c V B L S w M G z W v Z Q u R 8 K g 0 y J F N / U D f 3 T n I O 7 < l a t e x i s h 1 \_ b 6 4 = " q C + r p 5 P m X Y d H k o 9 2 A j E > c V B L S w M G z W v Z Q u R 8 K g 0 y J F N / U D f 3 T n I O 7 < l a t e x i s h 1 \_ b 6 4 = " p k F j q 8 J T L P V n r S A W m o u M > B + 3 c D N 2 f 7 d Z C Q X O y g G H R 9 5 E z K v U 0 I w Y / < l a t e x i s h 1 \_ b 6 4 = " p k F j q 8 J T L P V n r S A W m o u M > B + 3 c D N 2 f 7 d Z C Q X O y g G H R 9 5 E z K v U 0 I w Y / < l a t e x i s h 1 \_ b 6 4 = " W I J y E d k 8 P L K m o U 7 + Z p > A B 3 c V D S N F 2 r f C Q X O g n G H T M R u j 9 5 z q v 0 Y / w < l a t e x i s h 1 \_ b 6 4 = " W I J y E d k 8 P L K m o U 7 + Z p > A B 3 c V D S N F 2 r f C Q X O g n G H T M R u j 9 5 z q v 0 Y / w < l a t e x i s h 1 \_ b 6 4 = " v B G C / 8 7 n T N D 3 W 2 R S f A > + c V L F p r d Z Q J X O y g k m H M u j 9 5 P o E z q K U 0 I Y w < l a t e x i s h 1 \_ b 6 4 = " v B G C / 8 7 n T N D 3 W 2 R S f A > + c V L F p r d Z Q J X O y g k m H M u j 9 5 P o E z q K U 0 I Y w < l a t e x i s h 1 \_ b 6 4 = " p 5 g S m G I q H 7 v / E o N B J U 9 > A + 3 c V D L F 2 r f d Z C Q X O y n 8 k T M R u j P z K 0 w W Y < l a t e x i s h 1 \_ b 6 4 = " p 5 g S m G I q H 7 v / E o N B J U 9 > A + 3 c V D L F 2 r f d Z C Q X O y n 8 k T M R u j P z K 0 w W Y < l a t e x i s h 1 \_ b 6 4 = " Q W A 9 R m / N z O I k P E 3 0 c > C F n V B S w J G 7 + r q 2 X p T U L j K D M y u d H Y 5 Z g f o v 8 < l a t e x i s h 1 \_ b 6 4 = " Q W A 9 R m / N z O I k P E 3 0 c > C F n V B S w J G 7 + r q 2 X p T U L j K D M y u d H Y 5 Z g f o v 8 < l a t e x i s h 1 \_ b 6 4 = " y Y 5 k O w N S / g m K q I G P c U T 8 > A B 9 H V E J 3 r L Z C v o F X p 2 j d M D u 7 z n Q 0 W f R + < l a t e x i s h 1 \_ b 6 4 = " y Y 5 k O w N S / g m K q I G P c U T 8 > A B 9 H V E J 3 r L Z C v o F X p 2 j d M D u 7 z n Q 0 W f R + < l a t e x i s h 1 \_ b 6 4 = " P f D z E O q r N K + m / Y I 8 > A B 9 H c V S J 3 U L Z C v k o F w X 5 G p 2 j d M u g 7 n T Q 0 y W R < l a t e x i s h 1 \_ b 6 4 = " P f D z E O q r N K + m / Y I 8 > A B 9 H c V S J 3 U L Z C v k o F w X 5 G p 2 j d M u g 7 n T Q 0 y W R < l a t e x i s h 1 \_ b 6 4 = " K Y U n N g E 2 f L C m V 9 A > H c Z D S F I P v 7 p w W q J X G y r 0 k + T o R u B 3 O 8 / 5 z d j M Q < l a t e x i s h 1 \_ b 6 4 = " K Y U n N g E 2 f L C m V 9 A > H c Z D S F I P v 7 p w W q J X G y r 0 k + T o R u B 3 O 8 / 5 z d j M Q < l a t e x i s h 1 \_ b 6 4 = " M J D X 5 V S c + o u 3 U 8 N P A > C H Z 7 g B F I L v R j E Q 2 m k z O w / n 9 p r 0 f d W T Y K y G q < l a t e x i s h 1 \_ b 6 4 = " M J D X 5 V S c + o u 3 U 8 N P A > C H Z 7 g B F I L v R j E Q 2 m k z O w / n 9 p r 0 f d W T Y K y G q < l a t e x i s h 1 \_ b 6 4 = " u d J G X z E 8 0 I / V O v 3 S Y Q > A C H c Z D L N F P 7 p w W q m U y r 2 k + T o R f B 5 n 9 g K j M < l a t e x i s h 1 \_ b 6 4 = " u d J G X z E 8 0 I / V O v 3 S Y Q > A C H c Z D L N F P 7 p w W q m U y r 2 k + T o R f B 5 n 9 g K j M < l a t e x i s h 1 \_ b 6 4 = " 2 B G z Y U W L Z I P f m Q / c > A H V N S 8 E J 3 X O 0 r g M 9 D w 7 v T k y 5 + u n d q C p j K F o R < l a t e x i s h 1 \_ b 6 4 = " 2 B G z Y U W L Z I P f m Q / c > A H V N S 8 E J 3 X O 0 r g M 9 D w 7 v T k y 5 + u n d q C p j K F o R < l a t e x i s h 1 \_ b 6 4 = " O + Q G m D I P T W d R w B c > A n V N S 8 E J 3 U r q / 9 L C p 5 Y F 2 o z 7 Z u j y M X g f H k 0 K v < l a t e x i s h 1 \_ b 6 4 = " O + Q G m D I P T W d R w B c > A n V N S 8 E J 3 U r q / 9 L C p 5 Y F 2 o z 7 Z u j y M X g f H k 0 K v < l a t e x i s h 1 \_ b 6 4 = " 7 V R g G B Y / O p S P C n c H X T Q q 8 > A 3 N E J W v 0 I r M F + w K 2 d j D 9 m 5 f u L z k Z U y o < l a t e x i s h 1 \_ b 6 4 = " 7 V R g G B Y / O p S P C n c H X T Q q 8 > A 3 N E J W v 0 I r M F + w K 2 d j D 9 m 5 f u L z k Z U y o < l a t e x i s h 1 \_ b 6 4 = " V 5 q Z B R O U Q T / u P c y w W 2 m 0 > A n N S 8 E J 3 r 9 L p I Y F g o z + D 7 G j f d v X k M C H K < l a t e x i s h 1 \_ b 6 4 = " V 5 q Z B R O U Q T / u P c y w W 2 m 0 > A n N S 8 E J 3 r 9 L p I Y F g o z + D 7 G j f d v X k M C H K < l a t e x i s h 1 \_ b 6 4 = " K J z g P A 0 I + f 8 q 9 U / o Z 5 E k N Y > B 3 c V S r F u p L 2 Q T j D G m w y W n C H X v M R d O 7 < l a t e x i s h 1 \_ b 6 4 = " K J z g P A 0 I + f 8 q 9 U / o Z 5 E k N Y > B 3 c V S r F u p L 2 Q T j D G m w y W n C H X v M R d O 7 < l a t e x i s h 1 \_ b 6 4 = " f W L / v q g J 5 3 + U 9 V B E Y F K w > A n c N S 8 r C p 2 o Q z R O D 7 I m G Z u j y M d X 0 H k P T < l a t e x i s h 1 \_ b 6 4 = " f W L / v q g J 5 3 + U 9 V B E Y F K w > A n c N S 8 r C p 2 o Q z R O D 7 I m G Z u j y M d X 0 H k P T < l a t e x i s h 1 \_ b 6 4 = " P I 2 D S E M j v Q w N / V J 8 Y > A B H c L T g O z F + 9 R U k X C o m G d n 7 f W q y r K 3 0 Z u p 5 < l a t e x i s h 1 \_ b 6 4 = " P I 2 D S E M j v Q w N / V J 8 Y > A B H c L T g O z F + 9 R U k X C o m G d n 7 f W q y r K 3 0 Z u p 5 < l a t e x i s h 1 \_ b 6 4 = " D G I z d y p + n f 5 o L W R / S w E u > A B H c V N 8 J 3 X O 0 r g M 9 P U 2 m 7 v T k Q Y q Z C j F K < l a t e x i s h 1 \_ b 6 4 = " D G I z d y p + n f 5 o L W R / S w E u > A B H c V N 8 J 3 X O 0 r g M 9 P U 2 m 7 v T k Q Y q Z C j F K Figure 6: Execution times of over the benchmarks. ![Image](https://ijcai.org/proceedings/2022/fulltext/361/image_000005_670513c05a12f028961950aa6c5cced388b3e6323b090b20c195f00715b7852d.png) of the ∧ connective. Rule (5) defines the semantics of the X operator; in particular, note that when x0 is selected, then b1 must be selected too. Finally, rule (6) prevents that x1 is selected, because we are considering ℓ = 2 (and, hence, there is no subsequent time instant). The gray right box reports the rules encoding cost constraints. An atom weight(αi, w(α)) is included, for each propositional variable α and time instant i. A cost constraint states that the sum of the weights must not exceeded τ. It is immediate to check that there is no answer set (hence, trace) satisfying the above rules for τ<6. ✁ Finally, the ASP engine clingo [Gebser et al., 2018] is executed on the rewriting P(ϕ, ℓ, w) (see Figure 4). If no answer set with the desired length ℓ and weight is found, then we explore the successive level. The process ends if either we actually find a solution, or if ℓ exceeds the theoretical length thB(ϕ) of the longest path in the weighted transition graph, which is in general exponential w.r.t. ||ϕ||, and polynomially bounded in some syntactic fragments (cf. Theorem 3.5). ## 4.2 Experimental Results For the evaluation, we used a benchmark taken from the business process domain, namely a dataset of 109 satisfiable DECLARE formulas [van der Aalst et al., 2009] obtained by mining all DECLARE constraints that hold on a number of logs made available by the IEEE Task-Force on Process Mining (http://datacentrum.3tu.nl). The DECLARE constraints are then translated into their corresponding LTLf formulas [van der Aalst et al., 2009]. For each formula, we randomly generated the variable weights in the intervals [1, 5] and [1, 10] and considered all combinations of max and + operators, thus ending up with a dataset of 872 weighted settings. Moreover, for each weighted setting, we considered four different cost bounds obtained as follows: (i) we compute an arbitrary model π; (ii) we build a trace π′ whose length n is the same as π and such that π′i=V for each i ∈ {0, ..., n - 1}; (iii) we set the cost bounds to the 25%, 50%, 75% and 90% of v(π′ ). Clearly enough, for the reduced | 〈◦, ∗, w〉 | Solved formulas - 25% | Solved formulas - 50% | Solved formulas - 75% | Solved formulas - 90% | |----------------------|-------------------------|-------------------------|-------------------------|-------------------------| | 〈max, max, w[1,5] 〉 | 24 (0) | 24 (0) | 24 (0) | 33 (14) | | 〈max, max, w[1,10] 〉 | 24 (0) | 24 (0) | 25 (2) | 42 (25) | | 〈max, +, w[1,5] 〉 | 25 (2) | 96 (87) | 109 (105) | 109 (105) | | 〈max, +, w[1,10] 〉 | 26 (3) | 104 (94) | 109 (105) | 109 (107) | | 〈+, max, w[1,5] 〉 | 109 (106) | 109 (109) | 109 (109) | 109 (109) | | 〈+, max, w[1,10] 〉 | 109 (103) | 109 (109) | 109 (109) | 109 (109) | | 〈+, +, w[1,5] 〉 | 109 (108) | 109 (109) | 109 (109) | 109 (109) | | +, w[1,10] | 109 (108) | 109 (109) | 109 (109) | 109 (109) | 〈+, +, w[1,10] 〉 Table 1: Summary of results. Columns "Solved formulas" report the number of formulas for which WELTL computes a solution. For the remaining formulas, WELTL terminates in timeout. weight bounds, formulas quickly became unsatisfiable. Experiments have been carried out on a Intel CPU 2,4 GHz with 16GB RAM. Time and memory were limited to 600 seconds and 15GB, respectively. In particular, we first run WELTLbf (with 300 seconds of timeout); and if no solution has been returned, then we run WELTLdf (again with the same timeout). Table 1 reports a summary of the obtained results. For each valuation structure and each cost bound we report the number of formulas (out of 109) that are solved by WELTL within the time limit of 600 seconds. Each cell of the table reports inside the parenthesis the number of instances solved by WELTLbf during the first 300 seconds. All the instances solved by WELTLbf are satisfiable (i.e, a trace satisfying the cost bound has been found), while all the instances solved by WELTLdf during the last 300 seconds are unsatisfiable. To get further insights on WELTLbf , we report in Figure 6 the running times obtained on some instances. In particular, Figure 6.(a) reports the time to solve some satisfiable formulas when no weights are considered (i.e., standard satisfiability) and according to the valuation structure 〈max, +, w[1,5]〉 and the weight bounds 50% and 90%, respectively. The 22 formulas reported in the chart are those for which the model found at 90% did not meet the weight requirement at 50% and required to search for additional models. It can be noted that the time grows with the size of the formula and by lowering the cost bound. Figure 6.(b) reports the time required by WELTLbf to check the existence of models for 〈max,max,w[1,5]〉 and the bound 25% for 5 formulas, and by fixing different lengths ℓ in the encoding. The theoretical exponential dependency is nicely handled by the ASP engine. ## 5 Conclusion A framework to express LTLf properties in quantitative settings has been proposed and studied, based on the concept of valuation structures as mechanisms to equip each trace with a weight. While our approach departs from most of the quantitative LTL (and LTLf ) extensions proposed in the literature, a perspective similar to ours has been taken previously by [Lahijanian et al., 2015]-though in the specific context of temporal planning with partial satisfaction (and without providing any complexity analysis and systemprototype). In particular, a clear picture of the complexity issues arising when reasoning over weighted finite traces has been depicted and an efficient reasoning engine has been made available. On the theoretical level, instead, it remains open to study LTLf over valuation structures that are not monotone, by characterizing its computational properties and by defining and implementing computation algorithms. ## References 1. [Almagor et al., 2016] Shaull Almagor, Udi Boker, and Orna Kupferman. Formally reasoning about quality. Journal of the ACM, 63(3):24:1-24:56, 2016. 2. [Alur et al., 2001] Rajeev Alur, Kousha Etessami, Salva- tore La Torre, and Doron A. Peled. Parametric temporal logic for "model measuring". ACM Trans. on Computional Logics, 2(3):388-407, 2001. 3. [Baier et al., 2014] Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich. Weight monitoring with linear temporal logic: complexity and decidability. In Proc. of CSL-LICS, pages 11:1-11:10. ACM, 2014. 4. [Bouyer et al., 2014] Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In Proc. of CONCUR, pages 266-280, 2014. 5. [Brewka et al., 2011] Gerhard Brewka, Thomas Eiter, and Miroslaw Truszczynski. Answer set programming at a glance. Commun. ACM, 54(12):92-103, 2011. 6. [Camacho et al., 2018b] Alberto Camacho, Meghyn Bien- venu, and Sheila A. McIlraith. Finite LTL synthesis with environment assumptions and quality measures. In Proc. of KR, pages 454-463, 2018. 7. [de Alfaro et al., 2004] Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching metrics for quan- titative transition systems. In Proc. of ICALP, pages 97- 109, 2004. 8. [de Alfaro et al., 2005] Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. Model checking discounted temporal proper- ties. Theor. Comput. Sci., 345(1):139-170, 2005. 9. [De Giacomo and Vardi, 2013] Giuseppe De Giacomo and M. Y. Vardi. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In Proc. of IJCAI, pages 854-860. 10. [De Giacomo et al., 2014a] Giuseppe De Giacomo, Ric- cardo De Masellis, Marco Grasso, Fabrizio M. Maggi, and Marco Montali. Monitoring Business Metaconstraints Based on LTL and LDL for Finite Traces. In Proc. of BPM, pages 1-14, 2014. 11. [De Giacomo et al., 2014b] Giuseppe De Giacomo, Riccardi De Masellis, and Marco Montali. Reasoning on LTL on Fi- nite Traces: Insensitivity to Infiniteness. In Proc. of AAAI, pages 1027-1033, 2014. 12. [De Giacomo and Rubin, 2018] Giuseppe De Giacomo and Sasha Rubin. Automata-theoretic foundations of FOND planning for LTLf and LDLf goals. In Proc. of IJCAI, pages 4729-4735, 2018. 13. [De Giacomo and Vardi, 2015] Giuseppe De Giacomo and Moshe Y. Vardi. Synthesis for LTL and LDL on finite traces. In Proc. of IJCAI, pages 1558-1564, 2015. 14. [Droste and Rahonis, 2016] Manfred Droste and George Ra- honis. Weighted linear dynamic logic. In Proc. of EPTCS, volume 226, pages 149-163, 2016. 15. [Droste and Vogler, 2012] Manfred Droste and Heiko Vogler. Weighted automata and multi-valued logics over arbitrary bounded lattices. TCS, 418:14-36, 2012. 16. [Faber et al., 2011] Wolfgang Faber, Gerald Pfeifer, and Nicola Leone. Semantics and complexity of recursive aggregates in answer set programming. Artif. Intell., 175(1):278-298, 2011. 17. [Faella et al., 2008] Marco Faella, Axel Legay, and Mariëlle Stoelinga. Model checking quantitative linear time logic. E. N. in Theor. Comput. Sci., 220(3):61-77, 2008. 18. [Fionda and Greco, 2018] Valeria Fionda and Gianluigi Greco. LTL on finite and process traces: Complexity results and a practical reasoner. J. Artif. Intell. Res., 63:557-623, 2018. 19. [Gebser et al., 2018] Martin Gebser, Nicola Leone, Marco Maratea, Simona Perri, Francesco Ricca, and Torsten Schaub. Evaluation techniques and systems for answer set programming: a survey. In Proc. of IJCAI'18, pages 5450-5456, 2018. 20. [Kuperberg, 2014] Denis Kuperberg. Linear temporal logic for regular cost functions. Log. Methods Comput. Sci., 10(1), 2014. 21. [Kupferman and Lustig, 2007] Orna Kupferman and Yoad Lustig. Lattice automata. In Proc. of VMCAI, pages 199- 213, 2007. 22. [Kupferman et al., 2009] Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. From liveness to promptness. Formal Methods in System Design, 34(2):83-103, 2009. 23. [Lahijanian et al., 2015] Morteza Lahijanian, Shaull Al- magor, Dror Fried, Lydia E. Kavraki, and Moshe Y. Vardi. This time the robot settles for a cost: A quantitative ap- proach to temporal logic planning with partial satisfaction. In Proc. of AAAI, pages 3664-3671, 2015. 24. [Li et al., 2020] Jianwen Li, Geguang Pu, Yueling Zhang, Moshe Y. Vardi, and Kristin Y. Rozier. Sat-based explicit ltlf satisfiability checking. Artif. Intell., 289:103369, 2020. 25. [Mandrali, 2012] Eleni Mandrali. Weighted LTL with dis- counting. In Proc. of CIIA'12, pages 353-360, 2012. 26. [Montali et al., 2010] Marco Montali, Maja Pesic, Wil M. P. van der Aalst, Federico Chesani, Paola Mello, and Sergio Storari. Declarative specification and verification of ser- vice choreographiess. ACM Trans. on the Web, 4(1):3:1- 3:62, 2010. 27. [Pnueli, 1977] Amir Pnueli. The Temporal Logic of Pro- grams. In Proc. of FOCS, pages 46-57, 1977. 28. [van der Aalst et al., 2009] W.M.P. van der Aalst, M. Pesic, and H. Schonenberg. Declarative Workflows: Balancing Between Flexibility and Support. Computer Science -Re- search and Development, 23(2):99-113, 2009. 29. [Xiao et al., 2021] Shengping Xiao, Jianwen Li, Shufang Zhu, Yingying Shi, Geguang Pu, and Moshe Y. Vardi. On- the-fly synthesis for LTL over finite traces. In Proc. of AAAI, pages 6530-6537, 2021. 30. [Zhu et al., 2020] Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, and Moshe Y. Vardi. Ltlf synthesis with fairness and stability assumptions. In Proc. of AAAI, pages 3088-3095, 2020.