Computational Aspects of Progression for Temporal Equilibrium Logic

1 Introduction

Reasoning about dynamic systems and dealing with temporal data appropriately is an important issue. To this end, a range of temporal logics such as LTL, CTL, LDL etc. has been developed that allows one to specify and assess the behavior of systems with automated support. Monitoring temporal constraints and properties is an essential task that provides input for decision-making, diagnostics, prediction, and many other tasks. In that, data becomes available in a growing stream, requiring that reasoning proceeds in an online fashion. To this end, monitoring approaches for LTL have been developed, in which a 3-valued semantics is employed [Bauer et al., 2007] that approximates the LTL semantics, by informally telling whether a property is established true, false, or remains open.

As with many logics, LTL is monotonic, which limits its applicability when it comes to model systems involving properties and features such as exceptions, dealing with incomplete information, or belief states. Nonmonotonic logics have been conceived to address such aspects. They e.g. allow for expressing defaults and normative behavior [Cabalar et al., 2023], offer a solution to the frame problem [McCarthy and Hayes, 1981; Kautz, 1986] by concise modeling of inertia, and are more amenable to elaboration tolerance [McCarthy, 1998] for developing logical representations. In particular, Equilibrium Logic [Pearce, 2006], which is the logical basis of Answer Set Programming (ASP), caters to this possibility.

In ASP, temporal reasoning is usually expressed by encoding time in the language, which has disadvantages compared to handling time as a first-class citizen. This is done in Temporal Equilibrium Logic (TEL) [Aguado et al., 2013], which combines Equilibrium Logic with LTL by imposing a stability condition on LTL models resorting to Temporal Here-and-There Logic (THT) [Aguado et al., 2013]. Rule-based fragments of TEL like Temporal ASP (TASP) [Aguado et al., 2023] allow one to express problems beyond LTL (e.g., conformant planning) [Bozzelli and Pearce, 2016]. The interest in TEL has been increasing in the recent years, fueled by the availability of native solvers such as telingo [Cabalar et al., 2019].

As of today, support for online temporal reasoning in ASP is immature. ASP Streaming engines such as oclingo [Cerexhe et al., 2014], ticker [Beck et al., 2017], i-dlv-sr [Calimeri et al., 2021] use incremental ASP evaluation, but support only limited fragments of TASP and are like telingo bound to finite traces. MeTeoR [Wang et al., 2022; Wał˛ega et al., 2023a] uses interval semantics and does not address monitoring.

Recent work has addressed this issue with progression for temporal ASP [Soldà et al., 2023]. Progression is a wellknown technique by which formulas are partially evaluated along temporal states. It has been widely used in logic-based AI, e.g., in planning [Bacchus and Kabanza, 1998], reasoning about actions [Giacomo et al., 2016], or stream reasoning [de Leng and Heintz, 2018]. Notably, the logical approach to incremental TEL allows one to verify at runtime whether a trace satisfies a TEL specification, and to integrate observations as facts that need no justification. While [Soldà et al., 2023] presented the approach and an algorithm for TASP progression, computational aspects such as complexity and tractability, which in an online setting is desired, were not addressed. We fill this gap with the following contributions:

• We extend the language for progression to full THT and TEL, and we generalize the 3-valued semantics and progression operators P and PTEL in [Soldà et al., 2023] for THT and TEL, respectively. Furthermore, we provide a novel incremental version P inc TEL of TEL progression, which is better suited for online evaluation.
• We characterize the complexity of monitoring under TEL3

and THT3 semantics, showing that they are like TEL and THT EXPSPACE-complete and PSPACE-complete, respectively, in general [Bozzelli and Pearce, 2015]; we remind that LTL is PSPACE-complete. In our analysis, we also address observations provided as facts in an online manner; notably, they do not lead to a complexity increase in general.

● We show that THT progression with P is feasible in polynomial time, while TEL progression with PTEL (and likewise P inc TEL ) is mildly intractable, viz. D p -complete. Since stable model checking of (atemporal) ASP programs is coNP-complete [Eiter and Gottlob, 1995; Pearce, 2006], this is close to what we optimally could expect. The derivation employs suitable structures for storing progression formulas that can be incrementally maintained. We then present normal and headcycle-free temporal ASP programs as tractable classes of TASP for TEL progression with PTEL, while unrestricted TASP harnesses the full complexity of THT resp. TEL.

Our results show that PTEL and P progression are (nearly) tractable approximations of the TEL and THT semantics and their 3-valued versions. Furthermore, P inc TEL is a promising basis for practical implementation, as the syntactic restrictions allows one to express action domains and goals to be achieved.

2 Preliminaries

Both TEL and THT over infinite traces [Aguado et al., 2013] share the same syntax. We are interested in a fragment L of LTL with past-time operators, generated by the grammar

