On Temporal ASP with Eager Unfoldable Operators

1 Introduction

Answer Set Programming (ASP) [Brewka et al., 2011; Lifschitz, 2019] has been widely applied in dynamic environments, including applications in planning, multi-agent systems, and reasoning about evolving domains [Falkner et al., 2018]. ASP semantics is particularly well-suited for such settings due to its capability of expressing transitive closure, addressing the frame problem (via inertia rules), and providing both default and strong negation, which enables rich and flexible modeling possibilities. Temporal Equilibrium Logic (TEL) [Aguado et al., 2023] builds on this foundation by bridging the gap between the expressive power of linear-time temporal logic (LTL) [Pnueli, 1977] operators and the stable semantics of ASP. By integrating these paradigms, TEL provides a unified framework for reasoning about dynamic systems while preserving the non-monotonic reasoning capabilities and desirable properties of ASP.

A key distinction of TEL compared to LTL lies in its capability to address (i) non-determinism by naturally encoding various assumptions about unseen data, (ii) the inertia law, which allows for reasoning about persistence of facts over time, and (iii) dependencies, expressed in a rule-based manner, that are fundamental to many temporal systems.

Example 1 (Liveness property). A user may issue a "request" for a resource in a system that must be granted at some future point in time. The rules governing this system dictate that a "grant" action g can only occur if a corresponding "request" r has been made in a prior step, in formulas □(r → ♢g). Classical LTL semantics cannot fully capture this dependency, i.e., a grant g can appear even without a request r. To model it in LTL, one must also include □(g → ⧫r), ensuring that every grant g occurs due to a request r. However, this creates a cascading problem: if requests r themselves must be justified by other temporal rules, complicating the modeling, cf. frame problem as discussed in [McCarthy and Hayes, 1981].

While TEL effectively captures these temporal dependencies, its strong minimization condition often leads to unintended consequences. Specifically, if a request is derived infinitely often by a formula such as □♢r, no infinite equilibriummodel exists: after removing the first r from a model, we still have a model, which leads to an infinite chain of smaller models that compromises stability. For eventual persistence conditions such as ♢□p, the situation is similar.

To address this issue, we introduce a novel version of the until, release, since, and trigger operators, termed eager operators. These operators temper the strong minimization by suspending it until the operator is fulfilled along the trace. This yields new versions of derived operators, such as eventually and once, which align better with intuitive reading.

The proposed suspension ensures that in Example 1, we have infinite stable models of infinite length. For finitary semantics, the standard definition of eventually would in Example 1 place a grant g only in the very last state, from which it cannot be removed. However, such behavior does arguably not align with the intuitive reading of the formulas in Example 1. Therefore, even in the case of finite traces, we consider the eager version of the temporal operator a preferable choice to accurately capture the intended behavior.

Example 2 (Safety property). For another scenario where dependencies matter, assume there are admin users and regular user. Admin users can promote a regular user to be an admin while regular users can't. Thus, a schematic rule such as □(admin(X), promotes(X, Y ), user(Y ) → admin(Y )), where X and Y are placeholders for the grounded version of the formula, should not self-support the predicate admin.

Our main contributions are summarized as follows.

• We introduce new versions of the temporal operators that unfold eagerly. While they are indifferent in LTL, they suspend minimization and thus allow for stable models in scenarios where such models are intuitively expected. Notably, the new versions are expressible in TEL and the resulting extension of TEL has the same complexity, i.e., TEL-satisfiability is EXPSPACE-complete [Bozzelli and Pearce, 2015].
• We define NDTP as a rule-based fragment of the new language that, on the one hand, overcomes the problem of strong minimization and, on the other hand, has considerably lower complexity. The former is achieved by using eager temporal operators in rule heads and the latter by disallowing disjunction, which quickly leads to EXPSPACE-hardness [ˇSimkus, 2010]. We show that NDTP programs have benign properties and that deciding TEL-satisfiability for them is in EXPTIME in general, while model checking is feasible in polynomial time.
• Based on NDTP, we define a tight version of temporal programs (TTP). By generalizing results for ordinary tight logic programs [Erdem and Lifschitz, 2003], we show that the stable models of TTP programs are obtained as the LTLmodels of their temporal Clark's completion that we define. As a result, we obtain a polynomial encoding of TTP into LTL. Furthermore, we show that the tightness of temporal programs can be decided efficiently in NL, resorting to onecounter automata.

The use of NDTP as a starting point can be seen as a temporal extension of normal programs (or non-disjunctive programs as in [Erdem and Lifschitz, 2003]), which is the standard fragment on top of which the notion of tightness is usually defined [Dodaro et al., 2023; Lin and Zhao, 2003]. However, this approach has not yet been extended to ASP with modalities, which are highly useful logical operators for various domains. Our results enable bridging temporal nonmonotonicity with LTL-based model checkers such as SPIN [Holzmann, 1997], nuXmv [Cavada et al., 2014], and BLACK [Geatti et al., 2021].

