Automata for dynamic answer set solving: Preliminary report

Abstract

We explore diferent 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 of-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

• eol>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 knowledgeintense 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) constraints 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 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 diferent 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 of-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

sions are mutually defined by the pair of grammar rules: Given a set of propositional variables (called alphabet), dynamic formulas and path expres ::= | ⊥ | ⊤ | [ ] | ⟨ ⟩ ::= τ | ? | + | ; | * . defined as 0 d=ef

⊤? and +1 d=ef ; .

This syntax is similar to the one of Dynamic Logic (DL; [ 14 ]) but difers 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

The above language allows us to capture several derived operators, like the Boolean and temporal ones [ 3 ]: ◦ d=ef ⟨τ ⟩ ♢ d=ef ⟨τ * ⟩ = and finite otherwise.

T. The particular type of

{

∈ 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 and H′ = (′)∈[0.. ) both of length , we write H ≤ H′ if ⊆ ′ for each ∈ [0.. ); otherwise, that is,

= for some natural number ∈ N. Given traces H = ()∈[0.. ) usual, a (dynamic) theory is a set of (dynamic) formulas.

The overall definition of DHT satisfaction relies on a double induction. Given any HT-trace HT-traces that satisfy H = T are called total. length where H = ()∈[0.. ) and T = ()∈[0.. ) such that H ≤ 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 ⊆ ⊆

for any ∈ [0.. ). As before, an HT-trace is infinite if

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 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 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 For the semantics, we let [..] stand for the set { ∈ N | ≤ ≤ } and [..) for accordingly, H < H′ if both

H ≤

H′ and H ̸= H′. double, structural induction. satisfies conditions hold: Definition 1 (DHT satisfaction; [ 3 ]). An HT-trace M = ⟨H, T⟩ of length over alphabet a dynamic formula at time point ∈ [0.. ), written M, |= , if the following 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 1. M, |= ⊤ and M, ̸|= ⊥ 2. M, |= if ∈ for any atom ∈

for both M′ = M and M′ = ⟨T, T⟩ 3. M, |= ⟨ ⟩ if M, |= for some with (, ) ∈‖ ‖ 4. M, |= [ ] if M′, |= for all with (, ) ∈‖ ‖

M M′ where, for any HT-trace M, ‖ ‖M⊆ N2 is a relation on pairs of time points inductively defined as follows.

5. ‖ τ ‖M d=ef {(, + 1) | , + 1 ∈ [0.. )} 6. ‖ ? ‖M def

= {(, ) | M, |= } 7. ‖ 1 + 2 ‖M d=ef ‖ 2 ‖M ∪ ‖ 2 ‖M 8. ‖ 1 ; 2 ‖M d=ef {(, ) | (, ) ∈‖ 1 ‖M and (, ) ∈‖ 2 ‖M for some } 9. ‖ * ‖M d=ef ⋃︀≥ 0 ‖ ‖M

An HT-trace M is a model of a dynamic theory Γ if M, 0 |= for all ∈ Γ . We write DHT(Γ , ) to stand for the set of DHT models of length of a theory Γ , and define DHT(Γ) d=ef ⋃︀

=0 DHT(Γ , ), that is, the whole set of models of Γ of any length. A formula is a tautology (or is valid), written |= , if 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⟩, |= if 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⟩, |= ¬¬ if 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 if 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 ( )}, , , ∅ ) follows: 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 1. (⊤ , ) d=ef ⊤ 3. ( , ) d=ef

{︃ 5. (⟨τ ⟩ , ) d=ef ⊤ ⊥ {︃ ⊥ if ∈ if ∈/ if last ∈/ if last ∈ 2. (⊥ , ) d=ef ⊥ 4. (¬ , ) d=ef 6. ([τ ] , ) d=ef {︃ ⊥ ⊤ {︃ ⊤ if ∈ if ∈/ if last ∈/ if last ∈ 9. (⟨ 1; 2⟩ , ) d=ef (⟨ 1⟩ ⟨ 2⟩ , ) 7. (⟨ ?⟩ , ) d=ef ( , ) ∧ ( , ) 8. (⟨ 1+ 2⟩ , ) d=ef (⟨ 1⟩ , ) ∨ (⟨ 2⟩ , )

{︃ ( , ) 10. (⟨ * ⟩ , ) d=ef 11. (⟨( ?)* ⟩ , ) d=ef ( , ) 14. ([ 1; 2] , ) d=ef ([ 1] [ 2] , ) 12. ([ ?] , ) d=ef (nnf (¬ ) , ) ∨ ( , ) 13. ([ 1+ 2] , ) d=ef ([ 1] , ) ∧ ([ 2] , )

( , ) ∨ (⟨ ⟩ ⟨ * ⟩ , ) {︃ ( , ) 15. ([ * ] , ) d=ef 17. ([( ?)* ] , ) d=ef ( , ) 16. ([ * ] , ) d=ef ( , ) ∧ ([ ] [ * ] , ) ( , ) ∧ ([ ] [ * ] , ) if is a test otherwise if is a test otherwise

As an example, consider the formula, ,

Note that the resulting automaton lacks final states. This is compensated by the dedicated in ⊤ or ⊥ . Hence, for acceptance, it is enough to ensure that branches reach ⊤ . 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 ⟨([τ * ] )? ; τ ⟩ = □ ∧ ◦, (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 ∀ ∀

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 <ins>.lp and <enc>.lp) that satisfy the dynamic constraints in <dyncon>.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 constructs 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; 1The source code can be found in https://github.com/potassco/atlingo v1.0.

T clingoAPI ltlf2lp.py telingo clingo

A gringo clingo

M clingoAPI mso(0, ϕ) ldlf2mso.py STm(0, ϕ) mso.mona

mso.mona MONA dfa.dot dfa.lp ldlf2ltlf.py reified.lp

ldlf2afw.lp program.lp afw.lp

run.lp clingo

clingo Traces for the dynamic problem (<ins>.lp and <enc>.lp)

satisfying the dynamic constraints in <dycon>.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 diferent way in each workflow. At the end, however, each workflow produces a logic program that is combined with the original dynamic problem in <ins>.lp and <enc>.lp and handed over to clingo to compute all traces of length lambda satisfying the dynamic formula(s) in <dyncon>.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 <dyncon>.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 Proposition 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.

2Filenames 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 ifrst 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 eforts 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(, ), 3Note 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 of-the-shelf tool MONA 4 [ 11 ] to translate the resulting MSO formulas into DFAs. More precisely, we use clingo’s API to transform each dynamic constraint ¬¬ in <dyncon>.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.

We consider three diferent 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 4https://www.brics.dk/mona 5We start repetitions with τ as &t, to cope with movements in asprilo starting at time point 1.

Listing 6: Dynamic constraint for formula 1.

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 mover , movel , moveu and moved to refer to moving right, left, up and down, respectively. We use the path = (mover* + movel* ) 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 * ; ; moveu* ; pickup; ; moveu* ; deliver ; ; moved* ; 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 .

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 diference 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 of 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 diferent 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 of-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. 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, Eficiently 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.

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 .

[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 ifnite 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 nauchnykh 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 Concurrency: 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 ,