Equivalent Stream Reasoning Programs

Introduction

Stream reasoning is an emerging research field that aims at providing logic-oriented techniques on top of stream processing. High throughput of data is a central challenge for stream processing methods, which usually focus on low-level computations such as filtering and aggregation. Central to modern stream processing technologies are window mechanisms that limit the input to snapshots of recent data. Window operators can be utilized either to define which data is still relevant, or as a practical means to cope with the volume of data. Also declarative methods and logic-oriented languages for reasoning over data streams have been considered [Do et al., 2011; Gebser et al., 2012], in particular, ones that allow to express such windows [Barbieri et al., 2010b]. A recent expressive formalism is the logic-based LARS framework [Beck et al., 2015b], which allows for generic window functions and temporal operators in formulas. On top of this, LARS provides rule-based semantics that can be seen as an extension of Answer Set Programming (ASP) for data streams.

⇤This research has been supported by the Austrian Science Fund (FWF) projects P24090, P26471, and W1255-N23.

Declarative and logic-oriented approaches to stream reasoning typically aim for more expressiveness, which makes efficient evaluation even harder to achieve. One way to mitigate this problem is to optimize queries or programs by simplifying them using equivalence preserving transformations. However, this requires support for checking when two programs are equivalent in the first place.

Various notions of query or program equivalence have been studied in the literature, e.g., in database research and for answer set programs [Lifschitz et al., 2001; Eiter and Fink, 2003; Eiter et al., 2007b]. However, equivalence relations between declarative programs for stream reasoning have not been considered so far. Towards optimization of such programs, we are thus interested in techniques that allow us to tell when two programs produce the same results. Characterizing equivalence between LARS programs in purely logical terms is challenging due to a non-structural definition of the FLP-semantics [Faber et al., 2004] defined for them, which imposes some limitations. Yet another difficulty arises from the generic definition of window operators.

We tackle this issue with the following contributions:

• ÷ We develop practically relevant notions of equivalence for LARS programs that extend well-known equivalence relations for logic programs and introduce data equivalence for streams.
• ÷ We define a novel logic called Bi-LARS to capture the FLPbased semantics of a large fragment of LARS programs, including the practical one introduced in [Beck et al., 2015a] that we call plain LARS.
• ÷ We lift model-theoretic characterizations of strong/uniform/relativized uniform equivalence from ASP to the stream setting to characterize the defined equivalence relations.
• ÷ We introduce the notion of monotone windows and show how a variant of Bi-LARS leads to an extension of the logic of Here-and-There for our setting. We thus get a link to equilibrium logic [Lifschitz et al., 2001] for a class of programs.
• ÷ Finally, we investigate the complexity of checking the considered equivalence relations. Under benign window operators, the complexity is not worse than for logic programs; only in some cases the complexity does increase.

To the best of our knowledge, no similar work on equivalence notions in stream reasoning exists to date. Our results thus give an entry point towards optimization of expressive rule-based programs for reasoning over data streams.

LARS

We will gradually introduce the main concepts of LARS [Beck et al., 2015b], a recent logic-based framework for analyzing and expressing reasoning over streams. Where appropriate, we give only informal descriptions. We assume that the reader is familiar with ASP [Gelfond and Lifschitz, 1991; Brewka et al., 2011]; for equivalence relations between ASP programs, we refer to [Lifschitz et al., 2001; Eiter et al., 2007b].

We consider propositional (ground) LARS. Throughout, A denotes the set of atoms, which is partitioned into extensional (input) atoms AE and intensional (derived) atoms AI .

Definition 1 (Stream) A stream S = (T↪ υ) consists of a timeline T, which is a closed interval T ✓ N of integers called time points, and an evaluation function υ : N 7! 2A.

Intuitively, a stream S associates with each time point a set of atoms. We call S a data stream, if it contains only extensional atoms. To cope with the amount of data, one usually considers only recent atoms. Let S = (T↪ υ) and S0 = (T 0 ↪ υ0 ) be two streams such that S0 ✓ S, i.e., T 0 ✓ T and υ0 (t0 ) ✓ υ(t0 ) for all t0 2 T 0 . Then S0 is called a substream or a window of S.

Definition 2 (Window function) Any (computable) function w that returns, given a stream S = (T↪ υ) and a time point t 2 T , a substream S0 of S is called a window function.