Organization. The remainder of this paper is organized as follows. Section 2 provides a formal background on TEL. Section 3 introduces the new operators and shows their practical applicability. Section 4 introduces the NDTP fragment, while Section 5 presents tight temporal programs. In Section 6, we discuss related work and conclude.

2 Preliminaries

Both TEL and THT [Aguado et al., 2023] share the same syntax as LTL. Here we introduce the grammar

where p ∈ P for a finite set P of propositional atoms, △ ∈ {∧, ∨,→}, and O ∈ {U,R, S,T}. Negation is defined as ¬ϕ ∶= ϕ → bot. As usual, □ (globally) is defined by □ϕ ∶= botRϕ; ♢ (eventually) by ♢ϕ ∶= ⊺Uϕ; ∎ (historically) by ∎ϕ ∶= botTϕ; ⧫ (once) by ⧫ϕ ∶= ⊺Sϕ; ˆ○ (weak next) by ˆ○ϕ ∶= ○ϕ ∨ ¬○⊺;

and ˆ● (weak previous) by ˆ●ϕ ∶= ●ϕ ∨ ¬●⊺. Furthermore, for any unary operator u, we let ×0ϕ denote ϕ and ×i+1ϕ denote uuiϕ, for i ≥ 0.

The semantics of THT is defined via THT-traces (or simply traces, if clear from context), which are finite or infinite sequences ⟨H,T⟩ of pairs ⟨Hi,Ti⟩, where Hi ⊆ Ti ⊆ P for each 0 ≤ i < λ, where λ can be either in N or ω. Both H and T are traces as usual (LTL-traces), i.e., sequences H = H0,H1, . . . resp. T = T0, T1, . . . of sets of atoms. Given a THT-trace I (or an LTL-trace T), we denote its length by λI (resp. λT).

Definition 1 (THT-Satisfaction). Satisfaction of a THT formula by a THT-trace I = ⟨H,T⟩ at time k, where 0 ≤ k is integer, is inductively defined as follows:

