Loop Formulas for Splitable Temporal Logic Programs

Loop Formulas for Splitable Temporal Logic Programs? Felicidad Aguado, Pedro Cabalar, Gilberto P´erez and Concepci´on Vidal Department of Computing, University of Corunna (Spain) {aguado,cabalar,gperez,eicovima}@udc.es

Abstract. In this paper, we study a method for computing temporal equilibrium models, a generalisation of stable models for logic programs with temporal operators, as in Linear Temporal Logic (LTL). To this aim, we focus on a syntactic subclass of these temporal logic programs called splitable and whose main property is satisfying a kind of “future projected” dependence present in most dynamic scenarios in Answer Set Programming (ASP). Informally speaking, this property can be expressed as “past does not depend on the future.” We show that for this syntactic class, temporal equilibrium models can be captured by an LTL formula, that results from the combination of two well-known techniques in ASP: splitting and loop formulas. As a result, an LTL model checker can be used to obtain the temporal equilibrium models of the program.

1

Introduction

Although transition systems frequently appear in scenarios and applications of Non-Monotonic Reasoning (NMR), most NMR formalisms are not particularly thought for temporal reasoning. Instead, NMR approaches are typically “static,” in the sense that time instants are treated as one more argument for predicates representing actions and fluents. This has been usual, for instance, when representing temporal scenarios in Answer Set Programming (ASP) [1, 2], a successful NMR paradigm based on the stable model semantics [3] for logic programs. In this case, it is frequent that program rules depend on a parameter T , the previous situation, and the value T+1 representing its successor state. For instance, if t represents the action of toggling a switch that can take two positions, d (down) and u (up), the corresponding effect axioms would be encoded as: u(T +1) ← t(T ), d(T )

(1)

d(T +1) ← t(T ), u(T )

(2)

Similarly, the inertia law would typically look like the pair of rules:

?

u(T +1) ← u(T ), not d(T +1)

(3)

d(T +1) ← d(T ), not u(T +1)

(4)

This research was partially supported by Spanish MEC project TIN2009-14562-C0504 and Xunta de Galicia project INCITE08-PXIB105159PR.

Since ASP tools are constrained to finite domains, a finite bound n for the number of transitions is usually fixed, so that the above rules are grounded for T = 0, . . . , n − 1. To solve a planning problem, for instance, we would iterate multiple calls to some ASP solver and go increasing the value of n = 1, 2, 3, . . . in each call, until a (minimal length) plan is found. Of course, this strategy falls short for many temporal reasoning problems, like proving the non-existence of a plan, or checking whether two NMR system representations are strongly equivalent, that is, whether they always have the same behaviour, even after adding some common piece of knowledge, and for any narrative length we consider. To overcome these limitations, [4] introduced an extension of ASP to deal with modal temporal operators. Such an extension was the result of mixing two logical formalisms: (1) Equilibrium Logic [5, 6] that widens the concept of stable models to the general syntax of arbitrary theories (propositional and even first order); and (2) the well-known Linear Temporal Logic [7] (LTL) dealing with operators like  (read as “always”), ♦ (“eventually”), (“next”), U (“until”) and R (“release”). The result of this combination received the name of Temporal Equilibrium Logic (TEL). As happens with Equilibrium Logic, TEL is defined in terms of a monotonic formalism, in this case called Temporal Here-and-There (THT), plus an ordering relation among models, so that only the minimal ones are selected (inducing a non-monotonic consequence relation). These minimal models receive the name of Temporal Equilibrium Models and can be seen as the analogous of stable models for the temporal case. As an example, the rules (1)-(4) can be respectively encoded in TEL as: (d ∧ t → u)

(5)

(u ∧ t → d)

(6)

(u ∧ ¬ d → u)

(7)

(d ∧ ¬ u → d)

(8)

In [8] it was shown how to use equivalence in the logic of THT as a sufficient condition for strong equivalence of two arbitrary TEL theories. The THTequivalence test was performed by translating THT into LTL and using a model checker afterwards. This technique was applied on several examples to compare different alternative ASP representations of the same temporal scenario. Paradoxically, although this allowed an automated test to know whether two representations had the same behaviour, computing such a behaviour, that is, automatically obtaining the temporal equilibrium models of a given theory was still an open topic. When compared to the ASP case, part of the difficulties for computing temporal equilibrium models came from the fact that the general syntax of TEL allows complete arbitrary nesting of connectives (that is, it coincides with general LTL), whereas ASP syntax is constrained to disjunctive logic programs, that is, rules with a body (the antecedent) with a conjunction of literals, and a head (the consequent) with a disjunction of atoms. In a recent work [9], it was shown that TEL could be reduced to a normal form closer to logic programs