where p ∈ P for a finite set P of propositional atoms and ○ ∈ {∧, ∨, →}. Negation is defined as ¬ϕ ≡ ϕ → bot and ⊺ ≡ ¬bot. As usual, G (globally) is defined by Gϕ ≡ botRϕ and F (finally) by Fϕ ≡ ⊺Uϕ.

The semantics of THT is defined via sequences of pairs of sets of atoms. A THT-trace (or simply trace, if clear from context) is an infinite sequence ⟨H,T⟩ of pairs ⟨Hi,Ti⟩, where Hi ⊆ Ti ⊆ P for each i ≥ 0. Both H and T are traces as usual, i.e., infinite sequences H = H0,H1, . . . resp. T = T0,T1, . . . of sets of atoms.

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:

• I, k /⊧ bot
• I, k ⊧ p if p ∈ Hk, for any atom p ∈ P
• I, k ⊧Y ϕ if I, k - 1 ⊧ ϕ and k > 0
• I, k ⊧ ϕ∨ψ if I, k ⊧ ϕ or I, k ⊧ ψ
• I, k ⊧ ϕ∧ψ if I, k ⊧ ϕ and I, k ⊧ ψ

• I, k ⊧Xϕ if I, k + 1 ⊧ ϕ
• I, k ⊧ ϕ U ψ if there is j ≥ k s.t. I, j ⊧ ψ, and for all j ′ ∈ [k, j), I, j ′ ⊧ ϕ
• I, k ⊧ ϕRψ if for all j ≥ k s.t. I, j /⊧ ψ, there exists j ′ ∈ [k, j), I, j ′ ⊧ ϕ

A THT-trace I is a model for a formula ϕ if I, 0 ⊧ ϕ.

A THT-trace I is total, if H = T; we then simply write T for ⟨T,T⟩ if no confusion arises. Notably, T ⊧ ϕ, i.e., ⟨T,T⟩ ⊧ ϕ, iff T ⊧LTL ϕ [Aguado et al., 2011]. The salient difference between THT and LTL is a different evaluation of →. In particular the excluded middle axiom p ∨ ¬p does not hold in THT. This is witnessed by e.g., I = ⟨H,T⟩ where H = ∅ω and T = {p}ω . However, THT collapses to LTL under a temporal excluded middle axiom

Proposition 1 (cf. [Cabalar and Demri, 2011]). For ϕ ∈ L and I=⟨H, T⟩, I ⊧ ϕ ∧ T EM iff T ⊧LTL ϕ and T = H.

For traces T,T′ , and O, we write T ≤O T′ if Oi ⊆ Ti ⊆ T′i holds for every i ≥ 0. Furthermore, for THT-traces I = ⟨H,T⟩, I′ = ⟨H′ ,T′ ⟩, and a trace O, we write I ≤O I′ if H ≤O H′ and T = T′ . Intuitively, ≤O serves for defining Hminimality modulo observations; they are present in O online as facts and thus do not need to be proven.

We are now ready to introduce the semantics of TEL.

Definition 2 (TEL-Satisfaction w.r.t. Observations). Given an observation trace O, a trace O ≤ T is a temporal equilibrium model of a formula ϕ ∈ L w.r.t. O, if (i) ⟨T,T⟩ ⊧ ϕ, i.e., T is a total THT model of ϕ, and (ii) no H ≠ T exists s.t. H ≤O T and ⟨H,T⟩ ⊧ ϕ, i.e., ⟨T,T⟩ is minimal w.r.t. O.

If the observation trace O is empty, i.e., O = ∅ω , Definition 2 yields classical TEL satisfaction [Aguado et al., 2013]. Given two traces T,O and a formula ϕ ∈ L, we denote by T ⊧OTEL ϕ that T is an equilibrium trace of ϕ modulo observations O, where we may drop O if clear from context.

We will use temporal equilibrium model and equilibrium/stable traces interchangeably. Furthermore, we shall consider temporal programs [Cabalar, 2010], a fragment of L that resembles and extends the usual logic programming syntax.

Example 1. Assume T and O are traces, where switch, and power_failure can appear in O (they need no justification). A model πEX of an action domain has the following axioms:

r0 ∶ switch ∨ X anomaly

• r1 ∶ G(switch ∧ ¬light ∧ ¬X anomaly → X light)
• r2 ∶ G(switch∧ ¬X anomaly →X change_light)

r3 ∶ G(light ∧ X anomaly →X change_light)

r4 ∶ G(¬X change_light ∧ light → X light)

• r5 ∶ G(power_failure → anomaly)
• r6 ∶ G(switch ∧ X switch → bot)