1. I, k /⊧ bot and I, k /⊧ ⊺
2. I, k ⊧ p if p ∈ Hk, for any atom p ∈ P
3. I, k ⊧ ϕ∨ψ if I, k ⊧ ϕ or I, k ⊧ ψ
4. I, k ⊧ ϕ∧ψ if I, k ⊧ ϕ and I, k ⊧ ψ
5. I, k ⊧ ϕ→ψ if {⟨T,T⟩, k /⊧ ϕ or ⟨T,T⟩, k ⊧ ψ, and I, k /⊧ ϕ or I, k ⊧ ψ
6. I, k ⊧ ○ ϕ if k + 1 < λI and I, k + 1 ⊧ ϕ
7. I, k ⊧ ϕ U ψ if there is j ≥ k s.t. I, j ⊧ ψ, and for all j ′ ∈ [k, j), I, j ′ ⊧ ϕ
8. I, k ⊧ ϕ R ψ if for all j ≥ k s.t. I, j /⊧ ψ, there exists j ′ ∈ [k, j), I, j ′ ⊧ ϕ
9. I, k ⊧ ● ϕ if k > 0 and I, k - 1 ⊧ ϕ
10. I, k ⊧ ϕ S ψ if there is j ≤ k s.t. I, j ⊧ ψ, and for all j ′ ∈ (j, k), I, j ′ ⊧ ϕ
11. I, k ⊧ ϕ T ψ if for all j ≥ k s.t. I, j /⊧ ψ, there exists j ′ ∈ [k, j), I, j ′ ⊧ ϕ,

We recall that the persistence property holds for THT, i.e., that if a proposition is true in a here state Hi, it remains true in Ti, reflecting the notion that truth is preserved.

Proposition 1 (Persistence, [Aguado et al., 2023]). For any formula ϕ and THT -trace I = ⟨H, T⟩, I ⊧ ϕ implies T ⊧ ϕ.

As a consequence, interpreting the negation ¬ϕ in ⟨H,T⟩ at time point i amounts to ϕ not holding in T at i. Formally, Corollary 1. For any formula ϕ and THT-trace I = ⟨H,T⟩,

I ⊧ ¬ϕ iff T /⊧ ϕ.

Furthermore, LTL and THT are strongly related, as ⟨T,T⟩ ⊧ ϕ iff T ⊧ ϕ under LTL semantics, which is easily verified by comparing the respective satisfaction conditions.

We are now ready to introduce the semantics of TEL[Aguado et al., 2023].

Definition 2 (Stable (Equilibrium, TEL) Model). A trace T is a stable (equilibrium, TEL) model of formula ϕ if (i) T ⊧ ϕ, i.e., T is an LTL model of ϕ, and (ii) no H ≠ T exists s.t. ⟨H, T⟩ ⊧ ϕ.

Example 3. For a predicate admin(X) varying over time and its negation n admin(X), inertia default rules are as follows:

• □(n admin(X) ∧¬○admin(X) → ○n admin(X)) (3)

(2) states that, in any situation where admin(X) holds and there is no evidence that in the next state n admin(X) holds, then admin(X) remains true; (3) is analogous for n admin(X). The conjunction of (2), (3), and the formula ○○admin(X) ∧ ○○♢n admin(X) grounded to X = u1 has the stable models given by the regular expression ∅ ⋅ ∅ ⋅ {admin(u1)}+ ⋅ {n admin(u1)} ⋅ {n admin(u1)}λ , where λ ranges over N∪ {ω}, i.e., induces finite and infinite traces.

3 Eager Unfoldable Operators

Even though TEL effectively captures the intended meaning of scenarios like Example 2, where local positive loops are considered, it struggles to fully capture the intended semantics of Example 1. Consider the following formula:

This formula does not admit any infinite stable model. Intuitively, given a candidate LTL model T, it is always possible to construct a smaller H such that ⟨H,T⟩ ⊧ φ by omitting g in Hi for some arbitrary time point i, even if g occurs in Ti. This minimization condition undermines the satisfaction of the formula's intended meaning. The issue persists in the finite case, where the unique stable model involves finitely many occurrences of r, with g appearing only in the last state. Under TEL, any finite LTL model where g appears earlier in the trace is unstable, as we can remove it fromH.

A similar argument applies to the sub-formula □(♢r) by itself. As r must occur infinitely often, we can always remove an occurrence of r from H and still have THT-satisfaction. This highlights a fundamental limitation of TEL's strong minimization criterion in scenarios like Example 1.

The operators ♢ and U are non-deterministic in Definition 1, as their satisfaction depends on arbitrary points in the trace, akin to temporal disjunction. In contrast, □ and ○ are deterministic, and evaluated directly at specific points. To address this, we propose eager variants of Ue, Re, Se, and Te, which unfold deterministically once a T-trace is fixed. These operators are equivalent to the standard ones in LTL but weaker in THT, resolving non-determinism for clearer computational and modeling benefits.

Definition 3. The eager variant Oe of the operator O ∈ {U,R, S,T} is as follows. For any THT-trace I = ⟨H,T⟩ and time point k ≥ 0,

1. I, k ⊧ ϕ Ue ψ if there exists some j ≥ k s.t. I, j ⊧ ψ, and for all j ′ ∈ [k, j), I, j ′ ⊧ ϕ and T, j ′ /⊧ ψ;
2. I, k ⊧ ϕ Re ψ if for all j ≥ k s.t. (a) I, j /⊧ ψ or (b) T, j ⊧ ϕ andI, j /⊧ ϕ, some j ′ ∈ [k, j) exists s.t. I, j ′ ⊧ ϕ;
3. I, k ⊧ ϕ Se ψ if there is some j ≤ k s.t. I, j ⊧ ψ, and for all j ′ ∈ (j, k), I, j ′ ⊧ ϕ and T, j ′ /⊧ ψ;
4. I, k ⊧ ϕ Te ψ if for all j ≥ k s.t. (a) I, j /⊧ ψ or (b) T, j ⊧ ψ and I, j /⊧ ψ, some j ′ ∈ [k, j) exists s.t. I, j ′ ⊧ ϕ.

From these new operators, we can derive as usual operators such as: □e (eager globally) by □eϕ ∶= bot Re ϕ; ♢e (eager eventually) by ♢eϕ ∶= ⊺ Ue ϕ; ∎e (eager historically) by ∎eϕ ∶= bot Te ϕ; etc.

The notion of stable model in Definition 2 naturally extends to the new operators. In Example 1, we mentioned that one might be interested in expressing the following properties: (i) every request must eventually be satisfied with a grant, and (ii) a grant is given only if there was a prior request. In other words, intuitively, point (ii) requires a justification for every grant.

With the novel temporal operators, We can effectively capture points (i) and (ii) under stable semantics.

This formula yields infinitely many infinite models, where all occurrences of g along the trace following a request are considered stable. Intuitively, the new operators can be interpreted as suspending the minimization for a stable (Definition 2), introducing a temporal instance of the excluded middle axiom, which is propagated until the temporal formula is fulfilled. Note that if ⟨H,T⟩, i ⊧ p∨¬p, then p ∈ Hi iff p ∈ Ti.

From Corollary 1 we obtain that the new operators are expressible in THT.

Lemma 1. In THT,

Notably, □e coincides with □ and ∎e with ∎. According to Theorem 1 in [Cabalar and Di´eguez, 2014], THT-equivalent formulas ϕ and ψ are strongly equivalent in TEL, i.e., replacing any occurrence of ϕ in a formula χ with ψ, or vice versa, results in the same stable models for χ. Consequently, the formula τe(ϕ) that results from a formula ϕ by exhaustive application of Lemma 1 has the same stable models as ϕ.

We then obtain the following result.

Theorem 1. Deciding TEL-satisfiabilty of a formula ϕ in which eager operators occur is EXPSPACE-complete.

The membership part follows from EXPSPACEcompleteness of TEL-satisfiability and the fact that τe(ϕ) and ϕ have the same stable models; an exponential blowup can be avoided using Tseitin-style [Tseitin, 1983] naming of subformulas ψ, i.e., using atoms pψ and adding pψ ↔ ψ. The EXPSPACE-hardness follows from the fragment with arbitrary nesting of □ and implication [Bozzelli and Pearce, 2015] as well as from the fragment with □ and ○ [ˇSimkus, 2010].

4 Non Disjunctive Temporal Programs

In this section, we introduce NDTP programs, a nondisjunctive, rule-based fragment extending the class considered in [Erdem and Lifschitz, 2003] to the temporal case by incorporating TEL modalities in the body and allowing arbitrary nesting of eager unfoldable operators in the head.

Definition 4 (NDTP). A Non-Disjunctive Temporal Program π consists of

• (i) a set init(π) of initial rules of the form

where ϕ is either bot or a head formula from the grammar

where p ∈ P and γ is an arbitrary TEL formula, η[⋅] is parameterized by a grammar symbol (ϕ, ψ1 or ψ2), and

(ii) a set dyn(π) of dynamic rules of the form □r, where r is an initial rule.

For each rule r we denote ψ as body(r) and ϕ as head(r).

The NDTP fragment disallows: (i) nesting of implications outside the scope of a negation, (ii) negation within temporal unfoldable operators, and (iii) disjunctions in the head. It permits (i) eager operators in the head, and (ii) arbitrary formulas under negation. Notably, all examples from above are in this fragment.

The eager operators unfold deterministically along a given trace due to the restricted temporal disjunctions, making them conceptually similar to "shiftable" operators. This deterministic behavior ensures a clear justification for atoms appearing along a trace T, while the body admits richer syntax under the condition that the negated sub-formulas can be evaluated and replaced with ⊺ or bot without the need for further unfolding beyond the one for the dynamic rules.

As for properties of NDTP, a notable one is that eager operators in rule heads do not eliminate stable models.

Proposition 2 (Equilibrium Persistence). Given an NDTP program π, let π′ be a formula obtained from π by replacing some eager operators Oe with O. Then every stable model of π′ is a stable model of π.

Furthermore, as for ordinary logic programs, negation is necessary to prevent stability. Let us call ¬-free NDTP programs positive. Then

Theorem 2 (Positive NDTP). Every positive NDTP program π that is LTL-satisfiable has a stable model.

In particular, if π in Theorem 2 has no heads bot it has some stable model. For example, recall that □♢er has infinitely many stable models, while its counterpart □♢r has none.

Next, we observe that using a Tseitin-style transformation with auxiliary atoms as mentioned above, it is possible to obtain a normal form for head formulas.

Proposition 3 (Head Normal Form). Every NDTP program π is rewritable in polynomial time to an NDTP program π′ that has the same stable models as π modulo auxiliary atoms where π′ has only head formulas of the form p, ○p, and bot.

This result is particularly useful for simplifying inference and deriving complexity results.

We next present a characterization of stable models in terms of a program reduct.

Definition 5 (λ-Unfolding). For any NDTP program π and λ ≥ 1, the temporal program πλ is πλ ∶= init(π)∪{○i r ∣ □r ∈ πdyn, i ∈ [0, λ)}.

It is easy to see that πλ and π share the same LTL, THT and TEL models, for any NDTP program π and λ ≥ 1, and that □r holds iff r holds in every state i ∈ [0,λ) according to Defn. 1. We can now introduce temporal program reducts. Denote by sub¬(ϕ) the maximal subformulas of ϕ of the form ¬ψ, i.e., not within the scope of another negation.

Definition 6 (Temporal reduct). The temporal reduct πT of an NDTP program π w.r.t. an LTL trace T results from πλ by (1) replacing every ○i r ∈ πλ with τe(○i r); (2) unfolding temporal operators if they are finitely fulfilled; (3) if R (or T) unfolds infinitely, replace it with □ (resp. ∎); (4) replace each ψ ∈ sub¬(○i r) with ⊺ if T, i ⊧ ψ, and with bot otherwise.

We note that the temporal reduct is well-defined as negation is not allowed inside unfoldable temporal operators such as U, R, S, T, or their derived operators. The deterministic nature of rule heads in NDTP programs is formally evidenced by the fact that they admit a single minimal Here-Trace. Such a result can be shown by defining a fixed-point operator over a lattice of H-traces using the unfolded reduct πT as rules.

Proposition 4. Let π be an NDTP program and T an LTL model of π. Then there exists an H such that H ≤ H′ whenever ⟨H′ ,T⟩ ⊧ πT.

We call T a λ-stable model of π if T is an LTL-minimal model of πT (equivalently, T coincides with H in Proposition 4). We link the equilibrium-based (Defn. 2) and reductbased (Defn. 6) stable models, showing that they coincide.

Proposition 5 (Equivalence). A trace T is a stable model of an NDTP program π iff T is a λ-stable model of πT.

Regarding the form of stable models, any TEL-satisfiable formula ϕ that has an infinite stable model has one of the form T = TP ⋅TωC , where the length of TP ⋅TC is at most doubleexponential in the size of ϕ [Bozzelli and Pearce, 2015]. In the case of NDTP programs, this falls back to a single exponential length, and a finite stable model (if any) of exponential length exists. Details are given in the appendix.

Turning to complexity, it is well known that modelchecking of an LTL formula ϕ on a trace T is feasible in polynomial time [Demri and Schnoebelen, 2002]. This similarly holds for stable model checking of NDTP programs.

Theorem 3. Given an NDTP program π and a (finitely represented) trace T, deciding whether T is a stable model of π is feasible in polynomial time.

As for deciding TEL-satisfiability of NDTP programs, we have the following result.

Theorem 4. Deciding whether an NDTP program π is TEL-satisfiable is in EXPTIME.

Proof. (Sketch) The proof proceeds by encoding the program π into a B¨uchi automata using well-established LTL-toautomata techniques. To address the two-world semantics of THT, we employ the star-translation, which maps the twoworld structure into single-world representation by introducing fresh atoms for the Here-world formulas.

The automata construction involves two components: the (i) HT-local automata, which enforces local consistency for the There-world, and closure for head and body formulas for the Here-world. So if p, q are in the Here part of a node, and p ∧ q appears as a sub-formula in π, then we want also p ∧ w in the Here part of a node; the (ii) T-eventuality automata, which imposes fairness conditions, requiring that if an U formula is derived infinitely often, it must also be fulfilled infinitely often. We compute the synchronous product of these two automata.

The minimality of the H-trace is achieved via a fix-point computation. Starting with a list of nodes where nothing positive is derived in the Here-part, we iteratively apply the immediate consequence operator, propagating head formulas through the list of nodes once derived. Once a set of head formulas is derived, we update the list of nodes with new nodes with the minimal set of formulas in the Here part such that they contain the derived formulas. Identifying such nodes is deterministic due to the syntactic restrictions of NDTP programs.

Consequently, NDTP programs have, besides appealing semantic properties, significantly lower complexity than the full language of TEL. A matching lower bound is open, while PSPACE-membership of the problem is plausible.

5 Tight Temporal Programs

In this section, we introduce tight temporal programs (TTP), a fragment of TEL designed to keep complexity low by relying on LTL solvers. In ASP, the notion of tightness - programs without positive recursive dependencies - ensures that stable models can be obtained as supported models via Clark's completion. We establish similar results for NDTP programs, despite the challenges of defining support when (nested) temporal operators are allowed.

We start by defining the concept of support for head formulas, which will serve as the foundation for introducing support in NDTP programs.

Definition 7 (Supporting Head). Given a head formula φ, a trace T, and i, j ∈ [0, λT), we say that p ∈ Ti is supported by φ at time j, denoted suppT(φ, j, p, i), if T, j ⊧ φ and

• φ = p: i = j and i < λT;
• φ = φ1 ∧ φ2: supp(φk, j, p, i) for some k ∈ {1, 2};
• φ = φ1Ueφ2: if T, j ⊧ φ2 then suppT(φ2, j, p, i) else either suppT(φ1, j, p, i) or suppT(φ, j + 1, p, i);
• φ = φ1Reφ2: if T, j ⊧ φ1 then either suppT(φ1, j, p, i) or suppT(φ2, j, p, i), else either suppT(φ2, j, p, i) or suppT(φ, j + 1, p, i);
• φ = φ1Seφ2: if T, j ⊧ φ2 then suppT(φ2, j, p, i) else either suppT(φ1, j, p, i) or (b2) suppT(φ, j + 1, p, i);
• φ = φ1Teφ2: if T, j ⊧ φ1 then either suppT(φ1, j, p, i) or suppT(φ2, j, p, i) else either suppT(φ2, j, p, i) or suppT(φ, j - 1, p, i);
• φ = ○φ1 or φ = ˆ○φ1: suppT(φ1, j + 1, p, i);
• φ = ●φ1 or φ = ˆ●φ1: suppT(φ1, j - 1, p, i).

Note that Definition 7 is more straightforward in the atemporal case unless one wants to cover also boolean operators in the head, see e.g. [Alviano et al., 2016].

Definition 8 (Supported LTL Models). Trace T is supported by an NDTP π, if for every j ∈ [0,λT) and p ∈ Tj, either some (a) □r ∈ dyn(π) or (b) r ∈ init(π) exists s.t T, i ⊧ body(r) and suppT(head(r), i, p, j), where i = 0 in case (b).

We notice that the stable models of the theory in Example 3 coincide with its supported models. More in general, as for the relationship to LTL- and TEL semantics, we show that supported LTL models relax TEL-models.

Proposition 6. Every stable model T of an NDTP program π is a supported LTL model of π.

Furthermore, the supported LTL-models can be expressed in LTL. To this end, we introduce a temporal version tcc of Clark's completion [Clark, 1977] such that T is a supported model of π iff T is an LTL model of tcc(π).

Definition 9 (Temporal Clark's Completion). For any NDTP π, its temporal completion is

where γ(p) ∶= p → ⋁r∈π justify pr (head(r), body(r)) and justify pr (ϕ,ψ) is inductively defined as follows:

• ϕ = p: if r ∈ init(π) then ¬●⊺∧ψ else ψ;
• ϕ = q ≠ p, ϕ = ⊺, or ϕ = bot: bot;
• ϕ = ϕ1 ∧ϕ2: justify pr (ϕ1,ψ) ∨ justify pr (ϕ2,ψ);
• ϕ = ϕ1 Oe ϕ2, for O ∈ {U,R, S,T}: γO,1 ∨ γO,2, where

γR,1 = justify pr (ϕ1, ϕ1 ∧ (ψ ∨ ●(¬ϕ1 S (¬ϕ1 ∧ ψ)))),

• ϕ = ○ϕ1, ϕ = ˆ○ϕ1: ●justify pr (ϕ1,ψ),
• ϕ = ●ϕ1, ϕ = ˆ●ϕ1: ○justify pr (ϕ1,ψ).

Temporal operators like Ue, Se, ○ introduce dependencies between states, meaning that the support for an atom might need to be propagated among states.

Example 4. Consider the NDTP π with two dynamic rules □(r1) and □(r2), where r1 = ○p → p and r2 = □(○⊺), and no initial rules. As easily seen, □(r2) enforces infinite models; we are thus in the infinitary (standard) setting of LTL. Applying the temporal Clark's completion, we obtain γ(p) = p → ○p ∨ bot. Thus tcc(π) = π ∪ {□(p → ○p ∨ bot)}, which has the LTL models T = {p}ω and H = ∅ω .

In Example 4, T is supported by π but not a TEL-model of π (as ⟨H,T⟩ ⊧ π). However, without r2, finite models of tcc(π) would coincide with stable models. In general, we have:

Proposition 7 (Characterization). For any NDTP program π and an LTL model of π, T ⊧ tcc(π) iff T is a supported LTL model of π.

On the other hand, the LTL semantics of a program π is easily recovered from the supported LTL models of an augmented program, by adding □(p → p) for each p ∈ P to π.

We remark that the completion formula tcc(π) can be exponential in the nesting depth of operators Oe in rule heads. For a polynomial LTL encoding, we can introduce Tseitinstyle naming of subformulas as described above.

We next introduce notions of parents and relevance.

Definition 10. For the unfolded program πT of an NDTP program π and a trace T, an atom pi is a parent of qj if some rule ○k r exists s.t. T, i ⊧ body(r), suppT(head(r), k, q, j) and pi is relevant for body(r) w.r.t. T. We call pi relevant for body(r) w.r.t. T when in checking recursively T, k ⊧ body(r) (w.r.t. Defn. 1) we may end up evaluating T, i ⊧ p.

Note that given a head formula ϕ, (p, i) ∈ suppT(ϕ, j) iff pi is relevant for ϕ w.r.t. T.

In the following definition, we use the "being parent" relation over atoms. We assume that there is an order over the atoms in P, and we use the subscript k in pik to refer to the k-th atom in P at time point i.

Definition 11. An NDTP program π is tight on T, if there are no infinite sequences pi0 j0 , pi1 j1 , . . . such that for each k ≥ 1, pik jk is a parent of pik-1 jk-1 .

We recall and accommodate Proposition 3 from [Erdem and Lifschitz, 2003] to our terminology:

Proposition 8. A program π is tight on a trace T iff there exists a function f from P × [0,λT) to ordinals such that for every rule ○i in πT with T, i ⊧ body(r) ∧ head(r), for every (p, i) ∈ suppT(head(r), j), and for every qk relevant for body(r) w.r.t T, we have f(p, j) < f(q, k).

Based on this, we can then show:

Theorem 5. For any NDTP program π and any LTL model of π tight on T, T is an stable trace for π iff T is supported by π iff T ⊧ π ∧ tcc(π).

We proceed to a variant of Theorem 5 that is not parameterized by an LTL model T, but works for all possible traces. To achieve this goal, we need a notion of dependence among atoms that does not rely on a specific trace.

The dependency graph is an important tool in logic programming and is the basis of many relevant results, among them the semantic properties of tight logic programs. For our concerns, the dependency graph is defined as follows.

Definition 12 (Dependency Graph). Given an π be a NDTP program, we define its dependency graph, denoted DG(π) = ⟨V, E⟩ where:

• Each vertex v ∈ V corresponds to an indexed subformula ϕj in the ω-unfolding πω of π, representing the instance of ϕ holding at position j in the trace.
• The arcs in E are defined recursively as follows:
• head-to-body links:
• for ○i r in πω , E has an arc head(r)i → body(r)i ;
• head formulas dependencies:
• an arc from (ϕ1 ∧ϕ2)i to ψj implies an arc ϕik →ψj ;
• an arc ϕi →ψj resp. ˆ○ϕi →ψj implies an arc ϕi+1 → ψj ;
• an arc (●ϕ)i → ψj resp. (ˆ●ϕ)i → ψj implies an arc ϕi-1 →ψj if i - 1 ≥ 0;
• an arc (ϕ1 Oe ϕ2)i → ψj , for Oe ∈ {Ue, Re, Se, Te}), implies an arc ϕsk → ψj for every k ∈ {1, 2} and every s ≥ i if Oe ∈ {Ue, Re} and s ∈ [0, j] otherwise;
• body formulas dependencies:
• an arc ϕi → (ψ1 △ψ2)j , for △ ∈ {∨,∧}, implies an arc ϕi → ψjk for k ∈ {1, 2};
• an arc ϕi → ○(ψ)j resp. ϕi → ˆ○(ψ)j implies an arc ϕi → ψj+1 ;
• an arc ϕi → ●(ψ)j resp. ϕi → ˆ●(ψ)j implies an arc ϕi → ψj-1 if j - 1 ≥ 0;
• an arc ϕi → (ψ1 O ψ2)j for O ∈ {U, R, S, T}) implies an arc ϕi → ψsk for every k ∈ {1, 2} and every s ≥ i if O ∈ {U, R} and s ∈ [0, j]; otherwise;