Important are time-based window functions, which select all atoms appearing in last n time points, and tuple-based window functions, which select a fixed number of latest tuples.

Example 1 Figure 1 depicts a stream S = ([0↪ 4]↪ υ) where υ = ¶0 7! ¶a♦↪ 1 7! ¶a♦↪ 3 7! ¶b♦↪ 4 7! ¶a↪ c♦♦, and the application of the time-based window function w on S that looks back two time units from time point t = 3. This returns the substream S0 = ([1↪ 3]↪ ¶1 7! ¶a♦↪ 3 7! ¶b♦♦). ⌅

Window operators ⊞. Window functions can be accessed in formulas by window operators. For every window function w, employing an expression ⊞w ↵ has the effect that ↵ is evaluated on the substream of the data stream delivered by w.

Definition 3 (Formulas) The set F of formulas is given as follows, where a 2 A is an atom, t 2 N, w a window function.

The precedence of operators 3↪2↪@t and ⊞w is as for ≻; e.g., ≻ ⊞w 3a ^ @tb ! c = ((≻ ⊞w 3a) ^ (@tb)) ! c.

Definition 4 (Structure) A structure is any tuple M = hS↪W↪ Bi where S is a stream, W is a set of window functions and B ✓ A is the background data of M.

Definition 5 (LARS Entailment) Let M = hS↪W↪ Bi be a structure, S = (T↪ υ) and t 2 T. The LARS-entailment relation ⊩ between (M↪ t) and formulas is defined as follows. Let a 2 A be an atom, and let ↵↪ β 2 F be formulas. Then,

M↪ t ⊩ ≻↵ iff M↪ t 1 ↵↪

M↪ t ⊩ a iff a 2 υ(t) or a 2 B↪

M↪ t ⊩ ↵^ β iff M↪ t ⊩ ↵ and M↪ t ⊩ β↪

M↪ t ⊩ 3↵ iff M↪ t0 ⊩ ↵ for some t0 2 T↪

M↪ t ⊩ ↵! β iff M↪ t 1 ↵ or M↪ t ⊩ β↪

M↪ t ⊩ 2↵ iff M↪ t0 ⊩ ↵ for all t0 2 T↪

M↪ t ⊩ ⊞w ↵ iff M 0 ↪ t ⊩ ↵↪ where M 0 = hS0 ↪W↪ Bi

M↪ t ⊩ @t0↵ iff M↪ t0 ⊩ ↵ and t0 2 T↪

such that S0 = w(S↪ t)▷

Throughout, we assume that A contains two special atoms >/? that are true/false in every structure.

In the sequel, ⊞n stands for a time-based window operator that takes the last n time points and all data there.

Example 2 Let S = ([0↪ 3]↪ ¶07!¶a♦↪ 17!¶a♦↪ 37!¶b↪ x♦♦) be a stream and let ' = ⊞23a ^≻y ! x be a LARS formula. Consider the structure M = hS↪ ¶⊞2 ♦↪ ;i. We have that M↪ 3 ⊩ ⊞23a ^≻y. Indeed, since y ◁2 υ(3), it follows that M↪ 3 ⊩ ≻y. Furthermore, M↪ 3 ⊩ ⊞23a since M 0 ↪ 1 ⊩ a, where M 0 is obtained by replacing S with S0 = ([1↪ 3]↪ ¶1 7! ¶a♦↪ 3 7! ¶b↪ x♦♦), i.e., the result of applying the time-based window of size 2 on S at time point 3. Furthermore, M↪ 3 ⊩ x as x 2 υ(3); thus M↪ 3 ⊩ ' holds. ⌅ We now turn to LARS programs that build on formulas.

LARS Programs

Syntax. LARS programs [Beck et al., 2015b] are sets of rules

where ↵↪ β1↪ ▷ ▷ ▷ ↪ βn 2 F are formulas, and ↵ contains only intensional atoms; B(r) = ¶βi ♣ 1  i  n♦ is the body of r.

For instance, rule x ⊞23a↪ not y amounts to ' of Ex. 2. Semantics. Let D = (T↪ vD) be a data stream. We call a stream I = (T↪ υ) ◆D an interpretation stream for D, if it coincides with D on AE , i.e., for every a 2 AE and t 2 T, a 2 υ(t) only if a 2 υD(t); the structure M = hI↪W↪ Bi is then an interpretation for D. Throughout, we assume W (implicit by the considered programs) and B are fixed, and are thus also omitted. For a rule r of the form (1), we define