Intuitively, r0 says that either the light will be turned on, or an anomaly will happen at the second state; r1 is a defeasible effect axiom; r2 and r3 keep track of action executions or anomalies that flip the value of light; r4 is an inertia rule for light; r5 defines the power_failure as an anomaly; r6 is the property to monitor. Trace T = {s}, {c_l, l}, {a, p_f, c_l}, {a, p_f}ω is an equilibrium trace of πEX w.r.t. O = {s}, ∅, {p_f}ω .

We recall that in LTL, satisfiability is PSPACE-complete; the same holds for THT, while in TEL satisfiability is EXPSPACE-complete [Bozzelli and Pearce, 2016], where EXPSPACE-hardness holds for temporal programs. LTL stays in PSPACE if past time operators (including Y) are added, cf. [Lichtenstein et al., 1985]; this extends to the language L.

Lemma 1. Deciding whether ϕ ∈ L is THT- (resp. TEL-) satisfiable is PSPACE- (resp. EXPSPACE-)complete.

3 Online Setting

In online computation, we only have a prefix of a trace at any point in time. This motivates the following THT3 semantics with truth-values true (⊺), false (bot), and undefined (?). Given a THT-trace I = ⟨H,T⟩, its k-prefix (resp. k-suffix or suffix at k) is the sequence ⟨H0,T0⟩, . . . , ⟨Hk,Tk⟩ (resp. Ik = ⟨Hk,Tk⟩, ⟨Hk+1,Tk+1⟩, . . .), 0 ≤ k. A prefix of I is any k-prefix If of I whose length, denoted by ∣If ∣, is k+1. We call I an extension of If w.r.t. observation trace O, if H ≤O T holds; by ext(If ,O) we denote the set of all such I. We denote by PreTHT the set of all possible prefixes. Similarly as above, we may write Tf instead of ⟨Tf , Tf ⟩ and omit O.

Definition 3 (THT3 semantics, cf. [Soldà et al., 2023]). The truth value of ϕ ∈ L w.r.t. a prefix If and an observation trace O is as follows:

Here O is a parameter to define a 3-valued logic for TEL, where minimality over traces matters. If O is empty, Defn. 3 is the THT version of the LTL3 logic of Bauer et al. [2007]; further restriction to total traces yields their LTL3 semantics.

TEL3 semantics The 3-valued semantics of TEL, depicted in Figure 1, has been defined as follows:

Definition 4 (TEL3 semantics, cf. [Soldà et al., 2023]). For a total prefix Tf of length k, ϕ ∈ L, and observation trace O,

Note that the single minimal LTL model in ext(Tf ,O) is used for the verdict v = ⊺; this is because nonmonotonicity of TEL may compromise the persistence of verdict ⊺ when Tf is extended. The possible evolution of the verdict over time is illustrated in Figure 2. The dotted arrow would not appear in a monotonic setting like LTL3 , or THT3 , as ⊺ would be valid. For example, for ϕ = G(q ∨ ¬ q) ∧ G(q → G p) we have ∅ ⊧TEL3 ϕ = ⊺, while ∅⋅{q, p} ⊧TEL3 ϕ = ?. The reading of verdict ⊺ is that if nothing is left to be proven (i.e., empty T-suffix), this extension yields an equilibrium trace.

THT has the so-called persistence property, viz. that ⟨H,T⟩ ⊧ ϕ implies T ⊧ ϕ. As we deal with three possible verdicts and a fixed prefix, only a weaker form holds.

Lemma 2 (Persistence for THT3 ). For every ϕ ∈ L, prefix If = ⟨Hf ,Tf ⟩, and observation trace O, If ⊧OTHT3 ϕ≠bot implies Tf ⊧OTHT3 ϕ≠bot.

Note that both (I1) If ⊧OTHT3 ϕ = bot and (T1) Tf ⊧OTHT3 ϕ = ⊺ may hold. E.g., for ϕ = p ∨ ¬p, empty O, Tf = {p}, and If = ⟨∅, {p}⟩, we have If /⊧ p ∨ ¬p while Tf ⊧ p ∨ ¬p. Similarly, both (I2) If ⊧OTHT3 ϕ = ⊺ and (T2) Tf ⊧OTHT3 ϕ = ? may hold, e.g. for ϕ = p → Xp and O, If , Tf as before.

3.1 Complexity

We now analyze the complexity of the THT3 and the TEL3 semantics. We assume that prefixes of traces are explicitly given. We consider here that O is described by an LTLformula ψ, such that for each model T of ψ and position i ≥ 0, T, i ⊧LTL p iff p ∈ Oi.

We start by showing a negative result about the complexity of computing the verdict of THT3 and of TEL3 semantics, that justifies the introduction of the progression function P, and, respectively, PTEL, which are more efficient.

Theorem 1. Given ϕ ∈ L, a prefix If = ⟨Hf ,Tf ⟩, and a arbitrary observations trace O model of an LTL formula ψ, namely O ⊧LTL ψ, deciding If ⊧OTHT3 ϕ = v for v ∈ {⊺, bot, ?} is PSPACE-complete, and PSPACE-hardness holds if v is fixed arbitrarily and O is empty.