Intuitively, the construction parses each rule in π to extract its head and body, analyzing recursively its structure. As customary in logic programming, the transitive closure of DG(π) represents the positive dependencies in program π.

Definition 13 (Tight Temporal Program). A tight temporal program (TTP) is an NDTP program π that is tight, which means that DG(π) has no infinite path.

Definition 13 ensures the following property.

Lemma 2. If an NDTP program π is tight, then it is tight w.r.t. any possible trace T.

As a corollary of Theorem 5 and Lemma 2, we then obtain:

Theorem 6. Let π be a TTP program π. Then T is a TELmodel of π iff T is a supported LTL-model of π iff T ⊧ π ∧ tcc(π).

From Theorem 6 and the fact that the Clark completion tcc(π) is constructible in polynomial time, we thus obtain the following complexity result.

Theorem 7 (Satisfiability). Deciding whether a given TTP program π has a stable model is PSPACE-complete.

The membership comes from LTL, which is well-known to be PSPACE-complete. The PSPACE-hardness holds as we can express an LTL formula ϕ by ¬ϕ → bot and imposing □(¬¬p → p) for each atom p; note that ¬¬p → p is in THT equivalent to ¬p ∨ p (excluded middle).

Thus, for this class of programs TEL-satisfiability has the same complexity as classical LTL-satisfiability. However, to exploit this, we must check for tightness, which could be expensive. Fortunately, it turns out that this is not the case.