where, roughly speaking, in place of an atom p we can also use p, and any rule can be embraced by . This normal form received the name of Temporal Logic Programs (TLPs) – for instance, (5)-(8) are TLP rules. In this work we show how to compute the temporal equilibrium models for a subclass of TLPs called splitable. This subclass has a property we can call future projected dependence and that informally speaking can be described as “past does not depend on the future.” Formally, this means that we cannot have rules where a head atom without depends on a body atom with . In our example, (5)-(8) are also splitable TLP rules whereas, for instance, the following TLP rules are not in splitable form: (¬ p → p)

(9)

( p → p)

(10)

since the truth of p “now” depends on p in the next situation p. This syntactic feature of splitable TLPs allows us to apply the so-called splitting technique [10] (hence the name of splitable) to our temporal programs. Informally speaking, splitting is applicable when we can divide an ASP program Π into a bottom Π0 and a top Π1 part, where Π0 never depends on predicates defined in Π1 . If so, the stable models of Π can be computed by first obtaining the stable models of Π0 , and then using them to simplify Π1 and compute the rest of information in a constructive way. In the case of splitable TLPs, however, we cannot apply splitting by relying of multiple calls to an ASP solver since, rather than a single split between bottom and top part, we would actually have an infinite sequence of program “slices” Π0 , Π1 , Π2 , . . . where each Πi depends on the previous ones. To solve this problem, we adopt a second ASP technique called Loop Formulas [11, 12], a set of formulas LF (Π) for some program Π so that the stable models of the latter coincide with the classical models of Π ∪ LF (Π). In our case, LF (Π) will contain formulas preceded by a  operator, so that they affect to all program slices. As a result, the temporal equilibrium models of Π will correspond to the LTL models of Π ∪ LF (Π), which can be computed using an LTL model checker as a back-end. The rest of the paper is organised as follows. In the next section, we recall the syntax and semantics of TEL. Section 3 describes the syntax of splitable TLPs and their relation to stable models. Next, in Section ??, we explain how to construct the set of loop formulas LF (Π) for any splitable TLP Π, proving also that the LTL models of Π ∪ LF (Π) are the temporal equilibrium models of Π. In Section ?? we comment a pair of examples and finally, Section ?? concludes the paper.

2

Preliminaries

Given a set of atoms At, a formula F is defined as in LTL following the grammar: F ::= p | ⊥ | F1 ∧ F2 | F1 ∨ F2 | F1 → F2 | F | F | ♦F

where p ∈ At. A theory is a finite set of formulas. We use the following derived operators1 and notation: def

¬F = F → ⊥

def

i F = ( i−1 F )

def

> = ¬⊥ def

0

F ↔ G = (F → G) ∧ (G → F )

(with i > 1)

def

F = F

The semantics of the logic of Temporal Here-and-There (THT) is defined in terms of sequences of pairs of propositional interpretations. A (temporal) interpretation M is an infinite sequence of pairs mi = hHi , Ti i with i = 0, 1, 2, . . . where Hi ⊆ Ti are sets of atoms standing for here and there respectively. For simplicity, given a temporal interpretation, we write H (resp. T) to denote the sequence of pair components H0 , H1 , . . . (resp. T0 , T1 , . . . ). Using this notation, we will sometimes abbreviate the interpretation as M = hH, Ti. An interpretation M = hH, Ti is said to be total when H = T. Given an interpretation M and an integer number k > 0, by (M, k) we denote a new interpretation that results from “shifting” M in k positions, that is, the sequence of pairs hHk , Tk i, hHk+1 , Tk+1 i, hHk+2 , Tk+2 i, . . . Note that (M, 0) = M. Definition 1 (satisfaction). An interpretation M = hH, Ti satisfies a formula ϕ, written M |= ϕ, when: 1. 2. 3. 4. 5. 6. 7.

M |= p if p ∈ H0 , for any atom p. M |= ϕ ∧ ψ if M |= ϕ and M |= ψ. M |= ϕ ∨ ψ if M |= ϕ or M |= ψ. hH, Ti |= ϕ → ψ if hx, Ti 6|= ϕ or hx, Ti |= ψ for all x ∈ {H, T}. M |= ϕ if (M, 1) |= ϕ. M |= ϕ if ∀j ≥ 0, (M, j) |= ϕ M |= ♦ϕ if ∃j ≥ 0, (M, j) |= ϕ

A formula ϕ is valid if M |= ϕ for any M. An interpretation M is a model of a theory Γ , written M |= Γ , if M |= α, for all formula α ∈ Γ . We will make use of the following THT-valid equivalences: ¬(F ∧ G) ↔ ¬F ∨ ¬G

(11)

¬(F ∨ G) ↔ ¬F ∧ ¬G

(12)

(F ⊕ G) ↔ F ⊕ G

(13)

⊗F ↔⊗ F

(14)

for any binary connective ⊕ and any unary connective ⊗. This means that De Morgan laws (11),(12) are valid, and that we can always shift the operator to all the operands of any connective. 1

