Linear Temporal Logic over finite tracesLT(L ) stands as a prominent and highly valuable formalism with application in various areas, including AI, process mining, and model checking among many others. The key reasoning task foLrTL is satisfiability checking, which amounts to verifying whether an input formula admits temporal models. In this paper we propose a novel approach to satisfiability checking based on Answer Set Programming (ASP). The idea is to encode in an ASP program the search for a finite state automaton that recognizes (a subset of) the language of LtThLe formula given in input. An experimental analysis demonstrates the viability of our approach.
various areas, including A3I,[4, 5, 6], process mining [7, 8], model checking9[], and many others. The
CEUR
ceur-ws.org of view is that our approach does not require an explicit construction of the-eanutiormeaton (which is exponential in the size of the input) to check satisfiability. Indeed, the need for such a construction is generally seen as detrimental to the use of automata-based decision processes, by requiring an exponential consumption of resources before any actual “reasoning” is performed. An additional benefit for our encoding is that it allows for structure sharing of sub-formulas; that is, when a sub -formula appears repeatedly in the formula,our encoding represents only one copy owfithin the encoding.
setting and thus improve the overall performance.
We briefly introduce the notions of linear temporal logic over finite traLcTeLs )( which are necessary for understanding our workL.TL [20] is a temporal logic over linear, discrete timepoints which is characterised by considering o nfinliyte traces; that is, models must have a final timepoint. Syntactically, it is equivalent to the well known LTL (over infinite ti1m8e]); t[hat isL,TL formulas are built, starting from a set of propositional formulas, through the grammar
∶∶= ∣ ¬ ∣ ∧ ∣ ∣ where ∈ . Briefly, LTL extends propositional logic with the “n ext)”a(nd “until” ( ) operators.
valuations. Formally,valuation is a set ⊆ temporal model is a finite sequenceℳ of valuations. that intuitively describes which variabletsrauree. A Definition 1 (satisfiability).
Let ℳ = 1, 2, … , be a temporal model. Satisfactioonf a formula at time , 1 ≤ ≤
(denoted by ℳ, ⊧ ) is defined inductively as follows: • if ∈ , then ℳ, ⊧ if ∈
; • ℳ, ⊧ ¬ if ℳ, ⊧ ̸ ; • ℳ, ⊧ ∧ • ℳ, ⊧ • ℳ, ⊧
if ℳ, ⊧ and ℳ, ⊧ ; if <
and ℳ, + 1 ⊧ ; and if there exists ℓ, ≤ ℓ ≤ such that (i) ℳ, ℓ ⊧ and (ii) for all ≤ < ℓ ℳ, ⊧ . ℳ satisfies (denoted as ℳ ⊧ ) if ℳ, 1 ⊧ . In that case, we say that is satisfiable.
is equivalent t o∨ ( ∧ ( )) until formula now, or wait until the next point in time.
requires that there is at least one successive timepoint. By ; in other words, we can decide to satisfy an
In the literature one can find other temporal constructors likweeatkhenext, which is true also in cases that no next timepoint exists, orevtehnetually andalways in the future operators. They can all be expressed in terms of the constructors that we 2u2s]e. [We choose to preserve the limited syntax to handle reasoning more efectively. Yet, we will use the disjun c∨t io∶n= ¬(¬ ∧ ¬ ) and the tautolog⊤y ∶= ∨ ¬ , where is any propositional variable for brevity. 3. Automata for LTL satisfiability
of an automaton which, intuitively, accepts the temporal models that satisfy it. Thus, an emptiness test of the automaton yields a decision procedure for satisfiability. Since our method is based on this construction, we briefly recall it here assuming a basic knowledge of finite automata (for the full details, we refer the interested reader t2o3][).
of is the smallest se(t) that containsusb() ; is closed under negation; and such th a t∈i(f) then ( ) ∈ () too. The formulas in() are suficient to verify satisfiability of the formu la.
timepoint, can also be characterised by the formula(s)(i)nthat it makes true at each point in time. Under this view, each timepoint can be associatedtytpoe,awhich is a maximal consistent subset(o)f which also preserves the semantics of . Formally, a set⊆ () is a type if the following conditions hold: • for every ∈ () , ∈ if ¬ ∉ ; • for every 1 ∧ 2 ∈ () , 1 ∧ 2 ∈ if { 1, 2} ⊆ ; • for every 1 ∨ 2 ∈ () , 1 ∨ 2 ∈ if { 1, 2} ∩ ≠ ∅ ; • for every 1 2 ∈ () , 1 2 ∈ if either 2 ∈ or { 1, ( 1 2)} ⊆ .
the temporal semantics of the operator. Two types1 and 2 are compatible if for every formula of the form in () it holds th a t∈ 1 if ∈ 2. Notice that this in particular means (by the maximality of types) tha¬t ∈ 1 if ¬ ∈ 2. We say that a type tiesrminal if it does not contain any formula of the form .
Definition 2 ( -automaton). The LTL formula defines the unlabelled NFA ∶= (, , , ) where • is the set of all types for ; • ∶= {( 1, 2) ∈ 2 ∣ 1 and 2 are compatible}; • ∶= { ∈ ∣ ∈ } ; and • ∶= { ∈ ∣ is terminal}.
model with two successive timepoints satisfying the formu la1sainnd in 2, respectively. To construct a model of , we need to find a path that goes from ainnitial type (in ) to afinal type (in ). Note that the condition for a type to belong—ttohat is, the lack of formulas of the f orm—means that it is safe to stop at that point, as no successive timepoint is needed to satisfy the constraints in the last observed type. Yet, one is noretquired to stop (other, longer models may exist as well).
Proposition 3 ([20]). The LTL formula is satisfiable if is non-empty.
In Section5, we present our approach which takes advantage of an ASP reasoner to decide satisfiability of LTL formulas by encoding (implicitly) the execution of a run of the automa.tIonna nutshell, the approach guesses the types satisfied at each timepoint, but in a way that satisfies all the constraints of the automaton. An important property of our encoding is that it allows for structure sharing, hence potentially reducing the encoding length of a formula. Before that, it is important to understand the main features of ASP.
In this section we recall syntax and semantics of ASP. We refer the interested reader to the specific literature for a more detailed accou1n2,t1[3].
ASP syntax. A variable is a string starting with uppercase lettecor.nAstant is an integer number or a string starting with lowercase letteart.oAmnis an expression of the for m( 1, ⋯ , ) where is a predicate of arit yand 1, ⋯ , are terms. An atom isground if it contains no variable.litAeral is a atom or its negatio n where denotes negation as failure. A lit eirsanlegative if it is of the form , otherwise it ipsositive. The complement of positive (resp. negative) lite=ral (resp. = ), denoted by , is the liter a l (resp. ). A (normal)rule is an expression of the formℎ ← 1, ⋯ , where 1, ⋯ , is a conjunction of literals, referred to as bo≥d0y,, andℎ is an atom. All variables in a rule must occur in some positive literal of the body (i.e., are saf2e4c])f.r.A[ fact is a rule with an empty body (i.e. = 0 ). A constraint is a rule with an empty head that is a shorthand for rule ← 1, ⋯ , , , where is a standard ground atom not occurring anywhere elpsero.gAram is a ifnite set of rules.
Stable Models Semantics. Given a program , theHerbrand Universe denotes the set of constants in ; theHerbrand Base denotes the set of standard ground atoms that can be obtained from predicates in and constants i n. Given a rule ∈ , () denotes the set of possible rule instantiations that can be obtained by replacing variablewsinth constants i n. The ground instantiation of the program , denoted b y() , is the union of ground instantiations of rul e.sAinn interpretation is a subset of . Given an interpretati o,na positive (resp. negative) literaisltrue w.r.t. , if ∈ (resp. ∉ ); it is false i f∉ (resp. ∈ ). A conjunction of literals is true w .ri.fta.ll the literals are true w.r.t. . An interpretatio nis amodel of if for each ∈ () , the head of is true whenever the body of is true. Given a program and an interpretatio,nthe (Gelfond-Lifschitz) reduc1t3][, , is the program obtained from() by (i) removing all those rules having in the body a false negative literal w.r. t,. and (ii) removing negative literals from the body of remaining rules. Given a pr ogram and a mode l, is astable model or answer set of if there is no ′ ⊂ such tha t′ is a model o f . is coherent if it admits at least one answer set, otherwise it is incoherent.
particular, we first describe how to encode the input and then we describe the satisfiability checking encoding. 5.1. Input Data
/1 , /2 , /2 , /3 , /3 , and/3 .
In particular, each distinct sub-formula has to be uniquely identified by,wahnich is declared by facts of the for m() . Atoms of the form(, 1, 2) and(, 1, 2), encode sub-formulas defined as the conjunction or disjunction, respectively of the two sub-formulas identifie1d, baynd 2. Atoms of the form(, 1) models the negation of a sub-formula identified b1y, by means of a sub-formula identified by . We assume that both( 1, 2) and( 2, 1) are part of the input whenever 1 is the negation of2. Atoms of the form(, 1) encode sub-formulas of the form 1, where the sub-formul a 1 is identified by 1, and atoms of the for m(, 1, 2) denote sub-formulas of the form 1 2, where 1, and 2 are the identifiers of 1 and 2, respectively. The atomℎ() encodes the input formu la, where is the identifier of the outermost sub-formula. Runs of the automaton of leng tahre represented using atoms of the for(m) , where 1 ≤ ≤ . Given a formula , all these facts can be obtained by decomposing, botto mi-nutp,o diferent sub-formulas, going from propositional variables to the outermost operTahtuosr,. an input formul a can be encoded as a set of facts of linear size w.r.t. the number of subformula.s of Example 4. The formula = ¬() ∧ (( ) )
is encoded as:
()
(3)
(7)
(1, )
(9, 3)
(8, 4)
( )
(4)
(8)
(2, )
(5, )
(10, 9)
(
encode the sub-formula 10 ∶ ¬ 9 1 ∶ (, ) ← (), ( ), ( 1, ), (, 1) 2 ∶ (, 1) ← (), ( ), ( 1, ), (, ) Note that 4 is the outermost sub-formula after reconstructing the formula and so ℎ(4) encodes . In addition, note that 9 and 10 (along with most of the negations) are not strictly sub-formulas of but they must be included to guarantee the construction of a type from the set () as defined in Section 3. 5.2. Encoding In this section we present the encoding that models the satisfiability checLkToLf afonrmula. Notably, this encoding is highly general and does not depend on the specific formula being evaluated. Therefore, given any formul a and its corresponding encoding as ASP facts (as outlined in the previous section), the encoding can be directly reused to verify the satisfiabili t.yIonforder to better present the proposed encoding, in what follows we refer to sub-formulas by means of their identifier. The proposed encoding exploits the well-known Guess&Check paradi2g5m]i[n which the Guess part tries to guess maximal subset of formulae, by assigning to each state either a fo rmourliats negatio n1 .
Initial State. To ensure that state 1 (the first state in the run) contains the the outermost sub-formula denoted b y ℎ( ) we use the rule:
(1, ) ← ℎ( ).
Final and active states. A final state, which contains no-formula, should be observed within the ifrst states of the run. This is enforced through the rules: 1 ∶ 2 ∶ 3 ∶ 4 ∶ 5 ∶ ℎ () ← () ← _ ← (, ), ( , 1) (), ℎ () () ← () ← (), (), >= _ Rule 1 defines atoms of the formℎ () . These denote all those states containing at least one sub-formula, ∶ 1 . Rule 2 encodes the final states as atoms of the f o(rm) . A stat e is final if does not contain sub-formula of the f o 1rm (i.e. ℎ () ). Finally, rules3 and 4 impose that at least one final state exists. Moreover, since the proposed encoding search for a run of atstmaotsets, then the required conditions must be verified for all the states up to the actual final one. Thus, we mark as active, by means of rule 5 that derives an atom() , for each stat ethat is less or equal than the actual last st at(ie.e. () ).
Type Condition. We must still impose that each st1a≤te ≤ ℓ (where ℓ is the first observed final state) is a type. A sta ties a type if the following conditions hold for all formula(s) in
4. contains the formu la= if and only if at least one of the following conditions holds:
either or 1 ∶ ¬ to .
Condition2 is ensured by the constraints: 1 ∶ ← (, ), ( , , ), (, ), () 2 ∶ ← (, ), ( , , ), (, ), () 3 ∶ ← (, ), (, ), ( , , ), (, ), () 1 ∶ ← (, ), ( , , ), (, ), (, ), () 2 ∶ ← (, ), ( , , ), (, ), () 3 ∶ ← (, ), ( , , ), (, ), ()
≤ ℓ contains and does not conta in(resp. ). Constraint3 discards those answer sets in which a stat e≤ ℓ contains bot h and , and does not conta in.
contai n , but contain neithernor . Constraint2 (resp. 3) imposes that it is not possible that a state ≤ ℓ contains (resp. ) and does not conta in.
1 ∶ _(, , , ) ← ( , , ), (, ) 2 ∶ _(, , , ) ← ( , , ), (, ), ( 1, ), (, 1) Roughly, for each formula∶ , if there exists a statecontaining then conditio4na is satisfied; thus, rule 1 derives _(, , , ) . On the other hand, if there exists a s tactoentaining bot h and a formul a1 ∶ then conditio4nb is satisfied and so rule 2 derives _(, , , ) . Thus, condition4 is ensured by the constraints: 1 ∶ ← (, ), ( , , ), 2 ∶ ← (, ), _(, , , ), () _(, , , ), ()
cannot be added to,while, constrain t2, imposes that it is not possible t hacatn be added to the state but does not contain.
2. a state contains a formul 1a ∶ ¬( ) if is not the final state and the st a+t1e contains if is not the final state and the st a+t1e contains¬
1 ∶ ← (, ), ( , 1), 1 = + 1, (1), (1, 1), () 2 ∶ ← (, ), ( , 1), 1 = + 1, (1), (1, 1), () Basically, for every formul a∶ 1 , 1 imposes that it is not possible for a s tattoecontain if 1 is not assigned at st a+te1 . On the other han d2, imposes that it is not possible that there exists a state + 1 containing a formu l1a such that the sta tdeoes not contain the form ul∶a 1 . Condition2 is ensured by the constraints: 3 ∶ ← ( , 1), ( 1, 2), ( 3, 2), (, ),
1 = + 1, (1), (1, 3), () 4 ∶ ← ( , 1), ( 1, 2), ( 3, 2), (1, 3),
1 = + 1, (), (, ), () Intuitively, le∶t ¬ 1 , 1 ∶ 2 , and 3 ∶ ¬ 2 , 3 imposes that it is not possible that there exists a stat e containing the formula(i.e. ¬( 2) ), and the formul a3 (i.e. ¬ 2 ) is not assigned at state + 1 . On the other han d4, imposes that it is not possible that there exists a +st1atceontaining the formula 3 (i.e. ¬ 2 ), and the sta tedoes not contain the form ul(ai.e. ¬( 2) ).
denote the ASP program described in Secti5o.2n.
Proposition 5. An LTL formula is satisfiable if there exists an integer > 0 such that Π ∪ (, ) coherent. is
Implementation. By exploiting the encoding proposed in this section, it is possible to construct an
pseudo-code of such a procedure.
Intuitively, starting wi=th1 it is possible to incremetally search for an accepting run that uses at most timepoints (each tagged with a state). Thus, at each iter at=ioΠn∪if(, ) is coherent Algorithm 1 Decide-LTL
Input : An LTL formula 1 begin 2 = 1 3 while ≤ 2 ‖‖+1 do 4 := Π ∪ (, ) 5 if is coherent then 6 return SAT 7 return UNSAT
)
) Response (() ) RespondedExistence(() then we found a witness of satisfiability o.fConversely, if we were not able to found such a witness with up to2‖‖+1
where ‖‖ denotes the number of symbols, excluding parenthesis, appearin g, in then is unsatisfiability. This upper bound is an easy consequence of the definition of a type. Indeed, from Section3 it can be seen that the number of types is bounded2‖b‖+y1 and that in the worst case, a successful run from an initial to a final type will traverse all types once. In practice, many state-of-the-art proposa2l2s,[26, 27] operate following a similar strategy (i.e. incremental expanding horizon), and are efective whenever the formula admits temporal models with a reasonably short length. We implemented such an approach into a Python prototype that takes as input a ,formula at each iteration compu t(e, s)
, and uses the ASP solvecrlingo [28] for verifying the coherence Π ∪ (, )
.
We now present an empirical evaluation aimed at investigating the viability of the approach which we have proposed in practical settings.
marks commonly used in the literature to evaluate systemLsTfLorsatisfiability checking2[2]. Specifically, each benchmark corresponds to a distLinTcLt pattern formula as listed in Ta1b.lIet is worth noting that these formulas are expressed in the native synLtTaLx syntax in 2[2], but the formulas are equivalent. o,fwhich difers from the extended
thus these can be considered as representative of a concrete applicaLtTioLn. oTfhe remaining three, instead, are specific patterns of formulas suitable for a scalability analysis on a synthetic benchmark.
to 200. For benchmark(, )
we considered two values offor each value of: /2 and(3 × )/2 , respectively. As a result we obtained a benchmark suite comprising 320 formulas.
(a) Overall Comparison (b) Comparison on(, )
approach, implemented by running the ASP solvcelirngo [28]; (ii) theaaltaf system implementing (Conflict-Driven LTL Satisfiability Checking)2[2]; (iii) theblack system [27], in two diferent settings: (a) the standard version denotedblaasck; (b) the semi-decisional one denotedbalasck-semi.
with Intel(R) Core(TM) i7-8850H CPU @ 2.60GHz, running macOS 14.5 (23F79) (Darwin Kernel Version 23.5.0). Memory and time were limited to 2GB and 600s respectively. 1https://github.com/MazzottaG/LTLToAutomata.git
the execution time for each system ordered from best to worst. Specifically, in a cactus plot, instances are sorted by their execution time, and a po(,in)tindicates that a solver can solv e-theinstance within seconds.
solving every instance within few seconds. Specificalalsyp,-based and the other compared systems can solve all instances of the benchmarks referring to Declare patter(n)s (i.e,. ,() , () , and() ) almost instantaneously (less t0h.5anseconds per instance) even for larger values o(ufp to 1000), demonstrating a significant positive outcome for declarative process mining, which is an important application for LT Lreasoning.
benchmarks (i.e.,() and() ), all the compared systems are instantaneous, similarly to the Declare patterns. However, the last benchma(r,k), , proved to be more challenging than the previous ones. Figure (1b) reports the execution times of the compared systems on such benchmarks. Our approach exhibits a negligible overhead on very simple instances (less than 0.5 seconds) due to the
formulas, where the execution is orders of magnitude smaller than compared systems.
30]. These translations conveLrTtL semantics into First Order Logic and Monadic Second Order logic, and then uses tools like MON3A1][ to obtain the symbolic DFA. However, these approaches require the full materialization of the automata, which is exponential w.r.t. the size of the input formula. On the contrary, our approach incrementally searches for an accepting run of the underlying automata without materializing it.
uses SAT-solving to create a transition system foLrTaLn formula, turning satisfiability checking into a path-search problem. Additionally, the introduced CDLSC (Conflict-Driven LTLf Satisfiability Checking) algorithm uses SAT solver data for both satisfiable and unsatisfiable results. Another strategy for transforming anLTL formula into propositional formulas (c2fr6.][) can be used to verify the existence of a temporal model of length at m,ousnttil the theoretical upper bound foisrreached.
this approach the underlying tableau tree is built in a breadth-first way, by means of Boolean formulae encoding the possible tableau branches up to a given de,pwthhich is increased at each step. All the
provides a general uniform ASP encoding based o-nautomata that can be used for evaluating any
proposed [35]. In this approach a satisfiability checke2r6][ is used to verify the satisfiability of the input formula, and then an ASP solver searches for optimal models. While our first-order constraints resemble the variable-free ones in their model-checker program, our goal difers as we directly determine the satisfiability of aLnTL formula, whereas their approach relies on an initial satisfiability checker.
37]. The approach proposed in 3[8, 39] leverages algorithms for minimal unsatisfiable subprogram enumeration 4[0] applied to an ASP encoding for bounded satisfiabili4t1y].[
net and its behavioral requirements (in LTL) can be translated into a logic program, so bounded model checking amounts to computing its stable models. Moreover, recent applications of ASP to declarative process mining have been proposed4[3, 44, 45]. However, in these works the authors do not address the problem of satisfiabilty of LTLbut targeted related tasks such as Conformance Checking that indeed falls in lower complexity classes.
The extensions of ASP for modeling temporal properties are also related. The styeslitnegmo [46] extendsclingo by adding to ASP future and past temporal operators and incrementally solving the corresponding temporal logic programs usinclgingo’s multi-shot solving interface. Roughly, LTL relates to SAT in the same way the temporal extension supportteedlinbgyo relates to ASP. Thus, the formalism implemented bytelingo is more expressive thanLTL , and so, one could even envision modeling our task itnelingo. However, the goal of this paper is to provide an eficient encodingLToLf in plain ASP. Finally, we also mention methods for modeling temporal constraints in ASP that are based on alternating automa4t7a].[
area is being dominated by logic-based approach2e2s, 2[6, 27], which are based on propositional SAT solving.
based approach implemented in ASP. The resulting approach is based on a more direct modeling of the problem that does not require the input formula to be highly pre-processed or rendered a normal form; moreover, it gives as a byproduct a meaningful witness of the satisfiability outcome. A first experimental analysis demonstrates that our approach is also viable in practice, delivering good performance, comparable to the state-of-the-art CDSLC approach on declarative process mining benchmarks.
the one hand, the generation of witnesses of satisfiability in our approach lays a foundation for the development of explainability techniqueLsTiLn reasoning. On the other hand, this initial encoding in ASP presents potential for optimizations at both the encoding and system levels. Indeed, the usage of novel grounding-less evaluation techniq4u8e,s49[, 50] could beneficial for obtaining even better performances.
B29J24000680005, and MUR under projects: PNRR FAIR - Spoke 9 - WP 9.1 CUP H23C22000860006, Tech4You CUP H23C22000370006, and PRIN PINPOINT CUP H23C22000280006 and H45E21000210001.
[3] G. De Giacomo, F. M. Maggi, A. Marrella, S. Sardiña, Computing trace alignment against declarative process models through planning, in: ICAPS, 2016, pp. 367–375. [4] G. De Giacomo, M. Y. Vardi, Automata-theoretic approach to planning for temporally extended goals, in: ECP, volume 1809 oLfNCS, 1999, pp. 226–238. [5] F. Bacchus, F. Kabanza, Planning for temporally extended goals, Ann. Math. Artif. Intell. 22 (1998) 5–27. [6] D. Calvanese, G. De Giacomo, M. Y. Vardi, Reasoning about actions and planning in LTL action theories, in: KR, 2002, pp. 593–602. [7] G. De Giacomo, M. Dumas, F. M. Maggi, M. Montali, Declarative process modeling in BPMN, in:
CAiSE, volume 9097 ofLNCS, 2015, pp. 84–100. [8] A. Cecconi, G. De Giacomo, C. D. Ciccio, F. M. Maggi, J. Mendling, Measuring the interestingness of temporal logic behavioral specifications in process mining, Inf. Syst. 107 (2022) 101920. [9] Y. Tsay, M. Y. Vardi, From linear temporal logics to Büchi automata: The early and simple principle, in: Model Checking, Synthesis, and Learning, volume 13030LNoCfS, 2021, pp. 8–40. [10] S. Zhu, G. Pu, M. Y. Vardi, First-order vs. second-order encodings for \textsc ltl_f -to-automata translation, in: Theory and Applications of Models of Computation - 15th Annual Conference,
684–705. [11] Handbook of Satisfiability - Second Edition, volume 336Froofntiers in Artificial Intelligence and
Applications, 2021. [12] G. Brewka, T. Eiter, M. Truszczynski, Answer set programming at a glance, Com. ACM 54 (2011) 92–103. [13] M. Gelfond, V. Lifschitz, Classical negation in logic programs and disjunctive databases, New
Generation Comput. 9 (1991) 365–386. [14] Y. Lierler, M. Maratea, F. Ricca, Systems, engineering environments, and competitions, AI Magazine 37 (2016) 45–52. [15] M. Alviano, C. Dodaro, M. Maratea, Nurse (re)scheduling via answer set programming, Intelligenza
Artificiale 12 (2018) 109–124. [16] G. Grasso, S. Iiritano, N. Leone, V. Lio, F. Ricca, F. Scalise, An asp-based system for team-building in the gioia-tauro seaport, in: PADL, volume 5937Leocfture Notes in Computer Science, Springer, 2010, pp. 40–42. [17] V. Barbara, M. Guarascio, N. Leone, G. Manco, A. Quarta, F. Ricca, E. Ritacco, Neuro-symbolic AI for compliance checking of electrical control panels, Theory Pract. Log. Program. 23 (2023) 748–764. [18] A. Pnueli, The temporal logic of programs, in: Proc. of 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46–57. [19] J. R. Büchi, On a Decision Method in Restricted Second Order Arithmetic, New York, NY, 1990, pp.
425–435. [20] G. De Giacomo, M. Y. Vardi, Linear temporal logic and linear dynamic logic on finite traces, in:
pp. 854–860. [21] C. Y. Lee, Representation of switching circuits by binary-decision programs, The Bell System
Technical Journal 38 (1959) 985–999. [22] J. Li, G. Pu, Y. Zhang, M. Y. Vardi, K. Y. Rozier, SAT-based explicit LTLf satisfiability checking,
Artificial Intelligence 289 (2020) 103369. [23] J. E. Hopcroft, J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, 1979. [24] S. Ceri, G. Gottlob, L. Tanca, Logic Programming and Databases, Surveys in computer science, 1990. [25] T. Eiter, G. Gottlob, On the computational cost of disjunctive logic programming: Propositional case, Ann. Math. Artif. Intell. 15 (1995) 289–323. [26] V. Fionda, G. Greco, LTL on finite and process traces: Complexity results and a practical reasoner,
J. Artif. Intell. Res. 63 (2018) 557–623.
June 3-7, 2019, Proceedings, volume 11481 oLfNCS, 2019, pp. 256–269. [47] P. Cabalar, M. Diéguez, S. Hahn, T. Schaub, Automata for dynamic answer set solving: Preliminary report, in: Proceedings of the International Conference on Logic Programming 2021 Workshops co-located with the 37th International Conference on Logic Programming (ICLP 2021), Porto,
[48] G. Mazzotta, F. Ricca, C. Dodaro, Compilation of aggregates in ASP systems, in: AAAI, AAAI
Press, 2022, pp. 5834–5841. [49] C. Dodaro, G. Mazzotta, F. Ricca, Compilation of tight ASP programs, in: ECAI 2023 - 26th
372 of Frontiers in Artificial Intelligence and Applications , 2023, pp. 557–564. [50] C. Dodaro, G. Mazzotta, F. Ricca, Blending Grounding and Compilation for Eficient ASP Solving, in: Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, 2024, pp. 317–328. URL:https://doi.org/10.24963/kr.2024/3.0doi:10.24963/kr. 2024/30.