Deciding Tightness. We utilize a finite representation of the temporal dependency graph DG(π) in terms of a one-counter automaton [Comon and Jurski, 1998]. Such an automaton is a non-deterministic finite-state automaton operating on a single counter variable with value increments from {-1, 0, 1}.

Definition 14 (One-Counter Automaton). A one-counter automaton (OCA) A is a tuple (Q, Qt0 , ∆), where:

• Q is a finite set of control states,

• Qt0 ⊆ Q is a subset of control states,
• ∆ ⊆ Q × Q × {-1, 0, 1} is a finite transition relation.

Informally, Qt0 represents the set of states that can only be accessed if the counter equals zero. A configuration of an OCA is a pair (q, c) of a state q ∈ Q and an integer c ≥ 0 that represents the current value of the counter. The transition relation (q1, c1) → (q2, c2) between configurations holds if some (q1, q2, c) ∈ ∆ exists such that c2 = c1 + c, where in case qi ∈ Qt0 we must have ci = 0, for i ∈ {1, 2}.

A path from a configuration (q1, c1) to a configuration (q2, c2), denoted by π ∶ (q1, c1) →∗ (q2, c2), is a sequence of transitions leading from (q1, c1) to (q2, c2). We represent the dependency graph of a program π by an OCA ADG(π) = ⟨Q,Q0,∆⟩ as follows:

• Q = Qb ∪Qh ∪P, where Qb (resp. Qh ) contains ϕb (ϕh ) for each sub-formula ϕ in the body (head) of some rule r in π, where we let pb = pb = p for each atom p ∈ P;
• Q0 = {body(r)b ,head(r)h ∣ r ∈ init(π)};
• ∆ is defined recursively akin to E for DG(π), intuitively with a level increase or decrease in the ωunfolding of the program π. It contains
• head-to-body links:
• (head(r)h , body(r)b , 0), for each rule r ∈ init(π) ∪ dyn(π);
• head formulas dependencies: for each γ h ∈ Q of form
• (ϕh1 ∧ ϕh2 )h : (ϕkk , γ h , 0);
• (○ϕh )h , (ˆ○ϕh )h : (ϕh , γ h ,-1);
• (●ϕh )h , (ˆ●ϕh )h : (ϕh , γ h ,+1);
• (ϕh1 Oe ϕh2 )h , Oe ∈ {Ue, Re}): (γ h , γ h ,+1), (γ h , ϕhk , 0) for k ∈ {1, 2};
• (ϕh1 Oe ϕh2 ), Oe ∈ {Se,Te}): (γ h , γ h ,-1), (γ h , ϕhk , 0) for k ∈ {1, 2};
• body formulas dependencies: for each γ b ∈ Q of form
• (ϕb1 △ ϕb2 )b , △ ∈ {∧,∨}: (γ b ,ϕbk , 0) for k ∈ {1, 2};
• (○ϕb )b , ˆ○ϕb ) ∈ Q: (γ b ,ϕb ,+1);
• (●ϕb )b , (ˆ●ϕb )b ∈ Q: (γ b ,ϕb ,-1);
• (ϕb1 Oϕb2 )b , O ∈ {U,R}: (γ b , γ b ,-1), (γ b ,ϕbk , 0) ∈ ∆ for k ∈ {1, 2};
• (ϕb1 Oϕb2 )b , O ∈ {S,T}: (γ b , γ b ,+1), (γ b ,ϕbk , 0) for k ∈ {1, 2}.