As shown in [9], the LTL binary operators U (“until”) and R (“release”) can be removed by introducing auxiliary atoms.

The logic of THT is an orthogonal combination of the logic of Here-and-There (HT) [13] and the (standard) linear temporal logic (LTL) [7]. On the one hand, HT is obtained by disregarding temporal operators, so that only the pair of sets of atoms hH0 , T0 i is actually relevant and we use conditions 1-3 in Definition 1 for satisfaction of propositional theories. On the other hand, if we restrict the semantics to total interpretations, hT, Ti |= ϕ corresponds to satisfaction of formulas T |= ϕ in LTL. This last correspondence allows rephrasing item 4 of Definition 1 as: 4’. hH, Ti |= ϕ → ψ if both (1) hH, Ti |= ϕ implies hH, Ti |= ψ; and (2) T |= ϕ → ψ in LTL. Similarly hH, Ti |= ϕ ↔ ψ if both (1) hH, Ti |= ϕ iff hH, Ti |= ψ; and (2) T |= ϕ ↔ ψ in LTL. The following proposition can also be easily checked. Proposition 1. For any Γ and any M = hH, Ti, if M |= Γ then T |= Γ .



We proceed now to define an ordering relation among THT models of a temporal theory, so that only the minimal ones will be selected. Given two interpretations M = hH, Ti and M0 = hH0 , T0 i we say that M0 is lower or equal than M, written M0 ≤ M, when T0 = T and for all i ≥ 0, Hi0 ⊆ Hi . As usual, M0 < M stands for M0 ≤ M but M0 6= M. Definition 2 (Temporal Equilibrium Model). An interpretation M is a temporal equilibrium model of a theory Γ if M is a total model of Γ and there is no other M0 < M, M0 |= Γ .  Note that any temporal equilibrium model is total, that is, it has the form hT, Ti and so can be actually seen as an interpretation T in the standard LTL. Temporal Equilibrium Logic (TEL) is the logic induced by temporal equilibrium models. When we restrict the syntax to ASP programs and HT interpretations hH0 , T0 i we talk about (non-temporal) equilibrium models, which coincide with stable models in their most general definition [14].

3

Temporal Logic Programs

As we said in the introduction, in [9] it was shown that, by introducing auxiliary atoms, any temporal theory could be reduced to a normal form we proceed to describe. Given a signature At, we define a temporal literal as any expression in the set {p, ¬p, p, ¬ p | p ∈ At}. Definition 3 (Temporal rule). A temporal rule is either: 1. an initial rule of the form B1 ∧ · · · ∧ Bn → C1 ∨ · · · ∨ Cm where all the Bi and Cj are temporal literals, n ≥ 0 and m ≥ 0.

(15)

2. a dynamic rule of the form r, where r is an initial rule. 3. a fulfillment rule like (p → q) or like (p → ♦q) with p, q atoms.



In the three cases, we respectively call rule body and rule head to the antecedent and consequent of the (unique) rule implication. In initial (resp.) dynamic rules, we may have an empty head m = 0 corresponding to ⊥ – if so, we talk about an initial (resp. dynamic) constraint. A temporal logic program 2 (TLP for short) is a finite set of temporal rules. A TLP without temporal operators, that is, a set of initial rules without , is said to be an ASP program 3 . As an example of TLP take the program Π1 consisting of: ¬a ∧ b → a

(16)

(a → b)

(17)

(¬b → a)

(18)

where (16) is an initial rule and (17),(18) are dynamic rules. Looking at the semantics of  it seems clear that we can understand a dynamic rule r as an infinite sequence of expressions like i r, one for each i ≥ 0. Using (13),(14) we can shift i inside all connectives in r so that i r is equivalent to an initial rule resulting from prefixing any atom in r with i . To put an example, if r = (18) then 2 r would correspond to (¬ 2 b → 3 a). Definition 4 (i-expansion of a rule). Given i ≥ 0, the i-expansion of a dynamic rule r, written (r)i , is a set of rules defined as:  if i = 0 and r contains some ‘ ’ ∅ (r)i { j r | 0 ≤ j ≤ i − 1} if i > 0 and r contains some ‘ ’  { j r | 0 ≤ j ≤ i} otherwise If r is an initial rule, its i-expansion is defined as:  ∅ if i = 0 and r contains some ‘ ’ i def r = r otherwise



In this way, the superindex i refers to the longest sequence of ’s used in the 3 rule. For instance, (18) would be: { (¬b → a), (¬ b → 2 a), (¬ 2 b → 3 a) } We extend this notation to programs, so that given a TLP Π its i-expansion Π i results from replacing each initial or dynamic rule r in Π by ri . An interesting observation is that we can understand each Π i as a (non-temporal) ASP def