The hardness results are shown by simple reductions from THT-(non)validity, and the membership results by reductions to LTL-(un)satisfiability. For the latter, we exploit the startransformation of THT into LTL [Cabalar and Demri, 2011]. We encode the prefix If into a formula ϕIf and use the following formula ψO to constrain the models by the observations from O, which are expressed by the LTL formula ψ:

where ¯ ψ is ψ with all occurrences of p replaced by ¯ p and T EM¯ P is T EMrestricted to the atoms in ¯ P = {¯ p ∣ p ∈ P}.

Proposition 2. The THT-models I of ψO coincide on P with the traces over P that include O, and each I restricted to ¯ P is total and coincides with the bar-version ¯O of O.

For the TEL3 -semantics, we obtain a complexity picture analogous to Theorem 1.

Theorem 2. Given ϕ ∈ L, an LTL-prefix Tf , and a formula ψ describing an observation trace O, deciding Tf ⊧OTEL3 v for a given v ∈ {⊺, bot, ?} is EXPSPACE-complete, where EXPSPACE-hardness holds if v = bot or v =?, while for v = ⊺ the problem is PSPACE-complete and co-NP if O = ∅ω .

The EXPSPACE membership and hardness results are shown by reductions to resp. from TEL-(un)satisfiability, where the hardness results hold if, in addition, O is empty. For v = ⊺, the problem is in PSPACE: there are only exponentially many If for which must check If ⋅Ok ⊧ ϕ, where k is the length of Tf . For each such If , this reduces to an LTLentailment test, which is in PSPACE, and looping through all If is feasible in PSPACE. Notably, if in addition, O is empty, the complexity drops to co-NP as the test If ⋅∅ω ⊧ ϕ reduces to an LTL-model checking problem that is polynomial. The PSPACE- resp. co-NP-hardness is inherited from the complexity of LTL resp. ASP programs [Eiter and Gottlob, 1995].

We note that the hardness proofs in Theorem 2 can be adjusted to temporal programs showing that they harness the full complexity of TEL3 -semantics.

4 Progression for THT

As many monitoring tools have an online setting (see [Cimatti et al., 2022], [Chen and Ro¸su, 2007] among the others), we are interested in studying a framework where observations are provided on the fly. We thus consider an online computation of the THT3 semantics that relies on the progression technique for THT in [Soldà et al., 2023], which yields an approximation of the THT3 semantics.

In the progressive evaluation of a formula, an implication ϕ = p → Fq may be only partially evaluable in the current state -when p belongs to the current state, but q does not- and we must delegate part of the evaluation to the future, therefore we rewrite ϕ as Fq. The main idea is that we propagate Fq until we see q in the trace, when we can finally conclude ⊺.

We denote by Lc the set of formulas generated by the grammar in (1), where in place of → also →c may occur. The →c implication guides the progression by marking implication that must be evaluated in the There-trace only. Note that [Soldà et al., 2023] disregarded full U and R (only F and G were considered). We now introduce THT progression.

Definition 5 (THT progression on a prefix state). Progression P ∶ Lc ×PreTHT ×N→Lc is the partial function mapping a formula ψ, a THT-prefix If = ⟨Hf ,Tf ⟩ of length k, and an integer i ∈ [0, k), to an Lc formula as follows:

1. P(bot, If , i) = bot

1. P(Xϕ, If , i) = ϕ

In addition, ⊺ →∗ bot is replaced by bot; bot →∗ ϕ by ⊺; and ϕ →∗ ⊺ by ⊺, for every formula ϕ and →∗ ∈ {→,→c}.Furthermore, ⊺∨ϕ is replaced by ⊺; bot∨ϕ by ϕ; bot∧ϕ by bot; and ⊺∧ϕ by ϕ. Note that P(Gϕ, If , i) = P(ϕ, If , i)∧Gϕ and P(Fϕ, If , i) = P(ϕ, If , i) ∨ Fϕ. We do not apply the progression recursively on the future states, but we do so on the sub-prefix of the trace, as we assume to have access to the current and past states. Let us progress rule r2 ∈ πEX of the Example 1 over Tf = {s}. The application of progression leads to P(r2, ⟨Tf , Tf ⟩, 0) = G(s ∧ ¬X a →X c_l) ∧ (¬a → c_l).

Lemma 3. If ϕ has no temporal operators, then P(ϕ, If , k)=v, v ∈ {⊺, bot}, for every trace If and k ∈ [0, ∣Tf ∣).

In an online setting, the prefix is provided incrementally, extending it by one state at each iteration. The progression over a prefix is thus defined as follows.

Definition 6 (THT progression on a prefix). The progression of ϕ ∈ L on the THT-prefix If is