Intuitively, ADG(π) keeps track of the dependencies between atoms in the dependency graph, by emulating arcs with counter increments resp. decrements. It faithfully represents DG(π) as follows.

Proposition 9 (OCA Correspondence). For any NDTP program π and atoms pi , qj , it holds that pi reaches qj in DG(π) iff (p, i) →∗ (q, j) in ADG(π).

We now exploit Proposition 9 to conclude that

Theorem 8. Deciding whether a given NDTP program π is tight for either finite or infinite semantics is in NL.

Proof. (Sketch) By Proposition 9, we can use the automaton ADG(π) instead of DG(π) and distinguishes cases.

Finitary case. We can only have infinite paths by looping. To check this, we can search for a loop under the following two restrictions: (i) we start from a non-deterministically chosen p ∈ P with a counter value 0, i.e, from (p, 0), and (ii) we limit the possible configurations to those with a counter value at most n3 + n2 , where n is the number of nodes in ADG(π). The bound can be obtained by adjusting a result from [Lafourcade et al., 2005] to our needs.

Infinitary case. Besides loop checking, we need to check for infinite paths with no configuration repetition. We first notice that there is such a path iff there exists a path of length n with an atom p such that there is a path from (p, i) to (p, j) with i < j. Therefore, one can try to search for a path where (i) the path passes by an initial configuration at least once and (ii) a path where no initial configurations are visited.