program for signature Ati = {“ j p” | p ∈ At, 0 ≤ j ≤ i} where we understand each “ j p” as a different propositional atom. This same notation can be applied 2

3

In fact, as shown in [9], this normal form can be even more restrictive: initial rules can be replaced by atoms, and we can avoid the use of literals of the form ¬ p. In ASP literature, this is called a a disjunctive program with negation in the head.

to interpretations. If T is an LTL interpretation (an infinite sequence of sets of atoms) for signature At its i-expansion would be the corresponding proposidef

tional interpretation for signature Ati defined as Ti = { i p | p ∈ Ti } and if M = hH, Ti is a THT interpretation then its i-expansion is defined as the HT def

interpretation Mi = hHi , Ti i. In all these cases, we also define the ω-expansion (or simply, expansion) as the infinite union of all i-expansions for all i ≥ 0. Thus, def S for instance (r)ω = i≥0 (r)i and similarly for Π ω , Atω , Tω and Mω . It is interesting to note that, for any classical interpretation T0 for signature Atω , we can always build a corresponding LTL interpretation T in signature At such that Tω = T0 . The following theorem establishes the correspondence between a temporal program and its expansion. Theorem 1. Let Π be a TLP without fulfillment rules. Then hT, Ti is a temporal equilibrium model of Π under signature At iff Tω is a stable model of Π ω under signature Atω .  The above theorem allows us reading a TLP with initial and dynamic rules as an ASP program with infinite “copies” of the same rule schemata. In many cases, this allows us to foresee the temporal equilibrium models of a TLP. For instance, if we look at our example TLP Π2 , it is easy to see that we should 0 get T0 = ∅ as the only rule affecting the situation i = 0 is (17) = (a → b). For 1 1 situation i = 1 we would have rules ( a → b) ∈ (17) and (¬b → a) ∈ (18) so that, given T0 we obtain a ∧ b, that is, T1 = {a, b}. For i = 2, the involved 2 2 rules are ( 2 a → 2 b) ∈ (17) and (¬ b → 2 a) ∈ (18) so that, given T1 we obtain T2 = ∅. In a similar way, for i = 3 we have rules ( 2 a → 2 b) and (¬ 2 b → 3 a) leading to T3 = {a, b} and then this behaviour is repeated. To sum up, we get a unique temporal equilibrium model hT, Ti for Π2 where T can be captured by the regular expression ( ∅ {a, b} )+ . In some cases, however, we may face new situations that are not common in standard ASP. For instance, consider the TLP Π2 consisting of the two rules (9), (10). This program has no temporal equilibrium models. To see why, note that Π2 is equivalent to (¬ p ∨ p → p) that, in its turn, is LTL-equivalent to p. Thus, the only LTL-model T of Π2 has the form Ti = {p} for any i ≥ 0. However, it is easy to see that the interpretation hH, Ti with Hi = ∅ for all i ≥ 0 is also a THT model, whereas H < T. Note that, by Theorem 1, this means that the ASP program Π2ω has no stable models, although it is an acyclic program and (finite) acyclic programs always have a stable model. The intuitive reason for this is that atoms i p infinitely depend on the future, and there is no way to build a founded reasoning starting from facts or the absence of them at a given end point4 . 4

In fact, this example was extracted from a first-order counterpart, the pair of rules ¬p(s(X)) → p(X) and p(s(X)) → p(X), that were used in [15] to show that an acyclic program without a well-founded dependence ordering relation may have no stable models.

4

Splitting a Temporal Logic Program

Fortunately, most ASP programs dealing with transition systems represent rules so that past does not depend on the future. This is what we called future projected dependence and can be captured by the following subclass of TLPs. Definition 5 (Splitable TLP). A TLP Π for signature At is said to be splitable if Π consists of rules of any of the forms: B∧N →H

(19)

0

0

0

(20)

0

0

0

(21)

B ∧ B ∧ N ∧ N → H

(B ∧ B ∧ N ∧ N → H )

where B and B 0 are conjunctions of atoms, N and N 0 are conjunctions of negative literals like ¬p with p ∈ At, and H and H 0 are disjunctions of atoms.  The set of rules of form (19) in Π will be denoted ini0 (Π) and correspond to initial rules for situation 0. The rules of form (20) in Π will be represented as ini1 (Π) and are initial rules for the transition between situations 0 and 1. Finally, the set of rules of form (21) is written dyn(Π) and contains dynamic rules. Both in (20) and (21), we understand that operator is actually shifted until it only affects to atoms – this is always possible due to equivalences (13), (14). We will also use the formulas B, B 0 , N, N 0 , H and H 0 as sets, denoting the atoms that occur in each respective formula. Notice that a rule of the form (B ∧ N → H) (i.e., without operator) is not splitable but can be transformed into the equivalent pair of rules B ∧N → H and ( B ∧ N → H) which are both splitable. For instance, (17) becomes the pair of rules: a→b ( a → b)