Let t 2 T. We say M satisfies rule r at t, denoted by M↪ t ♣= r, if M↪ t ⊩ ¯ β(r) !↵. In this case, M is a model of r (for D) at t. The notions of satisfaction and models carry over to programs as usual, i.e., M↪ t ♣= P, if M↪ t ♣= r for all r 2 P. Moreover, M is a minimal model of P (for D at t) if there does not exist an M 0 = hI 0 ↪W↪ Bi s.t. M 0 ↪ t ♣= P where I 0 = (T↪ υ0 ) ⇢ I. Note that smaller models must have the same timeline.

Definition 6 (Answer Stream) Let P be a program, D = (T↪ υ) be a data stream and t 2 T. An interpretation stream I for D is an answer stream of P for D at t, if M = hI↪W↪ Bi is a minimal model of the (FLP)-reduct

AS(P↪D↪ t) denotes the set of all such answer streams I.

Example 3 (cont'd) Consider the stream D = ([0↪ 3]↪ υ), where υ=¶0 7! ¶a♦↪ 1 7! ¶a♦↪ 3 7! ¶b♦♦ and a program P , given by the following rules: x ⊞23a↪ not y and y ⊞23a↪ notx. By taking W = ¶⊞2 ♦ and B = ;, we get at t = 3 two answer streams I x and I y which augment D by adding x and y to υ(3), respectively. For instance, the reduct P M↪3 , where M = hI x ↪W↪ Bi, contains only the first rule. We have M↪ 3 ♣= P M↪3 , since M↪ 3 ⊩ ⊞23a ^ ≻y ! x. Towards a smaller model, we can not remove a, as a is extensional (i.e., in the data stream), nor x because this would invalidate the implication. The argument for I y is analogous. ⌅

Bi-Structural LARS Evaluation

We now define an extended variant of LARS semantics, where formulas (resp. programs) are evaluated on a pair of streams (SL↪ SR) at the same time. We will later consider a substream relation SL ✓ SR on according models similar to the logic of Here-and-There [Heyting, 1930] which was extensively studied in relation to equivalence notions for ASP.

In the sequel, we use the following notation. Given streams SL = (T↪ υL) and SR = (T↪ υR), we call S = (SL↪ SR) a bi-stream and M= hS↪W↪ Bi a bi-structure, where W are window functions and B is background data as in LARS. We call SL the left-stream and SR the right-stream. Moreover, L = hSL↪ W↪ Bi and R = hSR↪ W↪ Bi denote the underlying LARS structures of M; the left-structure and the rightstructure, respectively.

Definition 7 (Bi-LARS Entailment) Let M = hS↪ W↪ Bi be as above and let t 2 T . The Bi-LARS-entailment relation ⊩ between (M↪ t↪ w) for worlds w 2 ¶L↪ R♦ and formulas is defined as follows (where ↵↪ β 2 F are formulas):

M↪ t↪w ⊩ ↵^ β iff M↪ t↪w ⊩ ↵ and M↪ t↪w ⊩ β↪

M↪ t↪ w ⊩ a iff a 2 υw(t) or a 2 B↪ for a 2 A,

M↪ t↪w ⊩ 3↵ iff M↪ t0 ↪w ⊩ ↵ for some t0 2 T↪

M↪ t↪w ⊩ @t0↵ iff M↪ t0 ↪w ⊩ ↵ and t0 2 T↪

M↪ t↪w ⊩ 2↵ iff M↪ t0 ↪w ⊩ ↵ for all t0 2 T↪

M↪ t↪ L ⊩ ↵! β iff M↪ t↪ L 1 ↵ or M↪ t↪ L ⊩ β↪

and M↪ t↪ R ⊩ ↵ ! β

M↪ t↪ R ⊩ ⊞w ↵ iff R↪ t ⊩ ⊞w ↵▷

Moreover, we define M↪ t ⊩ ↵ iff M↪ t↪ L ⊩ ↵.

Similarly as for LARS, M↪ t ⊩ >/? always/never holds. If M↪ t ⊩ ↵ holds, we say that M entails ↵ at time t and we then call M a bi-model of ↵ at time t. Entailment and the notion of a model are extended to sets of formulas as usual.

Observe that for the connectives/operators ^, 3, 2, @t0 and !, Bi-LARS has a recursive definition, while the evaluation for ≻ and ⊞ branches into separate evaluation in the underlying LARS structures. This is required with the aim to provide semantic characterizations of equivalences for a large class of LARS programs. However, we will also later examine when a recursive definition is possible. Note that in general, entailment in both LARS structures does not imply entailment in the bi-structure. For instance, consider the bistream S = (SL↪ SR), where SL = ([0↪ 0]↪ ¶0 7! ¶a♦♦) and SR = ([0↪ 0]↪ ¶0 7! ;♦), and take ↵ = a ! ((a ! a) ! a). We have L↪ 0 ⊩ ↵ and R↪ 0 ⊩ ↵, but M↪ 0 1 ↵.

The following lemma, which is immediate fromDef. 7, intuitively states that evaluation for the right-stream is independent of the left-stream.

We call a bi-stream (SL↪ SR) total, if SL = SR. Restricting the study to total interpretations, Bi-LARS-satisfaction clearly collapses to LARS-satisfaction.

Proposition 1 Let M = hS↪W↪ Bi be a structure, where S = (T↪ υ) and M= hS↪W↪ Bi, where S = (S↪ S), t 2 T and ↵ be a formula. Then, M↪ t ⊩ ↵ iff M↪ t ⊩ ↵▷

Bi-LARS Semantics for LARS programs. Entailment in Bi-LARS is extended from formulas to programs analogously as for LARS. Let D = (T↪ υ) be a data stream, t 2 T and let P be a program. We say a bi-structure M satisfies a rule r of form (1) at t, denoted by M↪ t ♣= r ↪ if M↪ t ⊩ ¯ β(r) ! ↵. In this case, M is a (bi-)model of r (for D at t). Similarly as for LARS, M↪ t ♣= P↪ if M↪ t ♣= r for all r 2 P. We then call M a (bi-)model of P (for D at t).

Plain LARS and LARSbi. In [Beck et al., 2015a], a practical fragment of LARS was introduced. We call this fragment plain LARS, which restricts the rule head to be of form a or @ta, where a is an atom, and body formulas to be extended atoms, i.e., expressions of the grammar

While plain LARS serves as guiding fragment, we will obtain our results for the following broad class of LARS programs.

Definition 8 (Fbi, LARSbi) By Fbi we denote the class of LARS formulas without !, where 3 only occurs in the scope of ≻ or ⊞. Moreover, LARSbi is the class of LARS programs where all formulas ↵↪ βi in rules (1) are in Fbi.

In the sequel, programs are tacitly assumed to be in LARSbi.

Note that the FLP-semantics of answer streams (Def. 6) is defined non-recursively. Still, we can capture it by branching in Bi-LARS evaluation of ≻ and ⊞ into separate LARS evaluations for left and right, due to the following central property.

Proposition 2 Let M= hS↪W↪ Bi be such that SL ✓ SR and let ↵ 2 Fbi. Then, M↪ t ⊩ ↵ iff SL↪ t ⊩ ↵ and SR↪ t ⊩ ↵.

The proof is by induction on the structure of formulas. The relation SL ✓ SR naturally arises with minimality checking of models, where intuitively SR is a model M of a program P at time t and SL is a candidate model of the reduct P M↪t . It establishes a semantic connection between left and right, which can be exploited to conclude that M↪ t ⊩ ↵ implies SL↪ t ⊩ ↵; for arbitrary formulas, this fails. E.g., consider SL = ([0↪ 0]↪ ¶0 7! ;♦), SR = ([0↪ 0]↪ ¶0 7! ¶a♦♦), and ↵ = ≻a ! b; then M↪ 0 ⊩ ↵ but L↪ 0 1 ↵. Similarly, excluding 3' is necessary to ensure that the only-if direction of Proposition 2 holds.

The following result now captures the essence of the reduct-based semantics: the left-structure must satisfy each rule whose body is true in the model given by the rightstructure. The proof is based on [Lifschitz et al., 2001].

Theorem 1 For any M=hS↪W↪ Bi s.t. SL✓SR, time t and program P , we haveM↪ t ♣= P iff R↪ t ♣= P and L↪ t ♣= P R↪t .

We are now going to characterize answer streams similarly as in [Lifschitz et al., 2001] and [Turner, 2001], by capturing the minimality condition in terms of bi-equilibrium models.

Definition 9 (bi-EquilibriumModel) Let M = hI↪W↪ Bi be a structure. We say M = h(I ↪ I)↪ W↪ Bi is a bi-equilibrium model of a program P for data streamD at time t, if

• (i) M↪ t ♣= P, and
• (ii) M0 ↪ t 6♣= P, for each M0 = h(I 0 ↪ I)↪W↪ Bi such that D ✓ I 0 ⇢ I and I 0 = (T↪ υ0 ).

We obtain the next theorem from Def. 6, Prop. 1 and Thm. 1.

Theorem 2 Let M = hI↪W↪ Bi be a structure s.t. I is an interpretation stream for D at t. Then, I 2 AS(P↪D↪ t) iff M = h(I↪ I)↪ W↪ Bi is a bi-equilibrium model.

This allows us to characterize program equivalences which include non-trivial window operators, as will be shown next.

Equivalence

We now introduce equivalence notions for stream reasoning in our setting. Given a timeline T , we say a set A of @-atoms, i.e., extended atoms of form @ta, have time references in T, if ¶t ♣ @ta 2 A♦ ✓ T . This notion carries over naturally for programs P, i.e., if ¶t ♣ @ta occurs in P♦ ✓ T.

Definition 10 (Equivalence Notions) Let T be a timeline, D = (T↪ υ) be a data stream, and let t 2 T be a time point. We say two LARS programs P and Q are

• (i) (ordinary) equivalent (for D at t), denoted by P ⌘ Q, if AS(P↪ D↪ t) = AS(Q↪ D↪ t);
• (ii) strongly equivalent (for D at t), denoted by P ⌘s Q, if AS(P [R↪D↪ t) = AS(Q[R↪D↪ t) for all LARS programs R with time references in T ;
• (iii) uniform equivalent (for D at t), denoted by P ⌘u Q, if AS(P [F↪D↪ t) = AS(Q[F↪D↪ t) for sets F of @- atoms with time references in T ;
• (iv) data equivalent (for D at t), denoted by P ⌘d Q, if AS(P↪D[S↪ t) = AS(Q↪D[S↪ t) for all data streams S with timeline T .

Intuitively, (i)-(iii) can be seen as extensions of corresponding notions in ASP [Lifschitz et al., 2001; Eiter et al., 2007b] to the LARS setting. In particular, these notions emerge if the programs P and Q are ordinary logic programs (without windows and temporal operators) and we consider a void data stream D = ([0↪ 0]↪ υ) at time point 0. On the other hand, data equivalence is well-known in the database area and plays an important role in stream reasoning, as the possibility to drop data is crucial to gain performance. The addition of all rules resp. facts accounts for the nonmonotonic nature of answer streams, as replacing ordinary equivalent programs P and Q in the context of other rules R might change answer streams.

We now characterize strong and uniform equivalence by means of bi-models. To this end, from now we tacitly restrict to bi-structures M= hS↪W↪ Bi such that SL ✓ SR. By bi(P), we denote the set of all respective bi-models of a program P (where D and t are implicit).

Theorem 3 (Strong Equivalence) Let D = (T↪ υ) be a data stream, t 2 T, and let P and Q be LARSbi programs. Then, P ⌘s Q (for D at t) iff bi(P) = bi(Q) (for D at t).

Furthermore, we also characterize uniform equivalence in terms of bi-entailment. Let MLR = h(SL↪ SR)↪W↪ Bi and MRR = h(SR↪ SR)↪ W↪ Bi.

• (i) for eachMRR, MRR 2 bi(P) iff MRR 2 bi(Q), and

Theorem 4 (Uniform Equivalence) P ⌘u Q iff

• (ii) for each MLR, where SL ⇢ SR, MLR 2 bi(P) (resp. MLR 2 bi(Q)) iff M2 bi(Q) (resp. M2 bi(P)) for some M = h(S↪ SR)↪ W↪ Bi s.t. SL ✓ S ⇢ SR.

The proofs of Theorems 3 and 4 are abstracted from those for answer set programs (cf. [Lifschitz et al., 2001], resp. [Eiter and Fink, 2003]) and exploit the following key properties: (1) the reduct of the union of two programs is the union of their reducts (2) the reduct of a set of atoms F is F itself, (3) an atom evaluates to true iff it is in the interpretation stream, and (4) a structure entails the union of two programs iff it entails each program separately.

In a similar way, also relativised uniform equivalence [Woltran, 2004], denoted by P ⌘Au Q, can be characterized, i.e., the condition that AS(P [F↪D↪ t) = AS(Q[F↪D↪ t) for all facts F ✓ A, where A is a set of @-atoms. Notably, data equivalence amounts to a special case of relativized uniform equivalence: Consider for D = (T↪ υ) the set

Recall that plain LARS allows only intensional atoms and @-atoms with intensional atoms in rule heads. However, this is not the case for all LARSbi programs, which also allow window operators in rule heads.

LARS Here-&-There and Monotone Windows

In Definition 7, the semantics of the window operator ⊞ was defined in Bi-LARS by straight branching into separate evaluation of the left and the right stream. Consider the following alternative ⊞ semantics.

Definition 11 (Recursive ⊞) We define the following alternative ⊞ semantics for Bi-LARS. Let w 2 ¶L↪ R♦.

This recursive variant may in general break the connection between left and right, i.e., the relation SL ✓ SR.

Example 4 Consider streams SL = ([0↪ 4]↪ υL) and SR = ([0↪ 4]↪ υR) as depicted in Figure 2, where SL ⇢ SR. Applying a tuple-based window operator with size 3 at t = 4 returns S0L = ([1↪ 4]↪ ¶1 7! ¶a♦↪ 3 7! ¶b♦↪ 4 7! ¶a♦♦) as substream of SL, and S0R = ([3↪ 4]↪ ¶3 7! ¶b♦↪ 4 7! ¶a↪ c♦♦ for SR. We observe that S0L 6✓ S0R, i.e. the substream relation breaks. ⌅

In Example 4, the window is nonmonotonic in the sense that by increasing the input stream, atoms may disappear from the output. When excluding such nonmonotonic windows, the recursive version for ⊞ semantics may be equally used.

Definition 12 We call a window function w monotone, if for every streams S1 = (T1↪ υ1) and S2 = (T2↪ υ2) it holds that

S1 ✓ S2 implies w(S1↪ t) ✓ w(S2↪ t) for all t 2 T1↪

i.e., w preserves substreams. If T1 =T2, this extends to timelines, i.e., w(Si↪ t)=(T 0 i ↪ υ0i ) implies T 01 =T 02 for all t 2 T1.

Likewise, we call a window operator ⊞w monotone if the underlying window function w is monotone. E.g., time-based window operators just filter data and thus have this property.

Proposition 3 For plain LARS with monotone windows, the window semantics of Def. 7 and Def. 11 coincide.

Using Def. 11 for a variant of Bi-LARS on monotone windows can be seen as an extension of Here-and-There [Heyting, 1930] underlying Equilibrium Logic [Pearce, 2006].

Definition 13 (HT-entailment) HT-entailment is defined as variant of Bi-LARS entailment (Def. 7), using instead Def. 11 for the ⊞ semantics and ≻↵ := ↵ ! ? for negation.

Based on HT-entailment, we obtain a conservative extension of Pearce's Equilibrium Logic for LARS with monotone windows, which treats nested implications intuitionistically, and thus different from FLP-based semantics. Under limited nesting of negation, the two semantics actually coincide; e.g., for the following class of formulas/programs:

Definition 14 (FHT, LARSHT) By FHT we denote the class of LARS formulas where (i) each ⊞ is monotone, (ii) each subformula ↵! β expresses negation (i.e., ≻↵, as β = ?), and (iii) no negation occurs within the scope of 3 or another negation. By LARSHT we denote the class of LARS programs where all formulas ↵↪ βi in rules (1) are in FHT.

Note that nested negation must be excluded, as e.g. the rule a ≻≻a has the equilibrium models (;↪ ;) and (¶a♦↪ ¶a♦). Only the first one amounts to an FLP-answer set.

With an inductive argument, one can show that the central property of Prop. 2 carries over to formulas in FHT under HT-entailment. This allows one to establish the characterization in Theorem 1 for this setting. Thus, for LARSHT programs, FLP-based answers streams and HT-equilibrium models coincide, and the equivalence notions can equally be characterized by HT-entailment.

Theorem 5 (LARS Here-and-There) Theorems 1-4 also hold for LARSHT programs under HT-entailment.

Note that LARSHT includes plain LARS programs with monotone windows.

Computational Complexity

As regards the complexity of equivalence checking, different scenarios emerge. We focus here on deciding P ⌘e Q for an equivalence notion e, where the data stream D, the programs P , Q and a (query) time point t are given.

More general is to request equivalence at multiple or each time point t over D, and/or to consider evolutions of the data streamD. For a small (polynomial) horizon around t, i.e., an interval [t0↪ t1] such that t0 tt1 and ♣t1 -t0♣ is polynomially bounded, this essentially reduces to polynomially many such questions. This is in line with the view that stream reasoning may lose information, i.e., query results over the full history and the reduced data may be different.

Setup. We adopt the assumptions in [Beck et al., 2015b], in particular that relevant atoms are confined to A, the background B and the window functions W are fixed and can be polynomially evaluated. Then, both model checking and satisfiability testing for arbitrary LARS formulas is PSPACEcomplete [Beck et al., 2015b], as answer stream checking and deciding answer stream existence. However, we note:

Lemma 2 (cf. [Beck et al., 2015b]) For LARS formulas ↵ without nested windows, deciding M↪ t ⊩ ↵ is polynomial and deciding satisfiability of ↵ wrt. a timeline T and time point t is NP-complete. The same holds for window nesting depth bounded by a constant k.

In practice, bounded nesting of windows will apply; thus we adopt this assumption. As an easy consequence, we get:

Corollary 1 Given a bi-structure M, a time point t, and a (window-bounded) LARS formula ↵, deciding M↪ t ⊩ ↵ is feasible in polynomial time.

Besides plain LARS, we study here the following fragment.

Stratified LARS programs extend the usual notion of stratified logic programs by allowing constraints and building the dependency graph as follows. Formulas of the form @t0a and ⊞↵ are the nodes, where a 2 A, t0 is a time point, and ⊞↵ occurs only in a rule body as βi. Relative to D and t, atoms a are identified with @ta, and edges are added in the graph as usual, where also an (negation-style) edge from ⊞↵ to every @t0a is added such that the value of ⊞↵ at t depends on the one of a at t0 . As this depends on the semantics of the window operator, for a simple syntactic criterion we assume here that this is only the atom a in ↵; e.g. time-based windows satisfy this property. Stratified LARS programs are stream-stratified LARS programs in [Beck et al., 2015a] and can be evaluated bottom up using an iterative fixed-point computation to obtain an answer stream (which exists if no constraint is violated).

Complexity results. Our results are compactly summarized in Table 1. Besides the program classes, we distinguish between only monotonic and possible nonmonotonic windows.

As it appears, the complexities of the various problems ranges from P to ⇧p2 . In most of the cases, the upper bound is an immediate or easy consequence of Lemma 2 and the characterizations of answer streams and equivalences from above. In particular, deciding strong equivalence is always in coNP, while deciding answer stream existence resp. refuting uniform or data equivalence can be done in nondeterministic polynomial time using an NP oracle to verify a guess for an answer stream resp. counterexample to equivalence.

For stratified programs, the fixed-point computation of the unique answer stream is feasible in polynomial time; this explains the P-entries. Fixed-point computation is also feasible on the reduct P M↪t of a plain LARS program with monotone windows to check minimality of M, as here negative literals can be dropped in P M↪t . This explains why answer stream existence / ordinary equivalence is in NP/ coNP.

As for the lower bounds, deciding P ⌘u Q is reducible to deciding P ⌘d Q. Indeed, given ordinary logic programs P and Q on A, let Ad be a copy of A and let Pd = P [ Rd and Qd = Q[Rd, where Rd = ¶a ad ♣ a 2 A♦. Then, P and Q are uniformly equivalent (wrt. A) iff Pd and Qd are data equivalent wrt. Ad. This can be extended to LARS programs (where window operators possibly must be adapted), using rules @ta @tad for the time points t. Thus, for the hardness results, it is remains to consider uniform equivalence.

Many of the lower bounds are then inherited from the complexity of the respective notions for ordinary logic programs [Eiter et al., 2007b]. In particular, plain LARS programs subsume normal logic programs, for which deciding answer stream existence is NP-complete, while deciding uniform resp. strong equivalence is coNP-complete (even for acyclic, i.e., recursion-free programs [Eiter et al., 2007a]).

What remains are the ⌃p2 -hardness of answer stream existence and ⇧p2 -hardness of ordinary equivalence and uniform equivalence, respectively, for plain LARS programs with nonmonotonic windows. These results are shown by reductions of evaluating QBFs of the form 9X8YE(X↪ Y ), resp. 8X9Y E(X↪ Y ). Actually, the proofs establish them for plain programs without negation (i.e., for Horn programs); they hinge on techniques in [Eiter and Gottlob, 1995] and [Eiter and Fink, 2003] for the respective problems on ordinary disjunctive logic programs, but must compensate the lack of negation and of disjunction. We can emulate negation using nonmonotonic windows by the following construction.

Example 5 To emulate ≻a for an atom a, we create a window operator ⊞≻a with an associated window function w≻a(S↪ t) that removes da from υ(t), if a 2 υ(t), where da is a fresh atom, and otherwise leaves S unchanged. If da is a fact in a program P and thus true in every model M of P at t, we have M↪ t ⊩ ⊞≻a@tda iff M↪ t ⊩ ≻a. ⌅

Similarly we can define window operators ⊞Φ that check whether a model M satisfies at t a polynomial-time property Φ; e.g. whether a truth assignment given in υ(t) satisfies a Boolean formula. We use this to evaluate E(X↪ Y ) using window atoms. However, for space reasons, we must omit details.

Notably, the property Φ may also be deciding M↪ t ⊩ ⊞' where the window nesting in ⊞' is bounded (cf. Lemma 2); the latter can be used to compile complex formulas inside window operators away, and shows that plain LARS with nonmonotonic windows is quite powerful.

Related Work and Conclusion

Lifschitz et al. [2001] introduced strong equivalence of logic programs under ASP semantics and showed that it coincides with equivalence in Here-and-There logic. Inspired by this, Eiter et al. [2007b] characterized uniform and relativized notions of equivalence in ASP in terms of HT-interpretations (H↪ T). We generalize this to the LARS framework with bistructures (SL↪ SR) containing pairs of streams.

As regards optimization in stream reasoning, to our knowledge not much foundational work exists. Typically, the interest is concentrated on dealing with evolving data, and to develop incremental evaluation techniques, e.g., [Motik et al., 2015; Ren and Pan, 2011; Gebser et al., 2011; Barbieri et al., 2010a; Beck et al., 2015a]. In the context of data processing, [Arasu et al., 2006] studied query equivalence for the Continuous Query Language (CQL), but at a very elementary level. As in essence CQL can be captured by LARS programs [Beck et al., 2015b], results on LARS equivalence may be fruitfully applied in this context as well.

Naturally, stream reasoning relates to temporal reasoning; in [Cabalar and Vega, 2007], nonmonotonic Linear Temporal Equilibrium Logic (TEL) was presented as an extension of Pearce's Equilibrium Logic [2006] to linear time logic (LTL), defining temporal stable models over infinite structures. Notably, strong equivalence for TEL theories amounts to equivalence in the underlying Temporal Here-and-There logic [Aguado et al., 2008; Cabalar and Di´eguez, 2014]. However, TEL differs from LARS in several respects. LARS aims primarily at finite (single-path) structures, and the notion of window, which requires to go beyond the HT setting, has no counterpart in TEL. Furthermore, the temporal operators in LARS are more geared to access of data in windows in practice. Also the complexity of TEL, extensively studied in [Bozzelli and Pearce, 2015], and LARS is different: model checking for (unbounded) LARS formulas resp. programs is PSPACE-complete, while for LTL underlying TEL it is polynomial in our finite path setting (in fact, efficiently parallelizable [Kuhtz and Finkbeiner, 2009]).

Outlook. In future work, our studies can be extended in several directions. Apart from other notions of equivalence, additional program classes are of practical relevance. In particular, by confining to widely used time-based and tuple-based window operators one might exploit more specific properties than by the distinction of monotone vs. nonmonotone ones. Related to this is identifying maximal (relative to some criteria) fragments where Here-and-There semantics coincides with Bi-LARS, which is tailored for FLP. Furthermore, one might introduce window operators to the more expressive temporal equilibrium logic. Apart from potential extensions of Bi-LARS to capture according semantics, combining nonmonotonic temporal reasoning with features to drop data is an intriguing issue. Moreover, besides semantic also syntactic criteria for program equivalence are practically important. In particular, finding normal forms in relation to prominent window operators will directly support the optimization of programs for reasoning over streaming data.

Acknowledgments. We thank Andreas Humenberger for his assistance in the early phase of this work.