An intuitive reading of the progression outcome P(ϕ, If ) = v is as follows: (i) v = ⊺ means that the property expressed by ϕ is already satisfied within the prefix If ; (ii) the case v = bot is the opposite, i.e., the violation of ϕ has been detected within the prefix I; finally, (iii) v = ? means that one abstains given the partially processed formula ϕ. The following result now states that the progression function P faithfully approximates the THT3 semantics.

Theorem 3 (THT verdict on prefixes). For every prefix If , observation trace O, and formula ϕ ∈ L,

4.1 Computing P Progression

In the next results, we show that a P application to a formula ϕ ∈ Lc on a prefix If is feasible in polynomial time. By Theorem 3, we thus may justify P progression as a tractable approximation of the THT3 semantics. We first show that computing a single progression step on a state that is tractable.

Let us denote by → nψ the number of → and →c symbols in ψ, by temp nψ the number of U and R symbols in ψ.

Theorem 4. Given ψ ∈ Lc, a prefix If of length k, and s ∈ [0, k), obtaining some ψ′ ≡THT P(ψ, If , s) = ψ′′ is feasible in polynomial time where (i) ψ′′ ∈ {⊺, bot} implies ψ′ = ψ′′ and (ii) ∣ψ′ ∣ ≤ ( → nψ +1)(temp nψ +2)∣ψ∣.

Proof (Sketch). The result is obtained by using two look-up tables T and H, where each sub-formula φi of ψ is progressed for Tf resp. If at every position t ∈ [0, k) to a formula φ′i that is memorized in T [φi, t] resp. in H[φi, t]. One can then assemble ϕ′i from the progression results of its subformulas ϕ′j stored in T and H. The key to having a polynomial-size

Figure 3: Abstract syntax tree of ψ, where p, q, r, s ∈ P.

output is the fact that for progression over a total trace, we need to consider only one of → and →c in the assembly as they yield equivalent results. Without this optimization, the application of P may lead to exponential outcomes.

Note that whenever φ′i /∈ {⊺, bot}, we can simply write T [φi, t] =? (or T [φi, t - 1] =? for the Y-case) if we are interested in the decision problem only.

For computing P(ϕ, If ), repeated application of P(ϕ, If , k) does not allow us to conclude tractability, as ϕ may grow exponentially when progression is applied due to U and R operators. As an extreme example, consider the case of nested U: ψi = ψ2i+1 U ψ2i+2 for i = 0, . . . , 2n-1 - 1 and ψi = F p for some p ∈ P for all i = 2n-1 , . . . , 2n - 1, whose abstract syntax tree is depicted in Figure 3. By repeated application of P as in Theorem 4, P(ψ0, Tf ) grows exponentially in the size of Tf = ∅k≥1 .

Fortunately, we can avoid exponential explosion by sharing subformulas. Indeed, progressing in the example ψ0 over ∅ will yield two copies of ψ1 in the output formula for progression at state 1; these copies can be shared.

To represent formulas for the THT progression in a succinct way, we use the following concept and notation. A DAG representation of a formula ψ is any directed acyclic graph resembling the syntax tree of ϕ with possible sharing of subtrees. Let us denote by Ptemp(ϕ, If , i) the formula as in Definition 5 but with result p in cases 2 and 3; i.e., p is not evaluated over If and thus independent of If .

Definition 7. Given a DAG-representation of ψ ∈ L and ϕ ∈ sub(ψ), we denote by N j i ϕ the DAG representing the formula P j temp (ϕ, If , i) for any If of length ≤ i.

Notably, Ptemp(ϕ, If , i) can be viewed as a template to obtain P(ϕ, If , i) by evaluating it over prefix If , and accordingly N j i ϕ represents a template P j temp (ϕ, If , i) whose evaluation over If yields P j (ϕ, If i ), i.e., the result of j-fold progression of ϕ over the i-suffix of If .

Lemma 4. Given ψ ∈ L and k > 0 written in unary, we can compute N k 0 ψ in polynomial time (more precisely in O(k2 ∣ψ∣) time).

Proof. We provide an algorithm that computes a DAG with the root node labeled by N k 0 ψ, saving memory by means of sharing subformulas. Given the abstract syntax tree of the formula, we label each node representing the subformula ϕ by N 0 0 ϕ. When applying progression to N j i ϕ, we check whether already a node for N j+1 i ϕ exists; if so, the reference to N j+1 i ϕ is used; otherwise a new node N j+1 i ϕ is created, and we rewrite ϕ, applying Definition 5, with references to the progressions of its subformulas, by cases as follows:

• N j+1 i ϕ points to N j i ϕ, if ϕ has no temporal operators;
• N j+1 i Xϕ points to N j i+1ϕ;
• N j+1 i Yϕ points to N j+1 i-1 ϕ;
• N j+1 i ϕ1Uϕ2 points to a formula for N j+1 i ϕ2∨N j+1 i ϕ1∧ N j i+1 (ϕ1Uϕ2); to avoid introducing nodes for new subformulas, we may view U progression as a ternary connective, where ϕ1Uϕ2 = bot ∨ ⊺ ∧ (ϕ1Uϕ2). The case N j+1 i (ϕ1Rϕ2) is analogous.

We iterate the process from j = 0, . . . , k until the root of the DAG is labeled by N k 0 ψ; importantly, eachN j i of k2 ∣ψ∣ nodes occurs at any point in time at most once in the DAG.

Also in this case, we first run the algorithm for the T- part, successively for the H-part. The Here-DAG may share some nodes from the There-DAG if there are implications.

Thus, we can tractably compute the verdict of the progression on a formula ψ when a new state is provided:

Theorem 5. For any ϕ ∈ L, prefix If , such that ∣If ∣ = k, a DAG representation of P(ϕ, If ) is computable in polynomial time (more precisely, in O(k2 ∣ψ∣) time).

Proof. By Lemma 4, the DAGN k 0 ψ for the template formula P k temp (ϕ, If , 0) is computable in O(k2 ∣ϕ∣) time and by following the lookup technique of Theorem 4 we can compute the verdict, where the Here-DAG and the There-DAG allow us to efficiently navigate to sub-formulas; this is also feasible, including simplifications, in O(k2 ∣ϕ∣) time.

5 Progression for TEL

TEL progression resorts to THT progression as follows.

Definition 8 (TEL progression on a prefix, cf. [Soldà et al., 2023]). The TEL progression of ϕ ∈ L on a total prefix Tf is

Definition 8 faithfully approximates TEL3 semantics.

Theorem 6 (TEL verdict on prefixes). For any formula ϕ, prefix Tf , and observation trace O, PTEL progression is sound w.r.t. the TEL3 -verdict, i.e.,

We note that while both THT3 and TEL3 in Defn. 3 resp. 4 take an observation trace into account, the progressions P and PTEL do not. This is because we assume the observations are already encoded in the prefix of the trace to progress. If we replace Hf ⊂ Tf in Defn. 8 with Hf <O Tf defined by Oi ⊆ Hfi ⊆ Tfi for i ∈ [0, ∣Tf ∣) and Hf ≠ Tf , Theorem 6 still holds.

Since we focus on online computations, we introduce an incremental PTEL progression, where we resort to the Y temporal operator to rewrite the formula, unfolding it using the inductive definitions of the temporal operators.

Definition 9. The incremental version of TEL progression of ϕ ∈ L on a total prefix Tf for position i ∈ [0, ∣Tf ∣) is

where ϕ′i = P(ϕ, ⟨Tf , Tf ⟩, i), ϕ′′ i (Hf ) = P(ϕ, ⟨Hf , Tf ⟩, i), ϕY is defined inductively by

We define P inc,i TEL (ϕ, Tf ) as the P inc TEL progression reached at state i, i.e., P inc,0 TEL (ϕ,Tf , 0) = ϕ and P inc,i TEL (ϕ,Tf ) = P inc TEL(P inc,i-1 TEL (ϕ,Tf ),Tf , i) for 0 < i ≤ ∣Tf ∣. Then we obtain at the end of Tf the PTEL-result. Formally, let P inc TEL(ϕ,Tf ) = P inc,∣Tf ∣ TEL (ϕ,Tf ). Then

Theorem 7. For every ϕ ∈ L and prefix Tf , PTEL(ϕ, Tf ) = v iff P inc TEL(ϕ, Tf ) = v.

Note that the possible evolution of the verdict over time is still captured by Figure 2 even under the 3-valued semantics induced by PTEL (or, equivalently P inc TEL ).

5.1 Computing PTEL Progression

The results above show an exponential complexity gap between THT3 -satisfiability (PSPACE-complete) andTELsatisfiability (EXPSPACE-complete). We find a complexity gap between the P and the PTEL approximation, but it is much smaller: while intractable, PTEL is in the Boolean Hierarchy and close to NP and co-NP, being not harder than the conjunction of an NP and a co-NP problem.

Theorem 8. Given ϕ ∈ L and a prefix Tf , deciding PTEL(ψ,Tf ) = v is (i) for v = ⊺ co-NP-complete, (ii) for v = bot NP-complete, and (iii) for v =? D p -complete.

This result is shown by exploiting Theorem 5 for the upper bounds, and by providing reductions from stable model checking problems for logic programs for the hardness parts.

Thus, while by Theorem 8 PTEL progression requires NP/co-NP oracle calls, it may be as a near-tractable approximation of the TEL3 semantics.