(22) (23)

As an example, Π2 =(9)-(10) is not splitable, whereas Π1 =(16),(18),(22),(23) is splitable being ini0 (Π1 )=(22), ini1 (Π1 )=(16) and dyn(Π1 )=(22),(18). In particular, in (16) we have the non-empty sets B 0 = {b}, N = {a} and H 0 = {a}, whereas for (18) the sets are N = {b}, H 0 = {a}. It can be easily seen that the rules (5)-(8) are also in splitable form. As we explained in the introduction, the most interesting feature of splitable TLPs is that we can apply the so-called splitting technique [10] to obtain their temporal equilibrium models in an incremental way. Let us briefly recall this technique for the case of ASP programs. Following [10] we define: Definition 6 (Splitting set). Let Π be an ASP program consisting of (nontemporal) rules like (19). Then a set of atoms U is a splitting set for Π if, for any rule like (19) in Π: if H ∩ U 6= ∅ then (B ∪ N ∪ H) ⊆ U . The set of rules satisfying (B ∪ N ∪ H) ⊆ U are denoted as bU (Π) and called the bottom of Π with respect to U . 

Consider the program: a→c

(24)

b→d

(25)

¬b → a

(26)

¬a → b

(27)

The set U = {a, b} is a splitting set for Π being bU (Π) = {(26), (27)}. The idea of splitting is that we can compute first each stable model X of bU (Π) and then use the truth values in X for simplifying the program Π \ bU (Π) from which the rest of truth values for atoms not in U can be obtained. Formally, given X ⊆ U ⊆ At and an ASP program Π, for each rule r like (19) in Π such that ˆ ∧N ˆ → H where H ∩ U ⊆ X and N ∩ U is disjoint from X, take the rule rˆ : B ˆ ˆ B = (B \ U ) and N = (N \ U ). The program consisting of all rules rˆ obtained in this way is denoted as eU (Π, X). Note that this program is equivalent to replacing in all rules in Π each atom p ∈ U by ⊥ if p 6∈ X and by > if p ∈ X. In the previous example, the stable models of Π are {a} and {b}. For the first stable model X = {a}, we get eU (Π \ bU (Π), {a}) = {> → c} so that X ∪{c} = {a, c} should be a stable model for the complete program Π. Similarly, for X = {b} we get eU (Π \ bU (Π), {b}) = {> → d} and a “completed” stable model X ∪ {d} = {b, d}. The following result guarantees the correctness of this method in the general case. Theorem 2 (from [10]). Let U be a splitting set for a set of rules Π like (19). A set of atoms X is an stable model of Π if, and only if both – X ∩ U is a stable model of bU (Π) – X \ U is a stable model of eU (Π \ bU (Π), X ∩ U ).



In [10] this result was generalised for an infinite sequence of splitting sets, showing an example of a logic program with variables and a function symbol, so that the ground program was infinite. We adapt next this splitting sequence result for the case of splitable TLPs in TEL. From Definition 4 we can easily conclude that, when Π is a splitable TLP, its programs expansions have the form: Π 0 = ini0 (Π) Π i = ini0 (Π) ∪ ini1 (Π) ∪ dyn(Π)i

(for i > 0)

Proposition 2. Given a splitable TLP Π for signature At and any i ≥ 0: (i) Ati is a splitting set for Π ω ; (ii) and bAti (Π ω ) = Π i .



Given any rule like r like (20) of (21) and a set of atoms X, we define its simplification simp(r, X) as: 

B 0 ∧ N 0 → H 0 if B ⊆ X and N ∩ X = ∅ def simp(r, X) = > otherwise

Given some LTL interpretation T, let us define now the sequence of programs: def

Π[T, i] = eAti Π ω \ Π i , Ti




that is, Π[T, i] is the “simplification” of Π ω by replacing atoms in Ati by their truth value with respect to Ti . Then, we have: Proposition 3. Π[T, 0] = (dyn(Π)ω \ dyn(Π)1 ) ∪ {simp(r, T0 ) | r ∈ ini1 (Π) ∪ dyn(Π)} (28) and, for any, i ≥ 1 Π[T, i] = (dyn(Π)ω \ dyn(Π)i+1 ) ∪ { i simp(r, Ti ) | r ∈ dyn(Π)}

(29) 

As we can see, programs Π[T, i] maintain most part of dyn(Π)ω and only differ in simplified rules. Let us call these sets of simplified rules: def

slice(Π, T, 0) = Π 0 = ini0 (Π) def

slice(Π, T, 1) = {simp(r, T0 ) | r ∈ ini1 (Π) ∪ dyn(Π)} def

slice(Π, T, i + 1) = { i simp(r, Ti ) | r ∈ dyn(Π)}

for i ≥ 1

