Extensions of Answer Set Programming with language constructs from temporal logics, such as temporal equilibrium logic over finite traces ( TEL ), provide an expressive computational framework for modeling dynamic applications. In this paper, we study the so-called past-present syntactic subclass, which consists of a set of logic programming rules whose body references to the past and head to the present. Such restriction ensures that the past remains independent of the future, which is the case in most dynamic domains. We extend the definitions of completion and loop formulas to the case of past-present formulas, which allows capturing the temporal stable models of a set of past-present temporal programs by means of an LTL expression.
The representation and reasoning on dynamic scenarios is considered a central problem in the areas of Knowledge Representation [1] (KR) and Artificial Intelligence (AI). Several formal approaches and systems have emerged in order to introduce non-monotonic reasoning features in scenarios where the formalisation of time is fundamental. Such variety of approaches goes from (non-monotonic) temporal logics [2, 3, 4], to a calculi for reasoning about actions and change [5] or a combination of both approaches [6].
In the area of Answer Set Programming [7] (ASP), former approaches to temporal reasoning use first-order encodings [ 8] where the time is represented by means of a variable whose value comes from a finite domain. The main advantage of those approaches is that the computation of the answer sets of the previous approaches can be achieved via incremental solving [9]. Their downside is that they require an explicit representation of time points. However, their pragmatic advantages, such as a rich (static) modeling language and readily available solvers, so far seem to often outweigh the firm logical foundations of temporal reasoning via modal temporal logics [10].
In order to extend the ASP syntax with connectives from modal temporal logics, more precisely Linear Time Temporal Logic [11] (LTL), Temporal Equilibrium Logic [12, 13] (TEL) was proposed as a temporal extension of Equilibrium Logic [14, 15], the best-known logical characterisation of the stable models semantics for logic programming [16]. Built upon the product of the logic of here-and-there (HT for short) and LTL, TEL is, to the best our knowledge, the first temporal non-monotonic logic which does not impose any syntactic restriction on the input language.
In the last years, research on TEL shed lights on several of its properties such as complexity [17], expressiveness [18] or computational methods [19, 20].
Due to the computational complexity of its satisfiability problem ( ExpSpace), the problem of finding tractable fragments of TEL with good computational properties have also been a topic in the literature. Within this context, the so-called splittable temporal logic programs [21] have been proved to be a syntactic fragment of TEL that allows a reduction to LTL via the use of Loop Formulas [22].
When focusing on the relation between TEL and incremental solving, temporal logics on ifnite traces [ 23] (LTL ) have been shown to be a suitable semantics for incremental solving of temporal representations. The resulting logic, called Temporal Equilibrium Logic on Finite traces [24], became the foundations of the temporal ASP solver telingo [25].
In this paper we study a new syntactic fragment of TEL , named past-present temporal logic programs. Inspired by Gabbay’s seminal paper [26], where the declarative character of past temporal operators is emphasized, the language studied in this paper consists of a set of logic programming rules whose formulas in the head are disjunctions of atoms that reference the present, while in its body we allow any arbitrary temporal formula without the use of future operators.
The use of only past operators in the body has the advantage that, when using incremental solving, the body of each rule can be seen as a query whose satisfiability can be checked on the (partial) incremental computation at each step. This advantage allows us to exploit the advantages of telingo’s API in order to reuse partial computations during the solving in order increase its performance.
As a contribution, we study the Lin-Zhao theorem [27] within the context of past-present temporal logic programs. More precisely we show that when the program is tight [28], extending Clark’s completion [29, 30] to the temporal case sufices to capture the answer sets of a finite past-present program Π as the LTL -models of a temporal formula .
We also show that, when the program is not tight, the use of loop formulas is necessary. To this purpose, we extend the definition of loop formulas to the case of past-present programs and we prove the Lin-Zhao theorem in our setting. Finally, we also prove the generalisation of Lin-Zhao theorem in the sense of [22], where the computation of the completion is be replaced by the consideration of unitary loops.
The paper is organised as follows: in Section 2 we introduce the logic of temporal here and there over finite traces and its equilibrium counterpart. In Section 3 we introduce the concept of past-present temporal programs while, in Section 4 we extend the completion property to the temporal case and we prove that, for the case of tight programs, computing the temporal completion sufices to characterise the temporal answer sets of a past-present programs in terms of LTL formulas. The non-tight case is studied in Section 5, where we introduce our temporal extension of loop formulas and extend the results presented in Section 4 to the case of non-tight programs. Our last contribution, presented in Section 6, shows that temporal completion can be captured in the general theory of loop formulas by considering unitary cycles. Finally, in Section 7 we present the conclusions of the paper an we outline some future research lines.
For this paper to be self-contained, we first recall the definitions of THT and TEL as in [13]. All logics treated in this paper share the common syntax of LTL with past operators [2]. We start from a given set of atoms which we call the alphabet. Then, temporal formulas are defined by the grammar:
::= | ⊥ | 1 ⊗ 2 | • | 1 S 2 | 1 T 2 | ◦ | 1 U 2 | 1 R 2 where ∈ is an atom and ⊗ is any binary Boolean connective ⊗ ∈ {→ , ∧, ∨}. The last six cases correspond to the temporal connectives whose names are listed below:
• for previous S for since T for trigger
◦ for next U for until R for release the intended meaning of the previous temporal operators is the following: • (resp. ◦ ) means that is true at the previous (resp. next) time point. U means that is true until is true, while S can be read as is true since was true. For R and T the meaning is not as direct as for the previous operators. R means that is true until both and become true simultaneously or is true forever. T means that is true since both and became true simultaneously or has been true from the beginning.
We also define several common derived operators like the Boolean connectives ⊤ d=ef ¬⊥, ¬ d=ef → ⊥, ↔ d=ef ( → ) ∧ ( → ), and the following temporal operators: ■ ♦ • ̂︀ def = def = I def = def = ⊥ T always before ⊤ S eventually before ¬•⊤ initial • ∨ I weak previous □ ♢
F ◦ ̂︀ def = def = def = def = ⊥ R ⊤ U ¬◦⊤ ◦ ∨ F always afterward eventually afterward ifnal weak next A (temporal) theory is a (possibly infinite) set of temporal formulas.
Given ∈ N and ∈ N ∪ {}, we let [..] stand for the set { ∈ N | ≤ ≤ }, [..) for { ∈ N | ≤ < } and (..] for { ∈ N | < ≤ }. A trace T of length over alphabet is a sequence T = ()∈[0.. ) of sets ⊆ . We say that T is infinite if = and finite otherwise. To represent a given trace, we write a sequence of sets of atoms concatenated with ‘· ’. For instance, the finite trace {} · ∅ · { } · ∅ has length 4 and makes true at even time points and false at odd ones.
A Here-and-There trace (for short HT-trace) of length over alphabet is a sequence of pairs (⟨, ⟩)∈[0.. ) with ⊆ for any ∈ [0.. ). For convenience, we usually represent the HTtrace as the pair ⟨H, T⟩ of traces H = ()∈[0.. ) and T = ()∈[0.. ). Given M = ⟨H, T⟩, def we also denote its length as |M| = |H| = |T| = . Note that the two traces H, T must satisfy a kind of order relation, since ⊆ for each time point . Formally, we define the ordering H ≤ T between two traces of the same length as ⊆ for each ∈ [0.. ). Furthermore, we define H < T as both H ≤ T and H ̸= T. Thus, an HT-trace can also be defined as any pair ⟨H, T⟩ of traces such that H ≤ T. The particular type of HT-traces satisfying H = T are called total.
Definition 1 (THT-satisfaction; [31, 24]). An HT-trace M = ⟨H,T⟩ of length over alphabet satisfies a temporal 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, |= and M, |= 4. M, |= ∨ if M, |= or M, |= 5. M, |= → if ⟨H′,T⟩, ̸|= or ⟨H′,T⟩, |= , for all H′ ∈ {H,T} 6. M, |= • if > 0 and M,− 1 |= 7. M, |= S if for some ∈ [0..], we have M, |= and M, |= for all ∈ (..] 8. M, |= T if for all ∈ [0..], we have M, |= or M, |= for some ∈ (..] 9. M, |= ◦ if + 1 < and M,+1 |= 10. M, |= U if for some ∈ [.. ), we have M, |= and M, |= for all ∈ [..) 11. M, |= R if for all ∈ [.. ), we have M, |= or M, |= for some ∈ [..) A formula is a tautology (or is valid), written |= , if M, |= for any HT-trace M and any ∈ [0.. ). We call the logic induced by the set of all tautologies Temporal logic of Here-and-There (THT for short).
Proposition 2 ([31, 24]). Let M = ⟨H,T⟩ be an HT-trace of length over . Given the respective definitions of derived operators, we get the following satisfaction conditions: 12. M, |= I if = 0 13. M, |= ̂•︀ if = 0 or M,− 1 |= 14. M, |= ♦ if M, |= for some ∈ [0..] 15. M, |= ■ if M, |= for all ∈ [0..] 16. M, |= F if + 1 = 17. M, |= ◦̂︀ if + 1 = or M,+1 |= 18. M, |= ♢ if M, |= for some ∈ [.. ) 19. M, |= □ if M, |= for all ∈ [.. )
An HT-trace M is a model of a temporal theory Γ if M,0 |= for all ∈ Γ . We omit specifying LTL satisfaction since it coincides with THT when HT-traces are total. Proposition 1 ([31, 24]). Let T be a trace of length , a temporal formula, and ∈ [0.. ) a time point.
Then, T, |= in LTL if ⟨T,T⟩, |= . □ Satisfaction of derived operators can be easily deduced, as shown next. □ Proposition 3 (Persistence). Let ⟨H, T⟩ be an HT-trace of length and be a temporal formula. Then, for any ∈ [0.. ), ̸= , if ⟨H, T⟩, |= then ⟨T, T⟩, |= (or, if preferred, T, |= ). □ As a corollary, we have that ⟨H, T⟩ |= ¬ if T ̸|= in LTL.
Given a set of THT-models, we define the ones in equilibrium as follows.
A total HT-trace ⟨T, T⟩ ∈ S is a temporal equilibrium model of S if there is no other H < T such that ⟨H, T⟩ ∈ S.
The trace T is called a temporal stable model (TS-model) of S. □
Given alphabet , a pure past formula is defined by the grammar:
::= | ⊥ | ¬ | 1 ∧ 2 | 1 ∨ 2 | • | 1 S 2 | 1 T 2. where ∈ .
Definition 3 (Past-present Program). Given alphabet , the set of temporal literals is defined as {, ¬, •, ¬• | ∈ }. We refer to its subset {, ¬ | ∈ } as regular literals, and {•, ¬• | ∈ } as past literals.
A past-present rule is either: • an initial rule of form ← • a dynamic rule of form ◦̂︀ □ ( ← ) • a final rule of form □ ( F → (⊥ ← ) ) where is an pure past formula for dynamic rules and = 1 ∧ · · · ∧ with ≥ 0 for initial and final rules, the are regular literals, = 1 ∨ · · · ∨ with ≥ 0 and ∈ . A past-present program is a set of past-present rules.
We let I ( ), D ( ), and F ( ) stand for the set of all initial, dynamic, and final rules in a temporal program , respectively. Additionally we refer to as the head of a rule and to as the body of . We let B () = and H () = for all types of rules above.
For example, let consider the following past-present program 1:
← ◦̂︀□ (ℎ ∨ ∨ ← ) ◦□ ( ← ℎ ∧ ¬ S ) ̂︀ ◦̂︀□ (ℎ ← )
We get I (1) = {(
in the scope of • (previous).
Definition 4 (Positive occurence). An occurrence of an atom in a formula is positive if it is in the antecedent of an even number of implications, negative otherwise.
An occurrence of an atom in a formula is present if it is not Definition 6 (Dependency graph). Given a past-present program over , we define its (positive) dependency graph G ( ) as (, ) such that (, ) ∈ if there is a rule ∈ such that ∈ H () ∩ and has positive and present occurence in B () that is not in the scope of negation. Definition 7 (Loop). A nonempty set ⊆ of atoms is called loop of if, for every pair , of atoms in , there exists a path of length > 0 from to in G ( ) such that all vertices in the path belong to .
We let L( ) denote the set of loops of . Due to the structure of past-present programs, dependencies from the future to the past cannot happen, and therefore there can only be loops within a same time point. To reflect this, the definitions above only consider atoms with present occurences. For example, rule ← ∧ • generate the edge (, ) but not (, ).
do not contain any loop.
For 1, we get for the initial rules
A past-present program is said to be tight if I ( ) and D ( ) G (I (1)) = ({, , ℎ, }, ∅)
L(I (1)) = ∅ and for the dynamic rules,
G (D (1)) = ({, , ℎ, }, {(, ℎ), (, ), (ℎ, )}) L(D (1)) = {{ℎ, }} Definition 9 (Temporal completion). We define the temporal completion formula of an atom in a past-present program over , denoted () as: □ (︀ ↔
⋁︁ ∈I ( ),∈H () where (, ) = B () ∧ ⋀︀∈H ()∖{} ¬.
The temporal completion formula of , denoted ( ) is
{ () | ∈ } ∪ { | ∈ I ( ) ∪ D ( ), H () = ⊥} ∪ F ( ) Theorem 1. Lets be a tight past-present program and T a trace of length . Then, T is a TS-model of if T is a LTL -model of ( ).
The completion of 1, (1) is □ ( ↔ I ∨ (¬I ∧ ¬ℎ ∧ ¬)) □ (ℎ ↔ (¬I ∧ ¬ ∧ ¬)) ∨ (¬I ∧ )) □ ( ↔ (¬I ∧ ¬ℎ ∧ ¬)) □ ( ↔ (¬I ∧ ℎ ∧ ¬ S ))
For = 2, (1) has a unique LTL -model {} · { ℎ, }, which is identical to
the TS-model of 1. Notice that for this example, the TS-models of the program match the
LTL -models of its completion despite the program not being tight. It is generally not the case.
Let 2 be the program made of the rules (
Lin and Zhao [27] introduced the concept of loop formulas to restrict circular derivations. In this section, we extend the notion of loop formula to past-present programs.
Let be a implication-free past-present formula and a loop. We define the supporting transformation of with respect to as
S⊥()
S()
S¬ () S ∧ () def = def = def = def = ⊥ {︃ ¬ ⊥ if ∈ otherwise S () ∧ S ()
for any atom ∈ S ∨ ()
S• () S T () S S () def = def = def = def = • S () ∨ S () S () ∧ (S () ∨ •( T ))
S () ∨ (S () ∧ •( S ))
Given a past-present program , the external support formula of a set of atoms ⊆
wrt , is defined as ES () =
⋁︁ ∈,H ()∩̸=∅ ︀( SB()() ∧
⋀︁ ∈H ()∖ ¬ ︀) For our examples 1 and 2, and = {ℎ, }, we have
ES 2 () = S() ∨ Sℎ∧¬S() = ⊥ ∨ (⊥ ∧ ¬ ∨ •(¬ S )) = S() ∨ (Sℎ() ∧ S¬S()) = S() ∨ (Sℎ() ∧ S¬() ∨ •(¬ S )) = ⊥ and
ES 1 () = S() ∨ Sℎ∧¬S() ∨ (¬ ∧ ¬)
= ¬ ∧ ¬
Rule (
We define the set of loop formulas of a past-present program over , denoted LF ( ), as:
∈ ∈
⋁︁ → ES I ( )() for any loop in I ( )
◦□
̂︀
︁( ⋁︁ → ES D( )() for any loop in D ( )
︁)
(
For our examples, we have and
LF (1) = ◦̂︀□ (ℎ ∨ → ¬ ∧ ¬)
LF (2) = ◦̂︀□ (ℎ ∨ → ⊥) matching the TS-models of the respective programs.
{} · { ℎ, } satisfies LF (1), but not LF (2). So, we have that (1) ∪ LF (1) has a unique LTL -model {} · { ℎ, }, while (2) ∪ LF (2) has no LTL -model,
Ferraris et al. [22] proposed an approach where the computation of the completion can be avoided by considering unitary cycles. In this section, we extend such results for past-present programs. We first redefine loops so that unitary cycles are included.
Definition 13 (Unitary cycle). A nonempty set ⊆ of atoms is called loop of if, for every pair , of atoms in , there exists a path (possibly of length 0) from to in ( ) such that all vertices in the path belong to .
With this definition, it is clear that any set consisting of a single atom is a loop. For example, L(D (1)) = {{}, {}, {ℎ}, {}, {ℎ, }}.
Theorem 3. Let be a past-present program and T a trace of length . Then, T is a TS-model of if T is a LTL -model of ∪ LF ( ).
With unitary cycle, LF (1) becomes
→ ⊤ → ⊥ ℎ → ⊥ → ⊥ ◦□ ( → ¬ℎ ∧ ¬) ̂︀ ◦̂︀□ ( → ¬ℎ ∧ ¬) ◦̂︀□ (ℎ → (¬ℎ ∧ ¬) ∨ ) ◦□ ( → ℎ ∧ ¬ S ) ̂︀ ◦̂︀□ (ℎ ∨ → ¬ ∧ ¬) 1 ∪ LF (1) has the same LTL -model (1) ∪ LF (1), {} · { ℎ, }, which is the TS-model of 1.
In this paper we have focused on the computation methods for temporal logic programming within the context of Temporal Equilibrium Logic over finite traces. More precisely, we have studied a fragment close to logic programming rules in the spirit of [26]: a past-present temporal logic program consists of a set of rules whose body refers to the past and present while their head refers to the present. This fragment is very interesting for implementation purposes since it can be solved by means of incremental solving techniques like those implemented in telingo. Moreover, restricting the body of the rules to only present and past formulas makes it so that the body of the rules can be seen as queries on the set of conclusions generated during the solving phase.
Contrary to the propositional case [22], where the answer sets of an arbitrary propositional formula can be captures by means of the classical models of another formula , in the temporal case this is not possible to do the same mapping among the temporal equilibrium models of a formula and the LTL models of another formula [18].
In this paper we show that past-present temporal logic programs can be efectively reduced to LTL formulas by means of completion and loop formulas. More precisely we extend the definition of completion and temporal loop formulas in the spirit of Lin and Zhao [ 27] to the temporal case, and we show that for tight past-present programs, the use of completion is suficient to achieve a reduction to an LTL formula. Moreover, when the program is not tight, we also show that the computation of the temporal completion and a finite number of loop formulas sufices to reduce TEL to LTL . Finally, we consider Ferraris et al. approach [22] where the computation of the completion can be automatically replaced by the consideration of unitary loops. In this contribution, we extend such result to the case of past-present logic programs.
As future work we plan to study in detail the relation between temporal completion and loop formulas and unfounded sets [22, 32], since the latter plays a central role in the solving algorithm of clingo [33, 34]. Lastly, we will study the case of past-present temporal programs with variables [35] in order to get a second-order characterisation of loop formulas, in the spirit of [36]. Twenty-fourth International Conference on Logic Programming (ICLP’08), volume 5366 of Lecture Notes in Computer Science, Springer-Verlag, 2008, pp. 190–205. [10] S. Demri, V. Goranko, M. Lange, Temporal Logics in Computer Science: Finite-State Systems, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2016. [11] A. Pnueli, The temporal logic of programs, in: Proceedings of the Eight-teenth Symposium on Foundations of Computer Science (FOCS’77), IEEE Computer Society Press, 1977, pp. 46–57. [12] P. Cabalar, G. P. Vega, Temporal equilibrium logic: A first approach, in: R. MorenoDíaz, F. Pichler, A. Quesada-Arencibia (Eds.), Proceedings of the Eleventh International Conference on Computer Aided Systems Theory (EUROCAST’17), volume 4739 of Lecture Notes in Computer Science, Springer-Verlag, 2007, pp. 241–248. [13] F. Aguado, P. Cabalar, M. Diéguez, G. Pérez, T. Schaub, A. Schuhmann, C. Vidal, Linear-time temporal answer set programming, Theory Pract. Log. Program. 23 (2023) 2–56. [14] D. Pearce, A new logical characterisation of stable models and answer sets, in: J. Dix, L. Pereira, T. Przymusinski (Eds.), Proceedings of the Sixth International Workshop on Non-Monotonic Extensions of Logic Programming (NMELP’96), volume 1216 of Lecture Notes in Computer Science, Springer-Verlag, 1997, pp. 57–70. [15] D. Pearce, Equilibrium logic, Annals of Mathematics and Artificial Intelligence 47 (2006) 3–41. [16] M. Gelfond, V. Lifschitz, The stable model semantics for logic programming, in: R. Kowalski, K. Bowen (Eds.), Proceedings of the Fifth International Conference and Symposium of Logic Programming (ICLP’88), MIT Press, 1988, pp. 1070–1080. [17] L. Bozzelli, D. Pearce, On the complexity of temporal equilibrium logic, in: Proceedings of the Thirtieth Annual Symposium on Logic in Computer Science (LICS’15), IEEE Computer Society Press, 2015, pp. 645–656. [18] L. Bozzelli, D. Pearce, On the expressiveness of temporal equilibrium logic, in: L. Michael, A. Kakas (Eds.), Proceedings of the Fifteenth European Conference on Logics in Artificial Intelligence (JELIA’16), volume 10021 of Lecture Notes in Artificial Intelligence , SpringerVerlag, 2016, pp. 159–173. [19] P. Cabalar, M. Diéguez, STELP — a tool for temporal answer set programming, in: [37], 2011, pp. 370–375. [20] P. Cabalar, S. Demri, Automata-based computation of temporal equilibrium models, in: G. Vidal (Ed.), Proceedings of the Twenty-first International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR’11), volume 7225 of Lecture Notes in Computer Science, Springer-Verlag, 2011, pp. 57–72. [21] F. Aguado, P. Cabalar, G. Pérez, C. Vidal, Loop formulas for splitable temporal logic programs, in: [37], 2011, pp. 80–92. [22] P. Ferraris, J. Lee, V. Lifschitz, A generalization of the Lin-Zhao theorem, Annals of
Mathematics and Artificial Intelligence 47 (2006) 79–101. [23] G. De Giacomo, M. Vardi, Linear temporal logic and linear dynamic logic on finite traces, in: F. Rossi (Ed.), Proceedings of the Twenty-third International Joint Conference on Artificial Intelligence (IJCAI’13), IJCAI/AAAI Press, 2013, pp. 854–860. [24] 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. [25] P. Cabalar, R. Kaminski, P. Morkisch, T. Schaub, telingo = ASP + time, in: M. Balduccini, Y. Lierler, S. Woltran (Eds.), Proceedings of the Fifteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’19), volume 11481 of Lecture Notes in Artificial Intelligence , Springer-Verlag, 2019, pp. 256–269. [26] D. Gabbay, The declarative past and imperative future: Executable temporal logic for interactive systems, in: B. Banieqbal, H. Barringer, A. Pnueli (Eds.), Proceedings of the Conference on Temporal Logic in Specification, volume 398 of Lecture Notes in Computer Science, Springer-Verlag, 1987, pp. 409–448. [27] F. Lin, J. Zhao, On tight logic programs and yet another translation from normal logic programs to propositional logic, in: G. Gottlob, T. Walsh (Eds.), Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI’03), Morgan Kaufmann Publishers, 2003, pp. 853–858. [28] E. Erdem, V. Lifschitz, Tight logic programs, Theory and Practice of Logic Programming 3 (2003) 499–518. [29] K. Clark, Negation as failure, in: H. Gallaire, J. Minker (Eds.), Logic and Data Bases,
Plenum Press, 1978, pp. 293–322. [30] F. Fages, Consistency of Clark’s completion and the existence of stable models, Journal of
Methods of Logic in Computer Science 1 (1994) 51–60. [31] 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.
[32] V. Lifschitz, Answer Set Programming, Springer, 2019.
[33] M. Gebser, R. Kaminski, B. Kaufmann, T. Schaub, Clingo = ASP + Control: Extended Report,
Technical Report, Universität Potsdam, 2014. URL: http://www.cs.uni-potsdam.de/
wv/pdfformat/gekakasc14a.pdf.
[34] M. Gebser, R. Kaminski, B. Kaufmann, T. Schaub, Clingo = ASP + control: Preliminary
report, in: M. Leuschel, T. Schrijvers (Eds.), Technical Communications of the Thirtieth
International Conference on Logic Programming (ICLP’14), volume 14(
Definition 14. Let ⟨H, T⟩ and ⟨H′, T⟩ be two HT-traces of length and let ∈ [0.. ). We say denote by ⟨H, T⟩ ∼ ⟨H′, T⟩ the fact for all ∈ [0..), = ′.
Proposition 4. For all HT-traces ⟨H, T⟩ and ⟨H′, T⟩ and for all ∈ [0.. ), if ⟨H, T⟩ ∼ ⟨H′, T⟩ then for all ∈ [0..) and for all past formulas , ⟨H, T⟩, |= if ⟨H′, T⟩, |= Definition 15 ( X). Let ⟨H, T⟩ be a HT-trace of length and ∈ [0.. ). We denote X the trace of length satisfying = ∅ for all ∈ [0..).
Lemma 1. For all HT-traces ⟨H, T⟩ of length , for all ∈ [0.. ) and for any pure past formula , if each present and positive occurrence of an atom from in is in the scope of negation then ⟨H, T⟩, |= if ⟨H ∖ X, T⟩, |= .
Proof of Lemma 1. By induction on . First, note that for any formula of the form ∨ , ∧ , T or S , if all present and positive occurrences of an atom are in the scope of negation in , then all present and positive occurrences of are also in the scope of negation in and .
• case ⊥: clearly, ⟨H, T⟩, ̸|= ⊥ and ⟨H ∖ X, T⟩, ̸|= ⊥. • case : we consider two cases. If ̸∈ , ⟨H, T⟩, |= if ∈ , if ∈ ∖ , if ⟨H ∖ X, T⟩, |= .
If ∈ , then has a present and positive occurence in , which is not in the scope of negation. Therefore, the lemma automatically holds. • case ¬ : ⟨H, T⟩, |= ¬ if ⟨T, T⟩, ̸|= if ⟨H ∖ X(), T⟩, |= ¬ (because of persistency). • case • : – if = 0, then ⟨H, T⟩, ̸|= • and ⟨H ∖ X, T⟩, ̸|= • . – if > 0, then ⟨H, T⟩, |= • if ⟨H, T⟩, − 1 |= . Let − 1 be such that −− 11 = ∅. Then, we can apply the induction hypothesis, so ⟨H, T⟩, − 1 |= if (IH) ⟨H ∖ X− 1, T⟩, − 1 |= . Since ⟨H ∖ X− 1, T⟩ ∼ ⟨H ∖ X, T⟩ (Proposition 4) then ⟨H ∖ X− 1, T⟩, − 1 |= if ⟨H ∖ X, T⟩, − 1 |= , if ⟨H ∖ X, T⟩, |= • . • case ∨ : ⟨H, T⟩, |= ∨ if ⟨H, T⟩, |= or ⟨H, T⟩, |= . Since all positive and present occurences of atoms from in and are in the scope of negation, we can apply the induction hypothesis to get ⟨H ∖ X, T⟩, |= or ⟨H ∖ X, T⟩, |= .
Therefore, ⟨H ∖ X, T⟩, |= ∨ . • case ∧ : Similar as for ∨ . • case S : ⟨H, T⟩, |= S if for some ∈ [0..], ⟨H, T⟩, |= and ⟨H, T⟩, |= for all ∈ (..]. By induction we get that if for some ∈ [0..], ⟨H ∖ X , T⟩, |= and ⟨H ∖ X, T⟩, |= for all ∈ (..]. Since ⟨H ∖ X, T⟩ ∼ ⟨H ∖ X, T⟩ for all ∈ [0..), by Proposition 4 we get that if for some ∈ [0..], ⟨H ∖ X, T⟩, |= and ⟨H ∖ X, T⟩, |= for all ∈ (..]. if ⟨H ∖ X, T⟩, |= S . • case T : assume by contradiction that ⟨H ∖ X, T⟩, ̸|= T . This means that there exist ∈ [0..] such that ⟨H ∖ X, T⟩, ̸|= and ⟨H ∖ X, T⟩, ̸|= for all ∈ (..]. Since ⟨H ∖ X, T⟩ ∼ ⟨H ∖ X, T⟩ for all ∈ [0..), by Proposition 4 we get that there exist ∈ [0..] such that ⟨H ∖ X, T⟩, ̸|= and ⟨H ∖ X, T⟩, ̸|= for all ∈ (..]. By induction, there exist ∈ [0..] such that ⟨H, T⟩, ̸|= and ⟨H, T⟩, ̸|= for all ∈ (..] if ⟨H, T⟩, ̸|= T : a contradiction. □ Definition 16. Let ⊆ and let > 0 and ∈ [0.. ). By X() we mean a trace of length satisfying the following conditions: 1. ⊆ () ⊆ ; 2. () = ∅ for all ∈ [0..).
Lemma 2. Let ⟨H, T⟩ be a HT-trace of length , an pure past formula. Let us consider the set of atoms ⊆ . For all ∈ [0.. ), if each positive occurrence of an atom from () ∖ in is in the scope of negation, ⟨H, T⟩, |= S () if ⟨H ∖ X(), T⟩, |= .
Proof of Lemma 2. By induction on . First, note that for any formula of the form ∨ , ∧ , T or S , if all present and positive occurrences of an atom are in the scope of negation in , then all present and positive occurrences of are also in the scope of negation in and .
• case ⊥: ⟨H, T⟩, ̸|= ⊥ and ⟨H ∖ X(), T⟩, ̸|= ⊥. • case ̸∈ : we consider the following two cases – If ̸∈ , S() = and, by definition, ̸∈ (). Therefore, ⟨H, T⟩, |= S() if ⟨H, T⟩, |= , if ∈ if ∈ ∖ (), if ⟨H ∖ X(), T⟩, |= . – If ∈ then ̸∈ () ∖ and S() = ⊥. Therefore, we get that ⟨H, T⟩, ̸|=
S() and ⟨H ∖ X(), T⟩, ̸|= . • case ¬ : ⟨H, T⟩, |= S¬ () if ⟨H, T⟩, |= ¬ , if ⟨T, T⟩, ̸|= , if ⟨H∖X(), T⟩, |= ¬ . • case • : ⟨H, T⟩, |= S• () if ⟨H, T⟩, |= • .
– If = 0, then both ⟨H, T⟩, 0 ̸|= • and ⟨H ∖ X()0, T⟩, 0 ̸|= • . – If > 0, then ⟨H, T⟩, |= • if ⟨H, T⟩, − 1 |= . By definition, () = ∅ for ∈ [0..) so by Lemma 1, ⟨H ∖ X(), T⟩, − 1 |= , if ⟨H ∖ X(), T⟩, |= • . • case ∧ : ⟨H, T⟩, |= S ∧ () if ⟨H, T⟩, |= S () and ⟨H, T⟩, |= S (), if (IH) ⟨H ∖ X(), T⟩, |= and ⟨H ∖ X(), T⟩, |= , if ⟨H ∖ X(), T⟩, |= ∧ . • case ∨ : ⟨H, T⟩, |= S ∨ () if ⟨H, T⟩, |= S () or ⟨H, T⟩, |= S (), if (IH) ⟨H ∖ X(), T⟩, |= or ⟨H ∖ X(), T⟩, |= , if ⟨H ∖ X(), T⟩, |= ∨ . • case S : ⟨H, T⟩, |= S S () if 1. ⟨H, T⟩, |= S () if ⟨H ∖ X(), T⟩, |= (IH) or 2. ⟨H, T⟩, |= S () and ⟨H, T⟩, |= •( S ) if ⟨H ∖ X(), T⟩, |= (IH) and ⟨H, T⟩, |= •( S ) if ⟨H ∖ X(), T⟩, |= and ⟨H ∖ X(), T⟩, |= •( S ) From the previous items we conclude if ⟨H ∖ X(), T⟩, |= ∨ ( ∧ • ( S )) if ⟨H ∖ X(), T⟩, |= S . • case T : ⟨H, T⟩, ̸|= S T () if 1. ⟨H, T⟩, ̸|= S () if ⟨H ∖ X(), T⟩, ̸|= (IH) or 2. ⟨H, T⟩, ̸|= S () and ⟨H, T⟩, ̸|= •( T ) if ⟨H ∖ X(), T⟩, ̸|= (IH) and ⟨H, T⟩, ̸|= •( T ) if ⟨H ∖ X(), T⟩, ̸|= and ⟨H ∖ X(), T⟩, ̸|= •( T ) From the previous items we conclude if ⟨H ∖ X(), T⟩, ̸|= ∧ ( ∨ • ( T )) if ⟨H ∖ X(), T⟩, ̸|= T . □ Proof of Theorem 1. From left to right, let us assume towards a contradiction that T is a temporal answer set of , but T is not an LTL-model of (). By construction, if T is a temporal answer set of then T is an LTL model of so T, 0 |= . Therefore, T, 0 |= , for all ∈ such that H () = ⊥ and T, 0 |= for all ∈ (). Since T, 0 ̸|= (), there exists ∈ such that
T, 0 ̸|= □ (︀ ↔
⋁︁ ∈I(),∈H() So, there exists ∈ [0.. ) such that
T, ̸|= ↔
⋁︁ ∈I(),∈H() 1. T, |= and T, ̸|= ⋁︀∈I(),∈H()(I ∧ (, )) ∨ ⋁︀∈D(),∈H()(¬I ∧ (, )): • If = 0 then we get that for all ∈ I (), if ∈ H () then ⟨T, T⟩, 0 ̸|= (, ).
Therefore, for all ∈ I (), if ∈ H () then ⟨T, T⟩, 0 ̸|= S(, ). Let H be a trace of length such that 0 = 0 ∖ {} and = for ∈ [1.. ). Clearly, H < T. We show a contradiction by proving that ⟨H, T⟩ |= : a) ⟨H, T⟩, 0 |= I (): note that ⟨T, T⟩, 0 |= B() → H () for all ∈ I (), if for any ∈ I (), ⟨T, T⟩, 0 ̸|= B() or ⟨T, T⟩, 0 |= H (). If ⟨T, T⟩, 0 ̸|= B() then, by persistence, ⟨H, T⟩, 0 ̸|= B(), and ⟨H, T⟩, 0 |= B() → H (). If ⟨T, T⟩, 0 |= B(), then ⟨T, T⟩, 0 |= H (). There are two cases.
– Case ̸∈ H (): ⟨T, T⟩, 0 |= H () so there is some ∈ H () such that ∈ 0 and ̸= . Then, ∈ 0, ⟨H, T⟩, 0 |= H () and ⟨H, T⟩, 0 |= . – Case ∈ H (): We know that ⟨T, T⟩, 0 ̸|= B () ∧ ⋀︀∈H ()∖{} ¬. Since, by assumption, ⟨T, T⟩, 0 |= B (), it follows ⟨T, T⟩, 0 ̸|= ⋀︀∈H ()∖{} ¬ Therefore, there is ∈ H () ∖ {} such that ∈ 0. Then ∈ 0, ⟨H, T⟩, 0 |= H () and ⟨H, T⟩, 0 |= .
As is chosen arbitrarily, ⟨H, T⟩ |= I ( ). b) ⟨H, T⟩, 0 |= D ( ): ⟨T, T⟩ |= D ( ), then ⟨T, T⟩, |= B () → H () for all ∈ D ( ) and ∈ [1.. ). Then, for any ∈ D ( ) and ∈ [1.. ), ⟨T, T⟩, ̸|= B () or ⟨T, T⟩, |= H (). If ⟨T, T⟩, ̸|= B () then, by persistence, ⟨H, T⟩, ̸|= B (), and ⟨H, T⟩, |= . If, ⟨T, T⟩, |= H (), there is some ∈ H () such that ∈ . = , so ∈ and ⟨H, T⟩, |= H ().
Then ⟨H, T⟩, |= . As and are chosen arbitrarily, ⟨H, T⟩ |= D ( ). c) ⟨H, T⟩, 0 |= F ( ): final rules are constraints, so ⟨T, T⟩ |= F ( ) implies ⟨H, T⟩ |= F ( ).
We showed that ⟨H, T⟩, 0 |= : a contradiction.
• If > 0: we follow a very similar reasoning as for the case = 0. 2. T, ̸|= but T, |= ⋁︀∈I ( ),∈H ()(I ∧ (, )) ∨ ⋁︀∈D( ),∈H ()(¬I ∧ (, )): again, we consider two cases here • there exists ∈ I ( ), ∈ H () and T, |= I ∧ (, ): in this case, it follows that = 0, so T, 0 |= and T, 0 |= (, ). Therefore, T, 0 |= B (). Since T, 0 |= and T, 0 |= B () then T, 0 |= for some ∈ H (), which contradicts T, 0 ̸|= and T, 0 |= ¬ for all ∈ H () ∖ {}. • there exists ∈ D ( ), ∈ H () and T, |= ¬I ∧ (, ): in this case we conclude that > 0 and so T, |= and T, |= (, ). Therefore, T, |= B (). Since T, 0 |= and T, |= B () then T, |= for some ∈ H (). However, from T, |= (, ) and T, ̸|= we conclude that T, ̸|= for all ∈ H (): a contradiction.
For the converse direction, assume, again, by contradiction that ⟨T, T⟩ is not a TEL model of . We consider two cases: 1. ⟨T, T⟩, 0 ̸|= . Therefore, there exists ∈ such that ⟨T, T⟩, 0 ̸|= . Clearly, cannot be a constraint, otherwise we would already reach a contradiction. We still have to check two cases: • If ∈ I ( ), then ⟨T, T⟩, 0 |= B () and ⟨T, T⟩, 0 ̸|= H (). Take any ∈ H (). It follows that ⟨T, T⟩, 0 |= I ∧ (, ). so ⟨T, T⟩, 0 ̸|= (): a contradiction. • If ∈ D ( ) we follow a similar reasoning as for the previous case. 2. ⟨T, T⟩, 0 |= but ⟨H, T⟩, 0 |= for some H < T. By definition, there exists ≥ 0 such that ⊂ . Let us take the smallest satisfying this property. Therefore, = for all ∈ [0..). .Moreover, Let us take ∈ ∖ and let us proceed depending on the value of • If > 0 and ∈ then ⟨T, T⟩, |= () then there exists ∈ D ( ) such that ⟨T, T⟩, |= (, ). Therefore H () ∖ {} ∪ = 0 Since ̸∈ then ⟨H, T⟩, ̸|= H () and ⟨H, T⟩, ̸|= B ().
At this point of the proof we have that ⟨T, T⟩, |= B (), ⟨H, T⟩, ̸|= B () and ∖ = ∅ for any < . By Lemma 1, there must be some ∈ ∖ with a present and positive occurence in B () that is not in the scope of negation. Then, for any ∈ ∖ , there is some ∈ ∖ such that (, ) ∈ (D ( )). is tight, so (D ( )) is acyclic. Then, there is a topological ordering of the nodes in (D ( )), and therefore of the atoms in ∖ , such that if , ∈ ∖ and (, ) ∈ (D ( )), then appears before in the topoligical ordering. Then, there is no outgoing edge from the last node in the ordering, which contradict the fact that, for any ∈ ∖ , there is some ∈ ∖ such that (, ) ∈ (D ( )). • If = 0 we proceed as in the previous case. □
We first prove that if T is a temporal answer set of , then T is a LTL -model of ( ) and LF ( ). The proof for ( ) is the same as for Theorem 1. Remains to prove that T is a LTL -model of LF ( ). Assume by contradiction that ⟨T, T⟩ ̸|= LF ( ). Two diferent cases must be considered: • there is a loop in G (D ( )) such that ⟨T, T⟩, ̸|= ⋁︀∈ → ES D( )() for some ∈ [1.. ), or • there is a loop in G (I ( )) such that ⟨T, T⟩, 0 ̸|= ⋁︀∈ → ES I ( )().
For the first case, let H be a trace of length such that = ∖ and = otherwise. We show that ⟨H, T⟩, 0 |= , which will contradict the hypothesis T is a TEL -model of : 1. ⟨H, T⟩, 0 |= I ( ): follows from ⟨T, T⟩ |= I ( ) by Lemma 1 as 0 ∖ 0 = ∅. 2. ⟨H, T⟩, 0 |= F ( ): follows from ⟨T, T⟩ |= F ( ) as rules in F ( ) are constraints. 3. ⟨H, T⟩, 0 |= D ( ): ⟨T, T⟩, 0 |= D ( ) since T is a TEL -model of . Therefore, ⟨T, T⟩, |= for all ∈ [1.. ) and for all ∈ D ( ). Then, ⟨T, T⟩, ̸|= B () or ⟨T, T⟩, |= H (). If ⟨T, T⟩, ̸|= B (), by persistence, ⟨H, T⟩, ̸|= B () and ⟨H, T⟩, |= . If ⟨T, T⟩, |= B (), then ⟨T, T⟩, |= H ().
In the case ̸= , = and ⟨T, T⟩, |= H () imply ⟨H, T⟩, |= H ().In the case = , we have two cases.
• if ⟨T, T⟩, ̸|= SB()(), then, as ( ∖ ) ∖ = ∅ and ∖ = ∅ for < , by
Lemma 2, ⟨H, T⟩, ̸|= B (). So ⟨H, T⟩, |= . • if ⟨T, T⟩, |= SB()() and H () ∩ = ∅ then ⟨H, T⟩, |= H () follows from ⟨T, T⟩, |= H () and ⟨H, T⟩, |= . • if ⟨T, T⟩, |= SB()() and H () ∩ = ∅ then – if there is some ∈ H () ∖ such that ∈ , then ∈ . So ⟨H, T⟩, |=
H () and then ⟨H, T⟩, |= . – if there is no ∈ H () ∖ such that ∈ , then ⟨T, T⟩, |= ⋀︀∈H ()∖ ¬.
As we also have ⟨T, T⟩, |= SB()(), ⟨T, T⟩, |= ⋁︀∈ → ES D( )(), which contradict our hypothesis.
The proof of the second case follows a similar reasoning as for the first one.
Next, we prove that if T is a LTL -model of ( ) and LF ( ), then T is a TEL -model of . The proof for ⟨T, T⟩ |= is the same as for Theorem 1. Remains to prove that there is no H < T such that ⟨H, T⟩ |= .
Let assume that there exists such a trace H, and let be the smallest time point such that ⊂ . Therefore, = for all ∈ [0..).
• I⋀f︀∈>H (0:)∖L{et}¬∈). ∖As. ⟨T∈, T⟩, |=therei(ss)o,msoe⟨ Tru,lTe⟩, ∈|= D (↔ )⋁︀su∈cDh(th),a∈tH()∈(BH(()∧), ⟨T, T⟩, |= B (), and ⟨T, T⟩, |= ⋀︀∈H ()∖{} ¬. ⟨H, T⟩ |= , so ⟨H, T⟩, |= B () → ∨ ⋁︀∈H ()∖{} . Then, ⟨H, T⟩, ̸|= B () or ⟨H, T⟩, |= or ⟨H, T⟩, |= ⋁⋁︀︀∈H ()∖{} . As ̸∈ , ⟨H, T⟩, ̸|= . As ⟨T, T⟩, |= ⋀︀∈H ()∖{} ¬, ⟨H, T⟩, ̸|= ∈H ()∖{} . So, ⟨H, T⟩, ̸|= B (). ⟨T, T⟩, |= B (), ⟨H, T⟩, ̸|= B () and ∖ = ∅ for < , so, by Lemma 1, there must be some ∈ ∖ with a present and positive occurence in B () that is not in the scope of negation. Therefore, for any ∈ ∖ , there is some ∈ ∖ such that (, ) ∈ (D( )). It implies a loop in D( ), with ⊆ ∖ .
The strongly connected components (SCC) of the dependency graph of D( ) over ∖ form a directed acyclic graph, so there is some SCC , such that, for any ∈ , there is no ∈ ( ∖ ) ∖ such that (, ) ∈ G(D( )).
For any ∈ ∖ , ⟨H, T⟩, ̸|= B (), for all ∈ D( ) such that ∈ H () and ⟨T, T⟩, |= ⋀︀∈H ()∖{} ¬. So ⟨H, T⟩, ̸|= B (), for all ∈ D( ) such that ∩ H () ̸= ∅ and ⟨T, T⟩, |= ⋀︀∈H ()∖ ¬. Let X be a trace of length with = and = ∅ for ̸= . For any ∈ there is no ∈ ( ∖ ) ∖ such that (, ) ∈ G(D( )), so all positive and present occurences of atoms from in B () are in the scope of negation. Then, we can apply Lemma 1, and get that ⟨T ∖ X, T⟩, ̸|= B (), for all ∈ D( ) such that ∩ H () ̸= ∅ and ⟨T, T⟩, |= ⋀︀∈H ()∖ ¬. Then, as ∖ = ∅, by Lemma 2, ⟨T, T⟩, ̸|= SB()(), for all ∈ D( ) such that ∩ H () ̸= ∅ and ⟨T, T⟩, |= ⋀︀∈H ()∖ ¬. So, ⟨T, T⟩, ̸|= ⋁︀∈ → ES D( )(), and then ⟨T, T⟩ ̸|= LF ( ). Contradiction. • Case = 0: we reach a contradiction in a similar way as above. □
We first prove that if T is a temporal answer set of , then T is a LTL -model of ∪ LF ( ). T is a temporal answer set of , so T is a LTL -model of . We can show that T is a LTL -model of LF ( ) the same way as for Theorem 2.
Next, we prove that if T is a LTL -model of ∪ LF ( ), then T is a temporal answer set of . It amounts to showing that there is no H < T such that ⟨H, T⟩ |= . Let assume that there is such a trace H, and let be the smallest time point such that ⊂ . 1. I⋀f︀∈>H (0,)L∖{et}¬∈).∖As. ⟨∈T,T,⟩th|=erLeFex(ist)s, so ∈⟨TD,T(⟩,) s|=uch ↔tha⋁t︀∈∈D(H),(∈)H, (⟨T)(,STB⟩(,)(|=)∧ SB()() and ⟨T, T⟩, |= ⋀︀∈H ()∖{} ¬. ⟨H, T⟩ |= , so ⟨H, T⟩, |= B () → ∨ ⋁︀∈H ()∖{} . Then, ⟨H, T⟩, ̸|= B () or ⟨H, T⟩, |= or ⟨H, T⟩, |= ⋁︀ As ̸∈ , ⟨H, T⟩, ̸|= . As ⟨T, T⟩, |= ⋀︀∈H ()∖{} ¬, ⟨H, T⟩, ̸|= ⋁︀∈∈HH (())∖∖{{}} .. So, ⟨H, T⟩, ̸|= B (). ⟨T, T⟩, |= SB()(), ⟨H, T⟩, ̸|= B () and ∖ = ∅ for < , so, by Lemma 2, there must be some ∈ ∖ with a present and positive occurence in B () that is not in the scope of negation. Therefore, for any ∈ ∖ , there is some ∈ ∖ such that (, ) ∈ (D( )). It implies a loop in D( ), with ⊆ ∖ .
The strongly connected components (SCC) of the dependency graph of D( ) over ∖ form a directed acyclic graph, so there is some SCC , such that, for any ∈ , there is no ∈ ( ∖ ) ∖ such that (, ) ∈ G(D( )).
For any ∈ ∖ , ⟨H, T⟩, ̸|= B (), for all ∈ D( ) such that ∈ H () and ⟨T, T⟩, |= ⋀︀∈H ()∖{} ¬. So ⟨H, T⟩, ̸|= B (), for all ∈ D( ) such that ∩ H () ̸= ∅ and ⟨T, T⟩, |= ⋀︀∈H ()∖ ¬. Let X be a trace of length with = and = ∅ for ̸= . For any ∈ there is no ∈ ( ∖ ) ∖ such that (, ) ∈ G(D( )), so all positive and present occurences of atoms from in B () are in the scope of negation. Then, we can apply Lemma 1, and get that ⟨T ∖ X, T⟩, ̸|= B (), for all ∈ D( ) such that ∩ H () ̸= ∅ and ⟨T, T⟩, |= ⋀︀∈H ()∖ ¬. Then, as ∖ = ∅, by Lemma 2, ⟨T, T⟩, ̸|= SB()(), for all ∈ D( ) such that ∩ H () ̸= ∅ and ⟨T, T⟩, |= ⋀︀∈H ()∖ ¬. So, ⟨T, T⟩, ̸|= ⋁︀∈ → ES D( )(), and then ⟨T, T⟩ ̸|= LF ( ): a contradiction. 2. For the case when = 0 we reach a contradiction in a similar way as above.