Note that the complexity proofs for PTEL-progression exploit Theorem 5 for checks of varying prefixes If . The progression DAGs N k 0 of P(ψ, If ) in Lemma 4 can be instantiated for them on the fly, and with P inc TEL we can easily extend N k 0 incrementally. It is possible to see that the DAG representation leads to an equivalent formula of the P inc TEL . Taking the N k i=0 as a starting point we proceed top-down adding the proper connectives and placing k - i many Y operators in front of the sub-formula associated with the leaves of the DAG.

5.2 Progressing Temporal Programs

As mentioned, temporal ASP programs are an important fragment of TEL, for which efficient PTEL progression is desirable. We achieve this by suitable syntactic restrictions that resemble well-known classes of logic programs.

Definition 10 (Temporal Programs, cf. [Cabalar, 2010; Aguado et al., 2023]). A temporal program is any set of temporal rules of one of the following forms:

• (initial rule)

• (dynamic rule) Gr, where r is an initial rule;
• (fulfillment rule) either G(Gp → q) or G(p → Fq), where p, q are atoms.

An initial or dynamic rule r is a constraint, if its head is bot (i.e., l=0), and is a fact if its body is empty (k=0) and l=1. We call {p,X p ∣ p ∈ P} temporal atoms, and we denote by B+ (r) (resp. B- (r)) the set of (resp. negated) temporal atoms in the body of r, and by H(r) the set {c1, . . . , cl}.

Using auxiliary atoms, temporal programs are as expressive as full TEL [Cabalar, 2010] and harness the full complexity of TEL. This is paralleled by the fact that the complexity results in Theorem 8 carry over to temporal programs; in particular that PTEL progression is D p -complete.

As a syntactic restriction, we first consider normal programs, namely rules r, where H(r) = {p} or {X p}, i.e. l ≤ 1 w.r.t. (4) and fulfillment rules.

Theorem 9. Given a normal temporal program π and a prefix Tf , deciding whether PTEL(Tf , π) = v for v ∈ {bot, ⊺, ?} can be done in polynomial time.

Proof (Sketch). Let k = ∣Tf ∣-1. By Lemma 4 and Theorem 5, we can compute N k 0 in polynomial time, and evaluate it on Tf in polynomial time, obtaining as outcome vTf . According to the conditions of PTEL(Defn 8), we may have to consider some (all) Hf ⊂ Tf and evaluate N k 0 over If = ⟨Hf ,Tf ⟩. N k 0 represents a set of implications, and after evaluating in N k 0 the negated atoms over Tf , the atemporal rules (not involving any temporal operator) in N k 0 amount to a set of Horn clauses. We can compute the least model Mf of these clauses in polynomial time resp. find they have no model. As for the remaining implications in N k 0 , sub-formulas within the scope of an X,G,F operator cannot lead to ⊺ or bot, and thus either formulas are removed (when ϕ′′ (Hf ) should yield bot) resp. subformulas (when ϕ′′ (Hf ) should yield ⊺) before computing Mf . From vTf and Mf , we then easily obtain PTEL(Tf , π).

Unfortunately, the temporal program πEX is not a normal temporal program. In what follows we extend tractability to the larger head-cycle-free class, which includes πEX.

Given a temporal program π, its ω-unfolded version πω contains every initial rule r ∈ π and for each dynamic or fulfillment rule G(r) ∈ π it contains Xi (r) for all i ≥ 0.

For the sake of readability given an unfolded rule Xk (r), we denote p,X q ∈ B+ (r) ∪ B- (r) ∪H(r) as pk and qk+1 .

Definition 11 (Dependency Graph). The dependency graph of a temporal unfolded program πω is the directed graph DGπ = ⟨V,E⟩ where V = {pi ∣ p ∈ P and i ≥ 0} and (i) (a, b) ∈ E if a ∈ H(r) and b ∈ B+ (r) for some rule Xk r in πω , (ii) (qk , pk′ ) ∈ E for k′ ≥ k if Xk (Gp → q) ∈ πω , and and (iii) (qk′ , pk ) ∈ E for k′ ≥ k if Xk (p → Fq) ∈ π.

Intuitively, (ii) and (iii) are added because we can read Gp and Fp as a conjunction resp. disjunction of Xip, i ≥ 0.

We call a program π head-cycle free (hcf), if all the heads contain only positive temporal atoms, and its ω-unfolded version πω has the hcf property defined as follows: whenever distinct a, b ∈ V are on a cycle of DGπ, then (a) no rule Xk r ∈ πω satisfies {a, b} ⊆ H(Xk r) and (b) if a = qk and b = qk′ with k ≠ k′ then no fulfillment rule Xk (p → F q) ∈ πω exists. E.g., the program in Example 1 is hcf.

This notion of hcf for temporal programs conservatively extends hcf for logic programs in [Ben-Eliyahu and Dechter, 1994]. As well known, hcf logic programs can be rewritten into normal logic programs by shifting atoms from the head to the rule body. This property generalizes to temporal programs.