Theorem 3 (Splitting Sequence Theorem). Let hT, Ti be a model of a splitable TLP Π. hT, Ti is a temporal equilibrium model of Π iff (i) T0 = T0 is a stable model of slice(Π, T, 0) = Π 0 = ini0 (Π) and (ii) (T1 \ At0 ) is a stable model of slice(Π, T, 1) and (iii) (Ti \ Ati−1 ) is a stable model of slice(Π, T, i) for i ≥ 2.



As an example, let us take again program Π1 = (16), (22), (23), (18). The program Π10 = ini0 (Π1 ) = (22) has the stable model T0 = ∅ = T0 . Then we take slice(Π, T, 1) = {simp(r, T0 ) | r ∈ ini1 (Π) ∪ dyn(Π)} that corresponds to:

b → a

a → b

> → a

whose stable model is { a, b} = (T1 \ At0 ) so that T1 = {a, b}. In the next step, slice(Π, T, 2) = { simp(r, T1 ) | r ∈ dyn(Π)} =

2 a → 2 b

>

whose stable model is ∅ = (T2 \ At1 ) so that T2 = ∅. Then, we would go on with slice(Π, T, 3) = { 2 simp(r, T2 ) | r ∈ dyn(Π)} =

3 a → 3 b

> → 3 a

leading to { 3 a, 3 b} that is T3 = {a, b} and so on.

5

Loop formulas

Theorem 3 allows us building the temporal equilibrium models by considering an infinite sequence of finite ASP programs slice(Π, T, i). If we consider each program Π 0 = slice(Π, T, i + 1) for signature Ati+1 \ Ati then, since it is a standard disjunctive ASP program, we can use the main result in [12] to compute its stable models by obtaining the classical models of a theory Π 0 ∪LF (Π 0 ) where LF stands for loop formulas. To make the paper self-contained, we recall next some definitions and results from [12]. Given an ASP program Π we define its (positive) dependency graph G(Π) where its vertices are At (the atoms in Π) and its edges are E ⊆ At × At so that (p, p) ∈ E for any atom5 p, and (p, q) ∈ E if there is an ASP rule in Π like (19) with p ∈ H and q ∈ B. A nonempty set L of atoms is called a loop of a program Π if, for every pair p, q of atoms in L, there exists a path from p to q in G(Π) such that all vertices in the path belong to L. In other words, L is a loop of iff the subgraph of G(Π) induced by L is strongly connected. Notice that reflexivity of G(Π) implies that for any atom p, the singleton {p} is also a loop. Definition 7 (external support). Given an ASP program Π for signature At, the external support formula of a set of atoms Y ⊆ At with respect to Π, written ESΠ (Y ) is defined by:  _  ^ B∧N ∧ ¬p r∈R(Y )

p∈H\Y

where R(Y ) = {r ∈ Π like (19) | H ∩ Y 6= ∅ and B ∩ Y = ∅}.



Theorem 4 (from [12]). Given a program Π for signature At, and a (classical) model X W ⊆ At of Π then X is a stable model of Π iff for every loop Y of Π, X satisfies p∈Y p → ESΠ (Y )  If we apply this result to each si = slice(Π, T, i) we obtain an infinite sequence of classical theories. Fortunately, these theories have a repetitive pattern and can be captured by a single, finite LTL theory. Given a splitable TLP Π we will consider the dependency graph G(Π) generated from the expanded (ASP) program Π 2 , so that its nodes are atoms in the signature At2 = {p, p, 2 p | p ∈ At}. We define the concept of loop Y ⊆ At2 using this graph and signature. For instance, looking at G(Π1 ) in Figure 1 it is easy to see that loops for Π1 are { a, b} plus {A} for any A ∈ At2 . Theorem 5. Let Π be a splitable TLP and T an LTL model of Π. Then hT, Ti is a temporal equilibrium model of Π iff T is an LTL model of the union of 5

The original formulation in [12] did not consider reflexive edges, dealing instead with the idea of paths of length 0.

aO

a

b

b

U



2 a

O

2 b

Fig. 1. Graph G(Π1 ) (reflexive arcs are not displayed).

formulas LF (Y ) defined as: W p → ESini0 (Π) (Y ) Wp∈Y  p∈Y p → ESini1 (Π)∪dyn(Π)1 (Y )  W  p∈Y p → ESdyn(Π)2 \dyn(Π)2 (Y )

for any loop Y ⊆ At0 = At for any loop Y ⊆ (At1 \ At0 ) for any loop Y ⊆ (At2 \ At1 )