The NL membership follows then as we can construct ADG(π) using logarithmic workspace; used as an oracle, we can check in NL whether ADG(π) has a cycle.

6 Conclusion

Recent efforts aim to bridge ASP and Linear Temporal Logic (LTL), in particular in the context of planning [Cabalar et al., 2019] and monitoring [Sold`a et al., 2023]. Motivated by issues of the strong minimization criterion for stable models, we introduced eager unfolding temporal operators and defined non-disjunctive temporal programs (NDTP) and tight temporal programs (TTP), which amount to fragments of TEL. The latter can be readily translated in polynomial time into LTL using a temporal Clark completion, achieving an exponential complexity drop compared to full TEL and opening a possibility to use LTL-based model checkers.

Temporal Answer Set Programs (TASP) [Aguado et al., 2023] are a rule-based fragment of TEL that has been conceived as an extension of ASP. However, despite a rather plain form of rules, such programs harbour the full complexity of TEL [Cabalar, 2010] which is due to disjunction and ♢ in rule heads. This similarly follows from results about bidirectional answer set programs [Eiter and ˇSimkus, 2009; ˇSimkus, 2010] with a single function symbol, which amount to a fragment of TASP involving only ○ and □ as temporal operators; excluding disjunction in rule heads results in PSPACE-complexity. Our NDTP programs cater for a much richer syntax, with tight programs allowing for a polynomial translation into LTL.

Walega et al. [2021] also considered temporal dependency graphs, yet more for imposing a syntactic constraint to ensure that an immediate consequence operator reaches a fix-point in finite time; forward propagation, for instance, is ruled out. Beck et al. [2018] defined support of atoms from rules with temporal operators and complex formulas in the head. However, their notion is semantic without structural decomposition of formulas, requesting that turning the supported atom to false will violate the rule.

Future work will be devoted to implementation and application of the results for monitoring, as well studying possible restrictions and extensions of the program classes introduced.

Ethical Statement

There are no ethical issues.

Acknowledgments

The project leading to this application has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No 101034440.

Furthermore, this research was funded in whole or in part by the Vienna Science and Technology Fund (WWTF) project ICT22-023 and the Austrian Science Fund (FWF) project 10.55776/COE12.