Formally, denote for an initial rule r by r← the set of all rules r′ such that B+ (r′ ) = B- (r), B- (r′ ) = B- (r) ∪ (H(r) ∖ {a}), and H(r′ ) = {a}, where a ∈ H(r), and by π← the result of replacing in program π each initial rule r and dynamic rule Gr by r← resp. Gr′ , for all r′ ∈ r←. We then establish the following result, which is of interest in its own right.

Proposition 3. For any hcf temporal program π, π and π← have the same equilibrium models.

As the program π← is easily constructed from program π, we can generalize Theorem 9 to a larger class of TASP:

Theorem 10. Given a hcf temporal program π and a prefix Tf , deciding whether PTEL(Tf , π) = v for v ∈ {bot, ⊺, ?} can be done in polynomial time.

The notion of hcf can, in particular, be fruitfully applied to TASP classes from the literature, such as the STLP fragment [Cabalar and Diéguez, 2011]. STLP admits two types of initial rules: (i0) B∧N →H, or (i1) r: B∧XB′ ∧N ∧XN ′ → XH, and dynamic rules G(r) with r an initial rule of type r1, where B,B′ are conjunctions of atoms, N,N ′ are conjunctions of negative literals ¬p with p ∈ P, and H,H′ , are disjunctions of atoms. Notably, program πEX is of this form. We show that for STLP programs, the hcf property can be efficiently verified. Let DGiπ , i ≥ 0, be the subgraph of DGπ induced by all nodes pj , where p ∈ P and j ≤ i.

Proposition 4. A STLP program π is hcf iff DG1π satisfies the hcf-condition.

Figure 4 shows the clipped dependency graph DG1πEX , from which the hcf property of πEX is immediately verified.

Notably, we can use DGiπ to efficiently progress programs π whose unfolding on the prefix If is hcf. Let us say program

π is k-hcf if DGkπ satisfies the hcf-condition.

Corollary 1. Given a temporal program π and a prefix Tf , deciding whether PTEL(Tf , π) = v for v ∈ {bot, ⊺, ?} can be done in polynomial time if π is (∣If ∣ - 1)-hcf.

The k-hcf condition can be efficiently checked along the progression, as DGkπ can be incrementally built.

6 RelatedWork

Progression has been widely used in CPS, but also in KR, e.g., in [Zhou and Zhang, 2017], to generalize the GL reduct for ASP with variables; in [Belle and Levesque, 2020] and [Liu and Feng, 2023] to reason about actions in the presence of belief; in [Lin and Reiter, 1997] and [Vassos and Levesque, 2013] to update a database by the execution of an action.

Bozzelli and Pearce [2016] made a detailed complexity study of TEL, but considered merely 2-valued semantics.

Tools for stable traces are telingo [Cabalar et al., 2019], which builds on the clingo solver and handles finite traces, and STeLP [Cabalar and Diéguez, 2011], which is based on automata. Progression in temporal ASP is a novel approach in [Soldà et al., 2023], where recently a framework for temporal skeptical reasoning was proposed. However, no complexity study was provided for the monitoring problem.

Furthermore, several stream reasoners and incremental solvers for ASP semantics exist. One of the first incremental ASP-solvers was oclingo [Cerexhe et al., 2014], which extends clingo to handle dynamic events. TICKER [Beck et al., 2017] is another incremental stream reasoner for finite streams, which implements a fragment of LARS [Beck et al., 2018]. Calimeri et al. [2021] present an efficient stream reasoner, which however is limited to stratified programs.

MeTeoR [Wang et al., 2022] builds on DatalogMTL, which is an extension of Datalog with MTL operators. Wał˛ega et al. [2023a] recently proposed an incremental approach. The main differences between the setting we consider are that they (1) consider an interval-based semantics, (2) use Horn rules precluding backward propagation of information, and (3) define a reduct-based semantics. Furthermore, Walega et al. [2021; 2023b] introduced a stable semantics for negation akin to temporal ASP. They studied the complexity of stable model existence, but neither monitoring nor progression.

7 Conclusion

We have characterized the complexity of THT3 and TEL3 , as well as of progression for THT and PTEL by the P and the PTEL operator, respectively. Our results show that progression can be viewed as a (nearly) tractable approximation of THT3 and TEL3 semantics, and that tractability holds for significant fragments covering classes of temporal logic programs.

Our work can be extended in various directions. One could allow for past-time operators without any restriction, but a compact representation of progression formulas like a DAG would be barely needed. More expressive observation traces, represented by automata, and sets of observation traces can also be taken into account, modeling possible nondeterminism in the system. Our future agenda includes this and developing efficient implementations based on the algorithms and results presented, as well as refining the progression technique.

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. This work has been partially supported by the WWTF project ICT22-023.