In our running example Π1 we have At0 = {a, b} and ini0 (Π) = (22) with two loops {a}, {b} where LF ({a}) = (a → ⊥) and LF ({b}) = (b → a). For (At1 \ At0 ) = { a, b} we take the program ini1 (Π1 ) ∪ dyn(Π)1 ), that is, rules (16), (23), (18) ignoring . We get three loops leading to the corresponding loop formulas ( a → (¬a ∧ b) ∨ ¬b), ( b → a) and ( a ∨ b → ¬b). Finally, for At2 \ At1 we have two loop formulas ( 2 b → 2 a) and ( 2 a → ¬ b). It is not difficult to see that Π1 ∪ LF (Π1 ) is equivalent to the LTL theory: ¬a ∧ ¬b ∧ ( a ↔ ¬b) ∧ ( b ↔ ¬b).

6

Conclusions

We have presented a class of temporal logic programs (that is ASP programs with temporal operators) for which their temporal equilibrium models (the analogous to stable models) can be computed by translation to LTL. To this aim, we have combined two well-known techniques in the ASP literature called splitting and loop formulas. This syntactic class has as restriction so that rule heads never refer to a temporally previous situation than those referred in the body. Still, it is expressive enough to cover most ASP examples dealing with dynamic scenarios. We have implemented a system, called STeLP that uses this technique to translate a program and calls an LTL model checker to obtain its temporal equilibrium models, in the form of a B¨ uchi automaton. This tool allows some practical features like dealing with variables or specifying fluents and actions6 .

References 1. Niemel¨ a, I.: Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25 (1999) 241–273 6

More examples and information can be obtained in http://www.dc.fi.udc.es/~cabalar/stelp.pdf

2. Marek, V., Truszczy´ nski, M. In: Stable models and an alternative logic programming paradigm. Springer-Verlag (1999) 169–181 3. Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In Kowalski, R.A., Bowen, K.A., eds.: Logic Programming: Proc. of the Fifth International Conference and Symposium (Volume 2). MIT Press, Cambridge, MA (1988) 1070–1080 4. Cabalar, P., Vega, G.P.: Temporal equilibrium logic: a first approach. In: Proc. of the 11th International Conference on Computer Aided Systems Theory, (EUROCAST’07). LNCS (4739). (2007) 241–248 5. Pearce, D.: A new logical characterisation of stable models and answer sets. In: Non monotonic extensions of logic programming. Proc. NMELP’96. (LNAI 1216). Springer-Verlag (1996) 6. Pearce, D.: Equilibrium logic. Annals of Mathematics and Artificial Intelligence 47(1-2) (2006) 3–41 7. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag (1991) 8. Aguado, F., Cabalar, P., P´erez, G., Vidal, C.: Strongly equivalent temporal logic programs. In: Proc. of the 11th European Conference on Logics in Artificial Intelligence (JELIA’08). LNCS (vol. 5293). (2008) 8–20 9. Cabalar, P.: A normal form for linear temporal equilibrium logic. In: Proc. of the 12th European Conference on Logics in Artificial Intelligence (JELIA’10). Lecture Notes in Computer Science. Volume 2258. Springer-Verlag (2010) 64–76 10. Lifschitz, V., Turner, H.: Splitting a logic program. In: Proceedings of the 11th International Conference on Logic programming (ICLP’94). (1994) 23–37 11. Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. In: Artificial Intelligence. (2002) 112–117 12. Ferraris, P., Lee, J., Lifschitz, V.: A generalization of the Lin-Zhao theorem. Annals of Mathematics and Artificial Intelligence 47 (2006) 79–101 13. Heyting, A.: Die formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasse (1930) 42–56 14. Ferraris, P.: Answer sets for propositional theories. In: Proc. of the 8th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’05). LNCS (vol. 3662). (2005) 119–131 15. Fages, F.: Consistency of Clark’s completion and existence of stable models. Methods of Logic in Computer Science 1 (1994) 51–60

Appendix. Proofs Lemma 1. Let r be an initial rule like (15), and M a THT interpretation. Then (M, i) |= r iff Mω |= i r. Proof. It directly follows from construction of Mω and simple inspection of the THT satisfaction relation.  Lemma 2. Let Π be a TLP without fulfillment rules. Then hH, Ti |= Π in THT iff hHω , Tω i |= Π ω in HT. Proof. We prove that for any rule r in Π, M = hH, Ti |= r iff Mω = hHω , Tω i |= rω . We have two cases: 1. Let r be an initial rule r. The condition M |= r can be expressed as (M, 0) |= r and, from Lemma 1, this is equivalent to Mω |= 0 r that is Mω |= r. 2. Let r be a dynamic rule r = s. The condition M |= s is equivalent to: ∀i ≥ 0, (M, i) |= s. From Lemma 1, this is equivalent to ∀i ≥ 0, Mω |= i s, that is, Mω |= (s)ω .  Proof of Theorem 1.. For the left to right direction, suppose hT, Ti is a temporal equilibrium model of Π. This implies hT, Ti |= Π and, by Lemma 2, we get hTω , Tω i |= Π ∗ . Assume Tω is not a stable model of Π ω . This means that hTω , Tω i is not an equilibrium model of that program, that is, there exists some smaller Hω ⊂ Tω such that hHω , Tω i |= Π ω . But by Lemma 2 again we would have hH, Ti |= Π and as H < T (since Hω ⊂ Tω ) we conclude that hT, Ti cannot be a temporal equilibrium model of Π, reaching a contradiction. For the right to left direction, take any stable model Tω of Π ω . Since Tω |= ω Π or equivalently hTω , Tω i |= Π ω in HT, from Lemma 2, we get hT, Ti |= Π. Suppose that for some H ⊂ T, hH, Ti |= Π. By Lemma 2 we obtain hHω , Tω i |= Π ω and as Hω ⊂ Tω (since H ⊂ T) we obtain that hTω , Tω i cannot be an equilibrium model for Π ω , reaching a contradiction.  Proof of Proposition 2. (i) If a rule in Π ω has some head atom in Ati it will have the form j p for some 0 ≤ j ≤ i. By construction, in any of the three rule types (19),(20),(21) the whole head will consist of (expanded) atoms of the form

