=Paper=
{{Paper
|id=Vol-2970/aspocpinvited1
|storemode=property
|title=Automata for Dynamic Answer Set Solving: Preliminary Report
|pdfUrl=https://ceur-ws.org/Vol-2970/aspocpinvited1.pdf
|volume=Vol-2970
|authors=Pedro Cabalar,Martín Diéguez,Susana Hahn,Torsten Schaub
|dblpUrl=https://dblp.org/rec/conf/iclp/CabalarDHS21
}}
==Automata for Dynamic Answer Set Solving: Preliminary Report==
https://ceur-ws.org/Vol-2970/aspocpinvited1.pdf
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.