Automata for dynamic answer set solving: Preliminary report Pedro Cabalar1 , Martín Diéguez2 , Susana Hahn3 and Torsten Schaub3 1 University of Corunna, Spain 2 University of Angers, France 3 University of Potsdam, Germany Abstract We explore different ways of implementing temporal constraints expressed in an extension of Answer Set Programming (ASP) with language constructs from dynamic logic. Foremost, we investigate how automata can be used for enforcing such constraints. The idea is to transform a dynamic constraint into an automaton expressed in terms of a logic program that enforces the satisfaction of the original constraint. What makes this approach attractive is its independence of time stamps and the potential to detect unsatisfiability. On the one hand, we elaborate upon a transformation of dynamic formulas into alternating automata that relies on meta-programming in ASP. This is the first application of reification applied to theory expressions in gringo. On the other hand, we propose two transformations of dynamic formulas into monadic second-order formulas. These can then be used by off-the-shelf tools to construct the corresponding automata. We contrast both approaches empirically with the one of the temporal ASP solver telingo that directly maps dynamic constraints to logic programs. Since this preliminary study is restricted to dynamic formulas in integrity constraints, its implementations and (empirical) results readily apply to conventional linear dynamic logic, too. Keywords Dynamic Answer Set Programming, Linear Dynamic Logic, Alternating Finite Automaton on Words 1. Introduction Answer Set Programming (ASP [1]) has become a popular approach to solving knowledge- intense combinatorial search problems due to its performant solving engines and expressive modeling language. However, both are mainly geared towards static domains and lack native support for handling dynamic applications. Rather change is accommodated by producing copies of variables, one for each state. This does not only produce redundancy but also leaves the ASP machinery largely uninformed about the temporal structure of the problem. This preliminary work explores alternative ways of implementing temporal (integrity) con- straints in (linear) Dynamic Equilibrium Logic (DEL; [2, 3]) by using automata [4]. On the one hand, DEL is expressive enough to subsume more basic systems, like (linear) Temporal Equilibrium Logic [5, 6] or even its metric variant [7]. On the other hand, our restriction to integrity constraints allows us to draw on work in conventional linear dynamic and temporal 14th Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP’21) " cabalar@udc.es (P. Cabalar); martin.dieguezlodeiro@univ-angers.fr (M. Diéguez); hahnmartinlu@uni-potsdam.de (S. Hahn); torsten@uni-potsdam.de (T. Schaub) © 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) logic (cf. Proposition 1). Although this amounts to using dynamic formulas to filter “stable temporal models” rather than to let them take part in the formation of such models, it allows us to investigate a larger spectrum of alternatives in a simpler setting. Once fully elaborated, we plan to generalize our approach to the full setting. Moreover, we are interested in implementing our approach by means of existing ASP systems, which motivates our restriction to the finite trace variant of DEL, called DEL𝑓 . In more detail, Section 2 to 4 lay the basic foundations of our approach by introducing DEL, some automata theory, and a translation from dynamic formula into alternating automata. We then develop and empirically evaluate three different approaches. First, the one based on alternating automata from Section 4. This approach is implemented entirely in ASP and relies on meta-programming. As such it is the first application of gringo’s reification machinery to user defined language constructs (defined by a theory grammar; cf. [8]). For the second approach we employ our two alternative transformations of dynamic formulas into monadic second order (MSO [9]) formulas proposed in [10], namely Monadic Second Order Encoding and Standard Translation. These formulas can then be passed to the off-the-shelf automata construction tool MONA [11] that turns them into deterministic automata. And finally, the approach of telingo [12, 13], transforming each dynamic constraint directly into a logic program. All three approaches result in a program that allows us to sift out “stable temporal models” satisfying the original dynamic constraints. Usually, these models are generated by another logic program, like a planning encoding and instance. 2. Linear Dynamic Equilibrium Logic Given a set 𝒫 of propositional variables (called alphabet), dynamic formulas 𝜙 and path expres- sions 𝜌 are mutually defined by the pair of grammar rules: 𝜙 ::= 𝑎 | ⊥ | ⊤ | [𝜌] 𝜙 | ⟨𝜌⟩ 𝜙 𝜌 ::= τ | 𝜙? | 𝜌 + 𝜌 | 𝜌 ; 𝜌 | 𝜌* . This syntax is similar to the one of Dynamic Logic (DL; [14]) but differs in the construction of atomic path expressions: While DL uses a separate alphabet for atomic actions, LDL has a single alphabet 𝒫 and the only atomic path expression is the (transition) constant τ ̸∈ 𝒫 (read as “step”). Thus, each 𝜌 is a regular expression formed with the constant τ plus the test construct 𝜙? that may refer to propositional atoms in the (single) alphabet 𝒫. As with LDL [15], we sometimes use a propositional formula 𝜑 as a path expression and let it stand for (𝜑?; τ). This means that the reading of ⊤ as a path expression amounts to (⊤?; τ) which is just equivalent to τ, as we see below. Another abbreviation is the sequence of 𝑛 repetitions of some expression def def 𝜌 defined as 𝜌0 = ⊤? and 𝜌𝑛+1 = 𝜌; 𝜌𝑛 . The above language allows us to capture several derived operators, like the Boolean and temporal ones [3]: def def 𝜙 ∧ 𝜓 = ⟨𝜙?⟩ 𝜓 𝜙 ∨ 𝜓 = ⟨𝜙? + 𝜓?⟩ ⊤ def def 𝜙 → 𝜓 = [𝜙?] 𝜓 ¬𝜙 = 𝜙 → ⊥ ◦𝜙 def = ⟨τ⟩ 𝜙 ◦̂︀𝜙 def = [τ] 𝜙 def F = [τ] ⊥ def def ♢𝜙 = ⟨τ* ⟩ 𝜙 □𝜙 = [τ* ] 𝜙 def def 𝜙 U 𝜓 = ⟨(𝜙?; τ)* ⟩ 𝜓 𝜙 R 𝜓 = (𝜓 U (𝜙 ∧ 𝜓)) ∨ □𝜓 All connectives are defined in terms of the dynamic operators ⟨·⟩ and [·] . This involves the Booleans ∧, ∨, and →, among which the definition of → is most noteworthy since it hints at the implicative nature of [·] . Negation ¬ is then expressed via implication, as usual in HT. Then, ⟨·⟩ and [·] also allow for defining the future temporal operators F, ◦, ◦ ̂︀ , ♢, □, U, R, standing for final, next, weak next, eventually, always, until, and release. A formula is propositional, if all its connectives are Boolean, and temporal, if it includes only Boolean and temporal ones. As usual, a (dynamic) theory is a set of (dynamic) formulas. For the semantics, we let [𝑎..𝑏] stand for the set {𝑖 ∈ N | 𝑎 ≤ 𝑖 ≤ 𝑏} and [𝑎..𝑏) for {𝑖 ∈ N | 𝑎 ≤ 𝑖 < 𝑏} for 𝑎 ∈ N and 𝑏 ∈ N ∪ {𝜔}. A trace of length 𝜆 over alphabet 𝒫 is then defined as a sequence (𝐻𝑖 )𝑖∈[0..𝜆) of sets 𝐻𝑖 ⊆ 𝒫. A trace is infinite if 𝜆 = 𝜔 and finite otherwise, that is, 𝜆 = 𝑛 for some natural number 𝑛 ∈ N. Given traces H = (𝐻𝑖 )𝑖∈[0..𝜆) and H′ = (𝐻𝑖′ )𝑖∈[0..𝜆) both of length 𝜆, we write H ≤ H′ if 𝐻𝑖 ⊆ 𝐻𝑖′ for each 𝑖 ∈ [0..𝜆); accordingly, H < H′ iff both H ≤ H′ and H ̸= H′ . Although DHT shares the same syntax as LDL, its semantics relies on traces whose states are pairs of sets of atoms. An HT-trace is a sequence of pairs (⟨𝐻𝑖 , 𝑇𝑖 ⟩)𝑖∈[0..𝜆) such that 𝐻𝑖 ⊆ 𝑇𝑖 ⊆ 𝒫 for any 𝑖 ∈ [0..𝜆). As before, an HT-trace is infinite if 𝜆 = 𝜔 and finite otherwise. The intuition of using these two sets stems from HT: Atoms in 𝐻𝑖 are those that can be proved; atoms not in 𝑇𝑖 are those for which there is no proof; and, finally, atoms in 𝑇𝑖 ∖ 𝐻𝑖 are assumed to hold, but have not been proved. We often represent an HT-trace as a pair of traces ⟨H, T⟩ of length 𝜆 where H = (𝐻𝑖 )𝑖∈[0..𝜆) and T = (𝑇𝑖 )𝑖∈[0..𝜆) such that H ≤ T. The particular type of HT-traces that satisfy H = T are called total. The overall definition of DHT satisfaction relies on a double induction. Given any HT-trace M = ⟨H, T⟩, we define DHT satisfaction of formulas, namely, M, 𝑘 |= 𝜙, in terms of an accessibility relation for path expressions ‖ 𝜌 ‖M ⊆ N2 whose extent depends again on |= by double, structural induction. Definition 1 (DHT satisfaction; [3]). An HT-trace M = ⟨H, T⟩ of length 𝜆 over alphabet 𝒫 satisfies a dynamic formula 𝜙 at time point 𝑘 ∈ [0..𝜆), written M, 𝑘 |= 𝜙, if the following conditions hold: 1. M, 𝑘 |= ⊤ and M, 𝑘 ̸|= ⊥ 2. M, 𝑘 |= 𝑎 if 𝑎 ∈ 𝐻𝑘 for any atom 𝑎 ∈ 𝒫 3. M, 𝑘 |= ⟨𝜌⟩ 𝜙 if M, 𝑖 |= 𝜙 for some 𝑖 with (𝑘, 𝑖) ∈‖ 𝜌 ‖M ′ 4. M, 𝑘 |= [𝜌] 𝜙 if M′ , 𝑖 |= 𝜙 for all 𝑖 with (𝑘, 𝑖) ∈‖ 𝜌 ‖M for both M′ = M and M′ = ⟨T, T⟩ where, for any HT-trace M, ‖ 𝜌 ‖M ⊆ N2 is a relation on pairs of time points inductively defined as follows. def 5. ‖ τ ‖M = {(𝑘, 𝑘 + 1) | 𝑘, 𝑘 + 1 ∈ [0..𝜆)} def 6. ‖ 𝜙? ‖M = {(𝑘, 𝑘) | M, 𝑘 |= 𝜙} def 7. ‖ 𝜌1 + 𝜌2 ‖M = ‖ 𝜌2 ‖M ∪ ‖ 𝜌2 ‖M def 8. ‖ 𝜌1 ; 𝜌2 ‖M = {(𝑘, 𝑖) | (𝑘, 𝑗) ∈‖ 𝜌1 ‖M and (𝑗, 𝑖) ∈‖ 𝜌2 ‖M for some 𝑗} def ⋃︀ 9. ‖ 𝜌* ‖M = 𝑛≥0 ‖ 𝜌𝑛 ‖M An HT-trace M is a model of a dynamic theory Γ if M, 0 |= 𝜙 for all 𝜙 ∈ Γ. We write def DHT(Γ, 𝜆) to stand for the set of DHT models of length 𝜆 of a theory Γ, and define DHT(Γ) = 𝜔 𝜆=0 DHT(Γ, 𝜆), that is, the whole set of models of Γ of any length. A formula 𝜙 is a tautology ⋃︀ (or is valid), written |= 𝜙, iff M, 𝑘 |= 𝜙 for any HT-trace M and any 𝑘 ∈ [0..𝜆). The logic induced by the set of all tautologies is called (Linear) Dynamic logic of Here-and-There (DHT for short). We distinguish the variants DHT𝜔 and DHT𝑓 by restricting DHT to infinite or finite traces, respectively. We refrain from giving the semantics of LDL [15], since it corresponds to DHT on total traces ⟨T, T⟩ [3]. Letting T, 𝑘 |= 𝜙 denote the satisfaction of 𝜙 by a trace T at point 𝑘 in LDL, we have ⟨T, T⟩, 𝑘 |= 𝜙 iff T, 𝑘 |= 𝜙 for 𝑘 ∈ [0..𝜆). Accordingly, any total HT-trace ⟨T, T⟩ can be seen as the LDL-trace T. As above, we denote infinite and finite trace variants as LDL𝜔 and LDL𝑓 , respectively. The work presented in the sequel takes advantage of the following result that allows us to treat dynamic formulas in occurring in integrity constraints as in LDL: Proposition 1. For any HT-trace ⟨H, T⟩ of length 𝜆 and any dynamic formula 𝜙, we have ⟨H, T⟩, 𝑘 |= ¬¬𝜙 iff T, 𝑘 |= 𝜙, for all 𝑘 ∈ [0..𝜆). We now introduce non-monotonicity by selecting a particular set of traces called temporal equilibrium models [3]. First, given an arbitrary set S of HT-traces, we define the ones in equilibrium as follows. A total HT-trace ⟨T, T⟩ ∈ S is an equilibrium model of S iff there is no other ⟨H, T⟩ ∈ S such that H < T. If this is the case, we also say that trace T is a stable model of S. We further talk about temporal equilibrium or temporal stable models of a theory Γ when S = DHT(Γ). We write DEL(Γ, 𝜆) and DEL(Γ) to stand for the temporal equilibrium models of DHT(Γ, 𝜆) and DHT(Γ) respectively. Note that stable models in DEL(Γ) are also LDL-models of Γ. Besides, as the ordering relation among traces is only defined for a fixed 𝜆, the ⋃︀𝜔 set of temporal equilibrium models of Γ can be partitioned by the trace length 𝜆, that is, 𝜆=0 DEL(Γ, 𝜆) = DEL(Γ). (Linear) Dynamic Equilibrium Logic (DEL; [2, 3]) is the non-monotonic logic induced by temporal equilibrium models of dynamic theories. We obtain the variants DEL𝜔 and DEL𝑓 by applying the corresponding restriction to infinite or finite traces, respectively. As a consequence of Proposition 1, the addition of formula ¬¬𝜙 to a theory Γ enforces that every temporal stable model of Γ satisfies 𝜙. With this, we confine ourselves in Section 4 to LDL𝑓 rather than DEL𝑓 . In what follows, we consider finite traces only. 3. Automata A Nondeterministic Finite Automaton (NFA; [4]) is a tuple (Σ, 𝑄, 𝑄0 , 𝛿, 𝐹 ), where Σ is a finite nonempty alphabet, 𝑄 is a finite nonempty set of states, 𝑄0 ⊆ 𝑄 is a set of initial states, 𝛿 : 𝑄 × Σ → 2𝑄 is a transition function and 𝐹 ⊆ 𝑄 a finite set of final states. A run of an NFA (Σ, 𝑄, 𝑄0 , 𝛿, 𝐹 ) on a word 𝑎0 · · · 𝑎𝑛−1 of length 𝑛 for 𝑎𝑖 ∈ Σ is a finite sequence 𝑞0 , · · · , 𝑞𝑛 of states such that 𝑞0 ∈ 𝑄0 and 𝑞𝑖+1 ∈ 𝛿(𝑞𝑖 , 𝑎𝑖 ) for 0 ≤ 𝑖 < 𝑛. A run is accepting if 𝑞𝑛 ∈ 𝐹 . Using the structure of a NFA, we can also represent a Deterministic Finite Automata (DFA), where 𝑄0 contains a single initial state and 𝛿 is restricted to return a single successor state. A finite word 𝑤 ∈ Σ* is accepted by an NFA, if there is an accepting run on 𝑤. The language recognized by a NFA A is defined as ℒ(A) = {𝑤 ∈ Σ* | A accepts 𝑤}. An Alternating Automaton over Finite Words (AFW; [16, 15]) is a tuple (Σ, 𝑄, 𝑞0 , 𝛿, 𝐹 ), where Σ and 𝑄 are as with NFAs, 𝑞0 is the initial state, 𝛿 : 𝑄 × Σ → 𝐵 + (𝑄) is a transition function, where 𝐵 + (𝑄) stands for all propositional formulas built from 𝑄, ∧, ∨, ⊤ and ⊥, and 𝐹 ⊆ 𝑄 is a finite set of final states. A run of an AFW (Σ, 𝑄, 𝑞0 , 𝛿, 𝐹 ) on a word 𝑎0 · · · 𝑎𝑛−1 of length 𝑛 for 𝑎𝑖 ∈ Σ, is a finite tree 𝑇 labeled by states in 𝑆 such that 1. the root of 𝑇 is labeled by 𝑞0 , 2. if node 𝑜 at level 𝑖 is labeled by a state 𝑞 ∈ 𝑄 and 𝛿(𝑞, 𝑎𝑖 ) = 𝜙, then either 𝜙 = ⊤ or 𝑃 |= 𝜙 for some 𝑃 ⊆ 𝑄 and 𝑜 has a child for each element in 𝑃 , 3. the run is accepting if all leaves at depth 𝑛 are labeled by states in 𝐹 . A finite word 𝑤 ∈ Σ* is accepted by an AFW, if there is an accepting run on 𝑤. The language recognized by an AFW A is defined as ℒ(A) = {𝑤 ∈ Σ* | A accepts 𝑤}. AFWs can be seen as an extension of NFAs by universal transitions. That is, when looking at formulas in 𝐵 + (𝑄), disjunctions represent alternative transitions as in NFAs, while conjunctions add universal ones, each of which must be followed. In Section 5.2, we assume formulas in 𝐵 + (𝑄) to be in disjunctive normal form (DNF) and represent them as sets of sets of literals; hence, {∅} and ∅ stand for ⊤ and ⊥, respectively. 4. LDL𝑓 to AFW This section describes a translation of dynamic formulas in LDL𝑓 to AFW due to [17]. More precisely, it associates a dynamic formula 𝜙 in negation normal form with an AFW A𝜙 , whose number of states is linear in the size of 𝜙 and whose language ℒ(A𝜙 ) coincides with the set of all traces satisfying 𝜙. A dynamic formula 𝜙 can be put in negation normal form nnf (𝜙) by exploiting equivalences and pushing negation inside, until it is only in front of propositional formulas. The states of A𝜙 correspond to the members of the Fisher-Ladner closure [18] of 𝜙, denoted by cl (𝜙). The alphabet of an AFW A𝜙 for a formula 𝜙 over 𝒫 is Σ = 2𝒫∪{last} . It relies on a special proposition last [17], which is only satisfied by the last state of the trace. A finite word over Σ corresponds to a finite trace over 𝒫 ∪ {last}. Definition 2 (LDL𝑓 to AFW[17]). Given a dynamic formula 𝜙 in negation normal form, the corresponding AFW is defined as A𝜙 = (2𝒫∪{last} , {𝑞nnf (𝜑) | 𝜑 ∈ cl (𝜙)}, 𝑞𝜙 , 𝛿, ∅) where transition function 𝛿 mapping a state 𝑞nnf (𝜑) for 𝜑 ∈ cl (𝜙) and an interpretation 𝑋 ⊆ 𝒫 ∪ {last} into a positive Boolean formula over the states in {𝑞nnf (𝜑) | 𝜑 ∈ cl (𝜙)} is defined as follows: def def 1. 𝛿(𝑞⊤ , 𝑋) = ⊤ 2. 𝛿(𝑞⊥ , 𝑋) = ⊥ {︃ {︃ def ⊤ if 𝑎 ∈ 𝑋 def ⊥ if 𝑎 ∈ 𝑋 3. 𝛿(𝑞𝑎 , 𝑋) = 4. 𝛿(𝑞¬𝑎 , 𝑋) = ⊥ if 𝑎 ∈ /𝑋 ⊤ if 𝑎 ∈/𝑋 {︃ {︃ def 𝑞𝜙 if last ∈ /𝑋 def 𝑞𝜙 if last ∈ /𝑋 5. 𝛿(𝑞⟨τ⟩ 𝜙 , 𝑋) = 6. 𝛿(𝑞[τ] 𝜙 , 𝑋) = ⊥ if last ∈ 𝑋 ⊤ if last ∈ 𝑋 def 7. 𝛿(𝑞⟨𝜓?⟩ 𝜙 , 𝑋) = 𝛿(𝑞𝜓 , 𝑋) ∧ 𝛿(𝑞𝜙 , 𝑋) def 8. 𝛿(𝑞⟨𝜌1 +𝜌2 ⟩ 𝜙 , 𝑋) = 𝛿(𝑞⟨𝜌1 ⟩ 𝜙 , 𝑋) ∨ 𝛿(𝑞⟨𝜌2 ⟩ 𝜙 , 𝑋) def 9. 𝛿(𝑞⟨𝜌1 ;𝜌2 ⟩ 𝜙 , 𝑋) = 𝛿(𝑞⟨𝜌1 ⟩ ⟨𝜌2 ⟩ 𝜙 , 𝑋) {︃ def 𝛿(𝑞𝜙 , 𝑋) if 𝜌 is a test 10. 𝛿(𝑞⟨𝜌* ⟩ 𝜙 , 𝑋) = 𝛿(𝑞𝜙 , 𝑋) ∨ 𝛿(𝑞⟨𝜌⟩ ⟨𝜌* ⟩ 𝜙 , 𝑋) otherwise def 11. 𝛿(𝑞⟨(𝜓?)* ⟩ 𝜙 , 𝑋) = 𝛿(𝑞𝜙 , 𝑋) def 12. 𝛿(𝑞[𝜓?] 𝜙 , 𝑋) = 𝛿(𝑞nnf (¬𝜓) , 𝑋) ∨ 𝛿(𝑞𝜙 , 𝑋) def 13. 𝛿(𝑞[𝜌1 +𝜌2 ] 𝜙 , 𝑋) = 𝛿(𝑞[𝜌1 ] 𝜙 , 𝑋) ∧ 𝛿(𝑞[𝜌2 ] 𝜙 , 𝑋) def 14. 𝛿(𝑞[𝜌1 ;𝜌2 ] 𝜙 , 𝑋) = 𝛿(𝑞[𝜌1 ] [𝜌2 ] 𝜙 , 𝑋) {︃ def 𝛿(𝑞𝜙 , 𝑋) if 𝜌 is a test 15. 𝛿(𝑞[𝜌* ] 𝜙 , 𝑋) = 𝛿(𝑞𝜙 , 𝑋) ∧ 𝛿(𝑞[𝜌] [𝜌* ] 𝜙 , 𝑋) otherwise def 16. 𝛿(𝑞[𝜌* ] 𝜙 , 𝑋) = 𝛿(𝑞𝜙 , 𝑋) ∧ 𝛿(𝑞[𝜌] [𝜌* ] 𝜙 , 𝑋) def 17. 𝛿(𝑞[(𝜓?)* ] 𝜙 , 𝑋) = 𝛿(𝑞𝜙 , 𝑋) Note that the resulting automaton lacks final states. This is compensated by the dedicated proposition last. All transitions reaching a state, namely 𝛿(𝑞[τ] 𝜙 , 𝑋) and 𝛿(𝑞⟨τ⟩ 𝜙 , 𝑋), are subject to a condition on last. So, for the last interpretation 𝑋 ∪ {last}, all transitions end up in ⊤ or ⊥. Hence, for acceptance, it is enough to ensure that branches reach ⊤. As an example, consider the formula, 𝜙, ⟨([τ* ] 𝑏)? ; τ⟩ 𝑎 = □𝑏 ∧ ◦𝑎, (1) stating that 𝑏 always holds and 𝑎 is true at the next step. The AFW for 𝜙 is A𝜙 = (2{𝑎,𝑏,last} , 𝑄+ ∪ 𝑄− , 𝛿, ∅), where 𝑄+ = {𝑞⟨([τ* ] 𝑏)? ; τ⟩ 𝑎 , 𝑞⟨([τ* ] 𝑏)? ⟩ ⟨τ⟩ 𝑎 , 𝑞[τ* ] 𝑏 , 𝑞[τ] [τ* ] 𝑏 , 𝑞τ , 𝑞𝑏 , 𝑞⟨τ⟩ 𝑎 , 𝑞𝑎 } and 𝑄− contains all states stemming from negated formulas in 𝑄+ ; all these are unreachable in our case. The alternating automaton can be found in in Figure 1. 𝑏 ∧ ¬𝑙𝑎𝑠𝑡 𝑞□𝑏 ∀ 𝑏 ∧ last 𝑏 ∧ ¬last 𝑞𝜙 ∀ 𝑞𝑎 ∀ 𝑎 Figure 1: A𝜙 showing only the reachable states. The special node type, labeled as ∀, represents universal transitions, when the ∀-node has no outgoing edges it represents the empty universal constraint ⊤. {𝑎, 𝑏} {𝑏, last} {𝑎} 𝑞□𝑏 𝑞□𝑏 ∀✓ 𝑞□𝑏 ⊥ {𝑏} {𝑏} 𝑞𝜙 ∀ 𝑞𝜙 ∀ {𝑎, 𝑏} {𝑎} 𝑞𝑎 ∀✓ 𝑞𝑎 ∀✓ Figure 2: Accepted run for Figure 3: Rejected run for {𝑏} · {𝑎, 𝑏} · {𝑏, last}. {𝑏} · {𝑎} · {𝑏, last}. 5. Using automata for implementing dynamic constraints Our goal is to investigate alternative ways of implementing constraints imposed by dynamic formulas. To this end, we pursue three principled approaches: (T) Tseitin-style translation into regular logic programs, (A) ASP-based translation into alternating automata, (M) MONA-based translation into deterministic automata, using Mm and Ms for the Monadic Second Order Encoding and the Standard Translation, respectively. These alternatives are presented in our systems’ workflow 1 from Figure 4. The common idea is to compute all fixed-length traces, or plans, of a dynamic problem expressed in plain ASP (in files .lp and .lp) that satisfy the dynamic constraints in .lp. All such constraints are of form :- not 𝜙. which is the logic programming representation of the formula ¬¬𝜙. Note that these constraints may give rise to even more instances after grounding. The choice of using plain ASP rather than temporal logic programs, as used in telingo [6, 12], is motivated by simplicity and the possibility of using existing ASP benchmarks. For expressing dynamic formulas all three approaches rely on clingo’s theory reasoning framework that allows for customizing its input language with theory-specific language con- structs that are defined by a theory grammar [8]. The part telingo uses for dynamic formulas is given in Listing 1. 1 #theory del { 2 formula_body { 3 & : 7,unary; ~ : 5,unary; 4 ? : 4,unary; * : 3,unary; + : 2,binary,left; ;; : 1,binary,left; 1 The source code can be found in https://github.com/potassco/atlingo v1.0. grammar.lp .lp .lp .lp T A M clingoAPI gringo clingoAPI mso(0, ϕ) STm(0, ϕ) ldlf2mso.py ldlf2ltlf.py reified.lp ldlf2afw.lp mso.mona mso.mona ltlf2lp.py clingo MONA dfa.dot telingo program.lp afw.lp run.lp dfa.lp clingo clingo clingo Traces for the dynamic problem (.lp and .lp) satisfying the dynamic constraints in .lp Figure 4: Workflows of our framework. Elements in yellow correspond to user input, green ones are automatically generated, and red ones are provided by the system to solve the problem. 5 .>? : 0,binary,right; .>* : 0,binary,right 6 }; 7 &del/0 : formula_body, body 8 }. Listing 1: Theory specification for dynamic formulas (grammar.lp) The grammar contains a single theory term definition for formula_body, which consists of terms formed from the theory operators in Line 3 to 5 along with basic gringo terms. More specifically, & serves as a prefix for logical constants, eg. &true and &t stand for ⊤ and τ, while ~ stands for negation. The path operators ?, * , +, ; are represented by ?, *, +, ;;, where ? and * are used as prefixes, and the binary dynamic operators ⟨·⟩ and [·] by .>? and .>*, respectively (extending telingo’s syntax >? and >* for unary temporal operators ♢ and □). Such theory terms can be used within the set associated with the (zero-ary) theory predicate &del/0 defined in Line 7 (cf. [8]). Since we impose our dynamic constraints through integrity constraints, we restrict the occurrence of corresponding atoms to rule bodies, as indicated by the keyword body. The representation of our running example ⟨([τ* ] 𝑏)? ; τ⟩ 𝑎 as an integrity constraint is given in Listing 2. :- not &del{ ? (* &t .>* b) ;; &t .>? a }. Listing 2: Representation of ‘¬¬⟨([τ* ] 𝑏)? ; τ⟩ 𝑎’ from (1) (delex.lp) Once such a dynamic formula is parsed by gringo, it is processed in a different way in each workflow. At the end, however, each workflow produces a logic program that is combined with the original dynamic problem in .lp and .lp and handed over to clingo to compute all traces of length lambda satisfying the dynamic formula(s) in .lp. We also explored a translation from the alternating automata generated in A into an NFA using both ASP and python. This workflow, however, did not show any interesting results, hence, due to space limitations it is omitted. 5.1. Tseitin-style translation into logic programs The leftmost part of the workflow in Figure 4 relies on telingo’s infrastructure [6, 12]: Once grounded, a dynamic formula is first translated into a temporal formula (ldlf2ltlf.py), which is then translated into a regular logic program (ltlf2lp.py).2 These translations heavily rely on the introduction of auxiliary variables for subformulas, a technique due to Tseitin [19]. In this way, all integrity constraints in .lp get translated into the ground program program.lp. In the worst case, this program consists of lambda copies of the translated constraint. This approach is detailed in [12, 13]. 5.2. ASP-based translation into alternating automata The approach illustrated in the middle of Figure 4 follows the construction in Section 4. More precisely, it builds the AFW A𝜙 for each ground constraint ¬¬𝜙 by taking advantage of Propo- sition 1. Notably, the approach is fully based on ASP and its meta-programming capabilities: It starts by reifying each ¬¬𝜙 into a set of facts, yielding the single file reified.lp. These facts are then turned into one or more AFW A𝜙 through logic program ldlf2afw.lp. In fact, each A𝜙 is once more represented as a set of facts, gathered in file afw.lp in Figure 4. Finally, the encoding in run.lp makes sure that the trace produced by the encoding of the original dynamic problem is an accepted run of A𝜙 . In what follows, we outline these three steps using our running example. The dynamic constraint in Listing 2 is transformed into a set of facts via gringo’s reification option –output=reify. The facts provide a serialization of the constraint’s abstract syntax tree following the aspif format [8]. Among the 42 facts obtained from Listing 2, we give the ones representing subformula [τ* ] 𝑏, or ‘* &t .>* b’, in Listing 3. Gringo’s reification format uses integers to identify substructures and to tie them together. For instance, the whole expression ‘* &t .>* b’ is identified by 11 in Line 20. Its operator ‘.>*’ is identified by 4 and both are mapped to each other in Line 16. The two arguments ‘* &t’ and ‘b’ are indirectly represented by tuple 2 in Line 17-19 and identified by 9 and 10, respectively. While ‘b’ is directly associated with 10 in Line 15, ‘* &t’ is further decomposed in Line 14 into operator ‘*’ (cf. Line 11) and its argument ‘&t’. The latter is captured by tuple 1 but not further listed for brevity. 2 Filenames are of indicative nature only. 11 theory_string(5,"*"). 12 theory_tuple(1). 13 theory_tuple(1,0,8). 14 theory_function(9,5,1). 15 theory_string(10,"b"). 16 theory_string(4,".>*"). 17 theory_tuple(2). 18 theory_tuple(2,0,9). 19 theory_tuple(2,1,10). 20 theory_function(11,4,2). Listing 3: Facts 11-20 obtained by a call akin to gringo –output=reify grammar.lp delex.lp > reified.lp The reified representation of the dynamic constraint in Listing 2 is now used to build the AFW in Figure 1 in terms of the facts in Listing 4. As shown in Figure 4, the facts in afw.lp 1 prop(10,"b"). prop(14,"a"). prop(16,"last"). 2 state(0,dia(seq(test(box(str(stp),p(10))),stp),p(14))). 3 state(1,p(14)). 4 state(2,box(str(stp),p(10))). 5 initial_state(0). 6 delta(0,0). delta(0,0,out,16). delta(0,0,in,10). 7 delta(0,0,1). delta(0,0,2). 8 delta(1,0). delta(1,0,in,14). 9 delta(2,0). delta(2,0,out,16). delta(2,0,in,10). 10 delta(2,0,2). 11 delta(2,1). delta(2,1,in,16). delta(2,1,in,10). Listing 4: Generated facts representing the AFW in Figure 1 (afw.lp) are obtained by applying clingo to ldlf2afw.lp and reified.lp, the facts generated in the first step. An automaton A𝜙 is represented by the following predicates: • prop/2, providing a symbol table mapping integer identifiers to atoms, • state/2, providing states along with their associated dynamic formula; the initial state is distinguished by initial_state/1, and • delta/2,3,4, providing the automaton’s transitions. The symbol table in Line 1 in Listing 4 is directly derived from the reified format. In addition, the special proposition last is associated with the first available identifier. The interpretations over a, b, last constitute the alphabet of the automaton at hand. More efforts are needed for calculating the states of the automaton. Once all relevant symbols and operators are extracted from the reified format, they are used to build the closure cl (𝜙) of 𝜙 in the input and to transform its elements into negation normal form. In the final representation of the automaton, we only keep reachable states and assign them a numerical identifier. The states in Line 2 to 3 correspond to the ones labeled 𝑞𝜙 , 𝑞𝑎 and 𝑞□𝑏 in Figure 1. The transition function is represented by binary, ternary, and quaternary versions of predicate delta. The representation is centered upon the conjunctions in the set representation of the DNF of 𝛿(𝑞, 𝑋) (cf. Section 3). Each conjunction C represents a transition from state Q and is captuted by delta(Q,C). An atom of form delta(Q,C,Q’) indicates that state Q’ belongs to conjunction C and delta(Q,C,T,A) expresses the condition that either A ∈ 𝑋 or A ̸∈ 𝑋 depending on whether T equals in or out, respectively. The binary version of delta is needed since there may be no instances of the ternary and quaternary ones. The facts in Line 6 to 7 in Listing 4 capture the only transition from the initial state in Figure 1, viz. 𝛿(𝑞𝜙 , 𝑋) = {{𝑞□𝑏 , 𝑞𝑎 }}. Both the initial state and the transition are identified by 0 in Line 6. Line 6 also gives the conditions last ̸∈ 𝑋 and 𝑏 ∈ 𝑋 needed to reach the successor states given in Line 7. Line 8 accounts for 𝛿(𝑞𝑎 , 𝑋) = {∅}, reaching ⊤ (ie., an empty set of successor states) from 𝑞𝑎 provided 𝑎 ∈ 𝑋. We encounter two possible transitions from state 2, or 𝑞[τ* ] 𝑏 . Transition 0 in Line 9 to 10 represents the loop 𝛿(𝑞[τ* ] 𝑏 , 𝑋) = {{𝑞[τ* ] 𝑏 }} for last ̸∈ 𝑋 and 𝑏 ∈ 𝑋, while transition 1 in Line 11 captures 𝛿(𝑞[τ* ] 𝑏 , 𝑋) = {∅} that allows us to reach ⊤ whenever {last, 𝑏} ⊆ 𝑋. Finally, the encoding in Listing 5 checks whether a trace is an accepted run of a given automaton. We describe traces using atoms of form trace(A,T), stating that the atom identified 1 node(Q,0) :- initial_state(Q). 2 { select(C,Q,T): delta(Q,C) } = 1 :- node(Q,T), T<=lambda-1. 3 node(Q’,T+1) :- select(C,Q,T), delta(Q,C,Q’). 4 :- select(C,Q,T), delta(Q,C,in,A), not trace(A,T). 5 :- select(C,Q,T), delta(Q,C,out,A), trace(A,T). Listing 5: Encoding defining the accepted runs of an automaton (run.lp). by A is true in the trace at time step T. Although such traces are usually provided by the encoding of the dynamic problem at hand, the accepted runs of an automaton can also be enumerated by adding a corresponding choice rule. In addition, the special purpose atom last is made true in the final state of the trace. For verifying whether a trace of length lambda is accepted, we build the tree corresponding to a run of the AFW on the trace at hand. This tree is represented by atoms of form node(S,T), indicating that state S exists at depth/time T3 . The initial state is anchored as the root in Line 1. In turn, nodes get expanded by depth by selecting possible transitions in Line 2. The nodes are then put in place by following the transition of the selected conjunction in Line 3. Lines 4 and 5 verify the conditions for the selected transition. 5.3. MONA-based translation into deterministic automata The rightmost part of the workflow in Figure 4 relies on our translations of dynamic formulas into MSOs from [10]. These translations, called Monadic Second Order Encoding and Standard Translation, are defined for a dynamic formula 𝜙 and a time point 𝑡 as mso(𝑡, 𝜙) and stm(𝑡, 𝜙), 3 Note that we do not need to represent the edges between nodes as their depth is indicative enough for the acceptance. In the literature, runs of AFW are often represented using directed acyclic graphs instead of trees. respectively. We use the off-the-shelf tool MONA4 [11] to translate the resulting MSO for- mulas into DFAs. More precisely, we use clingo’s API to transform each dynamic constraint ¬¬𝜙 in .lp either into MSO formula mso(0, 𝜙) or stm(0, 𝜙). This results in a file ⁀extttmso.mona in MONA’s syntax, which is then turned by MONA into a corresponding DFA in dot format. All these automata are then translated into facts and gathered in dfa.lp in the same format as used for AFWs. The encoding in Listing 5 can be used to find accepted runs of DFAs by adding the following integrity constraint ensuring that runs end in a final state. :- node(Q,lambda), not final_state(Q). 6. Evaluation For our experimental studies, we use benchmarks from the domain of robotic intra-logistics stemming from the asprilo framework [20]. As illustrated in Figure 5 and 6, we consider grids of size 7×7 with 𝑛 ∈ {2, 3} robots and 𝑛 * 2 orders of single products, each located on a unique shelf. At each timestep, a robot can: (i) move in a direction(ii) pickup a shelf (iii) putdown a shelf or (iv) wait. Moreover, a robot will deliver an order if it waits at a picking station while carrying a shelf. The goal is to take each shelf to a picking station; in an optimal plan (wrt. trace length) each robot processes two orders. Figure 5: Asprilo visualization Figure 6: Asprilo visualization for two robots instance. for three robots instance. We consider three different dynamic constraints. The first one restricts plans such that if a robot picks up a shelf, then it must move or wait several times until the shelf is delivered. This is expressed by the dynamic formula 𝜙1 and represented in Listing 65 , were pickup 𝑠 and deliver 𝑠 refer to a specific shelf. 𝜙1 = [τ* ] [pickup 𝑠 ?] ⟨(τ; (move? + wait?))* ; deliver 𝑠 ?⟩ ⊤ The second one, 𝜙2 , represents a procedure where robots must repeat a sequence in which they move towards a shelf, pickup, move towards a picking station, deliver, move to the dropping place and putdown, and finish with waiting until the end of the trace . 𝜙2 = ⟨(move * ; pickup * ; move * ; deliver ; move * ; putdown)* ; wait * ⟩ F 4 https://www.brics.dk/mona 5 We start repetitions with τ as &t, to cope with movements in asprilo starting at time point 1. 1 :- not &del{ 2 (* &t) .>* 3 ?pickup(robot(R),shelf(S)) .>* 4 *(&t ;; ?move(robot(R)) + ?waits(robot(R))) ;; 5 ?deliver(robot(R),shelf(S)) .>? 6 &true}, 7 robot(R), shelf(S). Listing 6: Dynamic constraint for formula 𝜙1 . Table 1 Automata size for the 3 robots instance showing the number of appearances of each atom. 𝜙𝑖 predicate A Mm Ms 𝜙1 state/2 36 72 72 delta/2 162 234 216 𝜙2 state/2 24 51 51 delta/2 60 390 471 𝜙3 state/2 45 - 372 delta/2 189 - 16 503 For our last constraint we use the dynamic formula 𝜙3 . This corresponds to a procedure similar to 𝜙2 but which relies on a predefined pattern, restricting the direction of movements with move r , move l , move u and move d to refer to moving right, left, up and down, respectively. We use the path 𝜌 = (move r* + move l* ) so that robots only move in one horizontal direction. Additionally, each iteration starts by waiting so that whenever a robot starts moving, it fulfills the delivery without intermediate waiting. 𝜙3 = ⟨(wait * ; 𝜌; move u* ; pickup; 𝜌; move u* ; deliver ; 𝜌; move d* ; putdown)* ; wait * ⟩ F We use these constraints to contrast their implementations by means of our workflows A, T, Mm and Ms with 𝜆 ∈ {25, . . . , 31}, while using the option of having no constraint, namely NC, as a baseline. The presented results ran using clingo 5.4.0 on an Intel Xeon E5-2650v4 under Debian GNU/Linux 9, with a memory of 20 GB and a timeout of 20 min per instance. All times are presented in milliseconds and any time out is counted as 1 200 000 ms in our calculations. We first compare the size of the automata in Table 1 in terms of the instances of predicates state/2 and delta/2. We see that A generates an exponentially smaller automata, a known result from the literature [21]. More precisely, for 𝜙3 the number of transitions in Ms is 90 times larger than for A. Furthermore, for this constraint, Mm reached the limit of nodes for MONA’s BDD-based architecture, thus producing no result. This outcome is based on the fact that the MSO formulas computed by Mm are significantly larger than those of Ms . Next, we give the preprocessing times obtained for the respective translations in Table 2. For the automata-based approaches A, Mm and Ms the translation is only performed once and reused in subsequent calls, whereas for T the translation is redone for each horizon. The best performing approach is A, for the subsequent calls the times were very similar with the exception of T. We see how for 𝜙2 the Mm translation takes considerably longer than for Ms . Table 2 Pre-processing time in milliseconds shown as 𝑡1 /𝑡2 were 𝑡1 is the time for the first horizon and 𝑡2 the average over subsequent calls. 𝜙𝑖 #r A Mm Ms T NC 𝜙1 2 1 194/637 5 412/638 5 867/604 2 696/2 992 306/598 3 1 991/600 6 280/671 6 978/610 3 390/3 691 302/617 𝜙2 2 2 182/579 33 091/661 4 966/598 2 107/2 814 285/577 3 1 632/608 45 303/665 4 973/604 2 718/3 179 318/631 𝜙3 2 2 533/599 - 12 682/766 3 343/3 280 261/605 3 3 112/600 - 11,001/795 3,278/3,718 272/598 Table 3 Statistics computed by calculating the geometric mean of all horizons. 𝜙𝑖 #r A Mm Ms T 𝑁𝐶 clingo time 𝜙1 2 3 374 2 788 2 975 3 033 21 823 3 23 173 27 866 27 505 23 748 249 737 𝜙2 2 10 840 9 424 9 484 9 347 21 378 3 70 709 58 739 83 521 60 765 246 739 𝜙3 2 31 986 - 606 914 16 145 21 548 3 67 287 - 657 633 48 190 247 718 rules 𝜙1 2 89 282 97 396 97 404 96 793 77 832 3 172 641 196 220 190 943 189 637 147 209 𝜙2 2 84 180 122 003 126 634 90 178 77 832 3 157 525 214 454 229 063 166 391 147 209 𝜙3 2 94 653 - 4 413 056 102 687 77 832 3 173 210 - 3 360 382 185 155 147 209 constraints 𝜙1 2 146 999 146 323 146 306 140 801 132 370 3 275 747 274 419 274 382 260 675 241 752 𝜙2 2 138 418 166 449 171 796 139 909 132 370 3 252 023 295 946 308 204 254 020 241 752 𝜙3 2 153 179 - 3 341 017 147 123 132 370 3 274 851 - 2 743 736 264 847 241 752 The results of the final solving step in each workflow are summarized in Table 3, showing the geometric mean over all horizons for obtaining a first solution. First of all, we observe that the solving time is significantly lower when using dynamic constraints, no matter which approach is used. For 𝜙1 and 𝜙2 the difference is negligible, whereas for 𝜙3 , T is the fastest, followed by A, which is in turn twenty and ten times faster than Ms for 2 and 3 robots, respectively. Furthermore, Ms times out for 𝜙3 with 𝜆 = 31 and 𝜆 ∈ {30, 31} for 2 and 3 robots, respectively. The size of the program before and after clingo’s preprocessing can be read off the number of ground rules and internal constraints, with A having the smallest size of all approaches. However, once the program is reduced the number of constraints shows a slight shift in favour of T. 7. Discussion To the best of our knowledge, this work presents the first endeavor to represent dynamic constraints with automata in ASP. The equivalence between temporal formulas and automata has been widely used in satisfiability checking, model checking, learning and synthesis [21, 22, 17, 23, 24]. Furthermore, the field of planning has benefited from temporal reasoning to express goals and preferences using an underlying automaton [25, 26, 27]. There exists several systems that translate temporal formulas into automata: SPOT [28] and LTLf2DFA6 for linear temporal logic; abstem [29] and stelp [30] for temporal answer set programming. Nonetheless, there have only been a few attempts to use automata-like definitions in ASP for representing temporal and procedural knowledge inspired from GOLOG programs [31, 32]. We investigated different automata-based implementations of dynamic (integrity) constraints using clingo. Our first approach was based on alternating automata, implemented entirely in ASP through meta-programming. For our second approach, we employed the off-the-shelf automata construction tool MONA [11] to build deterministic automata. To this aim, we proposed two translations from dynamic logic into monadic second-order logic. These approaches were contrasted with the temporal ASP solver telingo which directly maps dynamic constraints to logic programs. We provided an empirical analysis demonstrating the impact of using dynamic constraints to select traces among the ones induced by an associated temporal logic program. Our study showed that the translation using solely ASP to compute an alternating automata yielded the smallest program in the shortest time. While this approach scaled well for more complex dynamic formulas, the MONA-based implementation performed poorly and could not handle one of our translations into second order formulas. The best overall performance was exhibited by telingo with the fundamental downside of having to redo the translation for each horizon. Our future work aims to extend our framework to arbitrary dynamic formulas in DEL𝑓 . Additionally, the automaton’s independence of time stamps points to its potential to detect unsatisfiability and to guide an incremental solving process. Finally, we also intend to take advantage of clingo’s application programming interface to extend the model-ground-solve workflow of ASP with automata techniques. References [1] V. Lifschitz, Answer set planning, in: Proc. of the Int. Conf. on Logic Programming, MIT Press, 1999, pp. 23–37. [2] A. Bosser, P. Cabalar, M. Diéguez, T. Schaub, Introducing temporal stable models for linear dynamic logic, in: Proc. of the Int. Conf. on Principles of Knowledge Representation and Reasoning, AAAI Press, 2018, pp. 12–21. [3] P. Cabalar, M. Diéguez, T. Schaub, Towards dynamic answer set programming over finite traces, in: [33], 2019, pp. 148–162. [4] J. Hopcroft, J. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979. 6 https://github.com/whitemech/LTLf2DFA [5] F. Aguado, P. Cabalar, M. Diéguez, G. Pérez, C. Vidal, Temporal equilibrium logic: a survey, Journal of Applied Non-Classical Logics 23 (2013) 2–24. [6] P. Cabalar, R. Kaminski, T. Schaub, A. Schuhmann, Temporal answer set programming on finite traces, Theory and Practice of Logic Programming 18 (2018) 406–420. [7] P. Cabalar, M. Diéguez, T. Schaub, A. Schuhmann, Towards metric temporal answer set programming, Theory and Practice of Logic Programming 20 (2020) 783–798. [8] R. Kaminski, T. Schaub, P. Wanko, A tutorial on hybrid answer set solving with clingo, in: Proc. of the Int. Summer School of the Reasoning Web, volume 10370 of LNCS, Springer, 2017, pp. 167–203. [9] T. Wolfgang, Languages, automata, and logic, in: Handbook of Formal Languages, volume 3: Beyond Words, Springer, 1997, pp. 389–455. [10] P. Cabalar, M. Diéguez, S. Hahn, T. Schaub, Automata for dynamic answer set solving: Preliminary report, 2021. arXiv:2109.01782. [11] J. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, A. Sandholm, Mona: Monadic second-order logic in practice, in: Proc. of the Int. Workshop on Tools and Algorithms for Construction and Analysis of Systems, volume 1019 of LNCS, Springer, 1995, pp. 89–110. [12] P. Cabalar, R. Kaminski, P. Morkisch, T. Schaub, telingo = ASP + time, in: [33], 2019, pp. 256–269. [13] P. Cabalar, M. Diéguez, F. Laferriere, T. Schaub, Implementing dynamic answer set programming over finite traces, in: Proc. of the European Conf. on AI, volume 325 of Frontiers in AI and Applications, IOS Press, 2020, pp. 656–663. [14] D. Harel, J. Tiuryn, D. Kozen, Dynamic Logic, MIT Press, 2000. [15] G. De Giacomo, M. Vardi, Linear temporal logic and linear dynamic logic on finite traces, in: Proc. of the Int. Joint Conf. on AI, IJCAI/AAAI Press, 2013, pp. 854–860. [16] A. Chandra, D. Kozen, L. Stockmeyer, Alternation, Journal of the ACM 28 (1981) 114–133. [17] G. De Giacomo, M. Vardi, Synthesis for LTL and LDL on finite traces, in: Proc. of the Int. Joint Conf. on AI, AAAI Press, 2015, pp. 1558–1564. [18] M. Fischer, R. Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences 18 (1979) 194–211. [19] G. Tseitin, On the complexity of derivation in the propositional calculus, Zapiski nauch- nykh seminarov LOMI 8 (1968) 234–259. [20] M. Gebser, P. Obermeier, T. Otto, T. Schaub, O. Sabuncu, V. Nguyen, T. Son, Experimenting with robotic intra-logistics domains, Theory and Practice of Logic Programming 18 (2018) 502–519. [21] M. Vardi, An automata-theoretic approach to linear temporal logic, in: Logics for Concur- rency: Structure versus Automata, volume 1043 of LNCS, Springer, 1995, pp. 238–266. [22] M. Vardi, Alternating automata: Unifying truth and validity checking for temporal logics, in: Proc. of the Int. Conf. on Automated Deduction, volume 1249 of LNCS, Springer, 1997, pp. 191–206. [23] K. Rozier, M. Vardi, Ltl satisfiability checking, in: Int. SPIN Workshop on Model Checking of Software, Springer, 2007, pp. 149–167. [24] A. Camacho, S. McIlraith, Learning interpretable models expressed in linear temporal logic, in: Proc. of the Int. Conf. on Automated Planning and Scheduling, AAAI Press, 2019, pp. 621–630. [25] J. Baier, C. Fritz, M. Bienvenu, S. McIlraith, Beyond classical planning: Procedural control knowledge and preferences in state-of-the-art planners, in: Proc. of the National Conf. on AI, AAAI Press, 2008, pp. 1509–1512. [26] G. D. Giacomo, S. Rubin, Automata-theoretic foundations of fond planning for LTLf and LDLf goals., in: Proc. of the Int. Joint Conf. on Artificial Intelligence, ijcai.org, 2018, pp. 4729–4735. [27] J. Baier, S. McIlraith, Planning with first-order temporally extended goals using heuristic search, in: Proc. of the National Conf. on AI, AAAI Press, 2006, pp. 788–795. [28] A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, L. Xu, Spot 2.0 - A framework for LTL and 𝜔-automata manipulation, in: Proc. of the Int. Symposium on Automated Technology for Verification and Analysis, volume 9938 of LNCS, 2016, pp. 122–129. [29] P. Cabalar, M. Diéguez, Strong equivalence of non-monotonic temporal theories, in: Proc. of the Int. Conf. on Principles of Knowledge Representation and Reasoning, AAAI Press, 2014. [30] P. Cabalar, M. Diéguez, STELP — a tool for temporal answer set programming, in: Proc. of the Int. Conf. on Logic Programming and Nonmonotonic Reasoning, volume 6645 of LNAI, Springer, 2011, pp. 370–375. [31] T. Son, C. Baral, T. Nam, S. McIlraith, Domain-dependent knowledge in answer set planning, ACM Transactions on Computational Logic 7 (2006) 613–657. [32] M. Ryan, Efficiently implementing GOLOG with answer set programming, in: Proc. of the National Conf. on AI, AAAI Press, 2014, pp. 2352–2357. [33] Proc. of the Int. Conf. on Logic Programming and Nonmonotonic Reasoning, volume 11481 of LNAI, Springer, 2019.