j q whereas the body may contain atoms of the form j q or j−1 q. All these expanded atoms have a sequence of ’s of length smaller than or equal to i, so they also belong to Ati . (ii) By Definition 4 the longest sequence of ’s occurring in any ri (and so, in Π i ) will have length i. This implies that Π i ⊆ bAti (Π ω ). To prove the opposite bAti (Π ω ) ⊆ Π i suppose we had r ∈ bAti (Π ω ) but r 6∈ Π i . Since bAti (Π ω ) ⊆ Π ω , we get r ∈ Π ω \ Π i . Then, for some j > i, r ∈ Π j \ Π i . Let us take the smallest j satisfying this. Then, r ∈ Π j but r 6∈ Π j−1 . But then, by construction of the program expansion, r must contain some atom of the form j p. Finally, as j > i, j p 6∈ Ati and so r 6∈ bAti (Π ω ) reaching a contradiction. 

Proof of Proposition 3. First note that Π ω
\ Π 0 = ini1 (Π) ∪ dyn(Π)ω . We obtain (28) by calculating eAt0 Π ω \ Π 0 , T0 , since T0 = T0 . Now take i ≥ 1 and suppose that (29) is true. Then
Π[T, i + 1] = eAti+1 Π ω \ Π i+1 , Ti+1 [
= (Π ω \ Π i+2 ) eAti+1 Π i+2 \ Π i+1 , Ti+1 and since i + 2 > 1 this is the same than: [
=(dyn(Π)ω \ dyn(Π)i+2 ) eAti+1 Π i+2 \ Π i+1 , Ti+1 =(dyn(Π)ω \ dyn(Π)i+1 ) [ { i+2 B 0 ∧ i+2 N 0 → i+2 H 0 | rule like (21) ∈ dyn(Π) and B ⊆ Ti+1 , N ∩ Ti+1 = ∅}  Proof of Theorem 3. Using Theorem 1, we have to prove that Tω is a stable model of Π ω iff the two above conditions are satisfied. As At0 is a splitting set of Π ω , Tω is an stable model of P ω iff – Tω ∩ At0 = T0 is a stable model of bAt0 (Π ω ) = Π 0 , which is (i), plus – Tω \ At0 is a stable model of eAt0 (Π ω \ Π 0 , T0 ) = Π[T, 0]. Since, At1 is again a splitting set of Π[T, 0], the last condition is equivalent to: – (Tω \ At0 ) ∩ At1 = (T1 \ At0 ) is a stable model of bAt1 (Π[T, 0]) that corresponds to {simp(r, T0 ) | r ∈ ini1 (Π) ∪ dyn(Π)}, so this is (ii), – and (Tω \ At0 ) \ At1 = (Tω \ At1 ) is a stable model of eAt1 (Π ω \ Π 1 , T1 ) = Π[T, 1]. As At2 is a splitting set for Π[T, 1] we can apply a similar reasoning to conclude that the last item above is equivalent to: – (Tω \ At1 ) ∩ At2 = (T2 \ At1 ) is a stable model of bAt2 (Π[T, 1]) that corresponds to { simp(r, T1 ) | r ∈ dyn(Π)}, so this is (iii) with i = 2, the base case, – and (Tω \ At1 ) \ At2 = (Tω \ At2 ) is a stable model of eAt2 (Π ω \ Π 2 , T2 ) = Π[T, 2]. and the induction step for (iii) follows by replacing in the two conditions above 1, 2 respectively by i and i + 1.  Proof of Theorem 5. For a proof sketch, notice that there cannot be loops between two different situations since this would require that some past situation depended on the future. So, each loop is always inside some slice(Π, T, i) and all atoms for Ati−1 are external to the loop. Since the first two slices are affected by initial rules, they are specified in a separate case, whereas from slice 2 on we get a repetitive pattern using .