# equivalent_stream_reasoning_programs__ec2be5da.pdf

Equivalent Stream Reasoning Programs

Harald Beck and Minh Dao-Tran and Thomas Eiter Institute of Information Systems, Vienna University of Technology

Favoritenstraße 9-11, A-1040 Vienna, Austria

{beck,dao,eiter}@kr.tuwien.ac.at

The emerging research field of stream reasoning faces the challenging trade-off between expressiveness of query programs and data throughput. For optimizing programs methods are needed to tell whether two programs are equivalent. Towards providing practical reasoning techniques on streams, we consider LARS programs, which is a powerful extension of Answer Set Programming (ASP) for stream reasoning that supports windows on streams for discarding information. We define different notions of equivalence between such programs and give semantic characterizations in terms of models. We show how a practically relevant fragment can be alternatively captured using Here-and-There models, yielding an extension of equilibrium semantics of ASP to this class of programs. Finally, we characterize the computational complexity of deciding the considered equivalence relations.

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

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-16)

Figure 1: Time-based window of size 2 at t = 3

thus give an entry point towards optimization of expressive rule-based programs for reasoning over data streams.

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.

::= a | | | ! | 3 | 2 | @t | w

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

Definition 4 (Structure) A structure is any tuple M = h S, 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 = h S, 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 a iff a 2 υ(t) or a 2 B, M, t iff M, t 1 , M, t β iff M, t and M, t β, M, t ! β iff M, t 1 or M, t β, M, t 3 iff M, t0 for some t0 2 T, M, t 2 iff M, t0 for all t0 2 T, M, t @t0 iff M, t0 and t0 2 T, M, t w iff M 0, t , where M 0 = h S0, W, Bi 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 = h S, { 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

β1, . . . , βm, not βm+1, . . . , not βn , (1) 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, v D) 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 = h I, 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

β(r) = β1 βm βm+1 βn . (2) 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 = h I0, W, Bi s.t. M 0, t |= P where I0 = (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 = h I, W, Bi is a minimal model of the (FLP)-reduct

P M,t = {r 2 P | M, t |= β(r)} ; 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, not x. By taking W = { 2} and B = ;, we get at t = 3 two answer streams Ix and Iy which augment D by adding x and y to υ(3), respectively. For instance, the reduct P M,3, where M = h Ix, 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 Iy 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 = h S, 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 = h SL, W, Bi and R = h SR, W, Bi denote the underlying LARS structures of M; the left-structure and the rightstructure, respectively.

Definition 7 (Bi-LARS Entailment) Let M = h S, 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 a iff a 2 υw(t) or a 2 B, for a 2 A, M, t, w β iff M, t, w and M, t, w β, M, t, w 3 iff M, t0, w for some t0 2 T, M, t, w 2 iff M, t0, w for all t0 2 T, M, t, w @t0 iff M, t0, w and t0 2 T, M, t, L ! β iff M, t, L 1 or M, t, L β, and M, t, R ! β M, t, R ! β iff M, t, R 1 or M, t, R β, M, t, L iff L, t and R, t M, t, R iff R, t M, t, L w iff L, t w and R, t w , 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 from Def. 7, intuitively states that evaluation for the right-stream is independent of the left-stream. Lemma 1 M, t, R iff R, t . 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 = h S, W, Bi be a structure, where S = (T, υ) and M = h S, 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

a | @ta | @ta | 3a | 2a . (3) 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 = h S, 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=h S, W, Bi s.t. SL SR, time t and program P, we have M, 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-Equilibrium Model) Let M = h I, W, Bi be a structure. We say M = h(I, I), W, Bi is a bi-equilibrium model of a program P for data stream D at time t, if

(i) M, t |= P, and (ii) M0, t 6|= P, for each M0 = h(I0, I), W, Bi such that

D I0 I and I0 = (T, υ0). We obtain the next theorem from Def. 6, Prop. 1 and Thm. 1. Theorem 2 Let M = h I, 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 = h S, 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).

0 0 1 1 2 2 3 3 4 4

0 0 1 1 2 2 3 3 4 4

Figure 2: Tuple-based windows of size 3 at t = 4.

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. Theorem 4 (Uniform Equivalence) P u Q iff

(i) for each MRR, MRR 2 bi(P) iff MRR 2 bi(Q), and (ii) for each MLR, where SL SR, MLR 2 bi(P) (resp.

MLR 2 bi(Q)) iff M 2 bi(Q) (resp. M 2 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 A

u 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 A = {@ta | a 2 AE and t 2 T}. Then,

P d Q iff P A

u Q. 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}.

M, t, w w iff M0, t, w ,

where M0 = h(S0

R), W, Bi and S0

w = w(Sw, t). 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 S0

L = ([1, 4], {1 7! {a}, 3 7! {b}, 4 7! {a}}) as substream of SL, and S0

R = ([3, 4], {3 7! {b}, 4 7! {a, c}} for SR. We observe that S0

R, 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) implies T 0

2 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

stream D. 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 p

2. 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 co NP, 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

AS(P, D, t)6=; / P o Q P e Q, e = s / u / d mon nonmon

plain LARS NP / co NP p

2 co NP/ co NP / co NP co NP/ p

2 stratified P / P P / P co NP / co NP / co NP co NP / co NP / co NP

Table 1: Complexity of consistency and equivalence checking for D at t (entries denote completeness results)

can be dropped in P M,t. This explains why answer stream existence / ordinary equivalence is in NP/ co NP.

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 co NP-complete (even for acyclic, i.e., recursion-free programs [Eiter et al., 2007a]).

What remains are the p

2-hardness of answer stream existence and p

2-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 9X8Y E(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.

References [Aguado et al., 2008] Felicidad Aguado, Pedro Cabalar, Gilberto P erez, and Concepci on Vidal. Strongly equivalent temporal logic programs. In JELIA, 2008. [Arasu et al., 2006] Arvind Arasu, Shivnath Babu, and Jen-

nifer Widom. The CQL continuous query language: semantic foundations and query execution. VLDB J., 15(2):121 142, 2006. [Barbieri et al., 2010a] Davide Francesco Barbieri, Daniele

Braga, Stefano Ceri, Emanuele Della Valle, and Michael Grossniklaus. Incremental reasoning on streams and rich background knowledge. In ESWC 2010, pages 1 15, 2010. [Barbieri et al., 2010b] Davide Francesco Barbieri, Daniele

Braga, Stefano Ceri, Emanuele Della Valle, and Michael Grossniklaus. Querying RDF streams with C-SPARQL. SIGMOD Record, 39(1):20 26, 2010. [Beck et al., 2015a] Harald Beck, Minh Dao-Tran, and Thomas Eiter. Answer update for rule-based stream reasoning. In IJCAI, 2015. [Beck et al., 2015b] Harald Beck, Minh Dao-Tran, Thomas

Eiter, and Michael Fink. LARS: A logic-based framework for analyzing reasoning over streams. In AAAI, 2015. [Bozzelli and Pearce, 2015] Laura Bozzelli and David Pearce. On the complexity of temporal equilibrium logic. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 645 656. IEEE, 2015. [Brewka et al., 2011] Gerd Brewka, Thomas Eiter, and Miroslaw Truszczy nski. Answer set programming at a glance. Communications of the ACM, 54(12):92 103, 2011. [Cabalar and Di eguez, 2014] Pedro Cabalar and Mart ın Di eguez. Strong equivalence of non-monotonic temporal theories. In KR, 2014. [Cabalar and Vega, 2007] Pedro Cabalar and Gilberto P erez

Vega. Temporal equilibrium logic: A first approach. In Computer Aided Systems Theory - EUROCAST 2007, pages 241 248, 2007. [Do et al., 2011] Thang M. Do, Seng Wai Loke, and Fei Liu.

Answer set programming for stream reasoning. In AI, pages 104 109, 2011. [Eiter and Fink, 2003] Thomas Eiter and Michael Fink. Uni-

form equivalence of logic programs under the stable model semantics. In ICLP, 2003. [Eiter and Gottlob, 1995] T. Eiter and G. Gottlob. On the Computational Cost of Disjunctive Logic Programming: Propositional Case. Annals of Mathematics and Artificial Intelligence, 15(3/4):289 323, 1995. [Eiter et al., 2007a] T. Eiter, M. Fink, H. Tompits, and

S. Woltran. Complexity results for checking equivalence of stratified logic programs. In IJCAI, 2007. [Eiter et al., 2007b] Thomas Eiter, Michael Fink, and Stefan

Woltran. Semantical characterizations and complexity of

equivalences in answer set programming. ACM Transactions on Computational Logic, 8(3), July 2007. [Faber et al., 2004] Wolfgang Faber, Nicola Leone, and Ger-

ald Pfeifer. Recursive aggregates in disjunctive logic programs: Semantics and complexity. In JELIA, 2004. [Gebser et al., 2011] Martin Gebser, Orkunt Sabuncu, and

Torsten Schaub. An incremental answer set programming based system for finite model computation. AI Commun., 24(2):195 212, 2011. [Gebser et al., 2012] Martin Gebser, Torsten Grote, Roland

Kaminski, Philipp Obermeier, Orkunt Sabuncu, and Torsten Schaub. Stream reasoning with answer set programming. Preliminary report. In KR, 2012. [Gelfond and Lifschitz, 1991] M. Gelfond and V. Lifschitz.

Classical negation in logic programs and disjunctive databases. New Generation Computing, 9:365 385, 1991. [Heyting, 1930] Arend Heyting. Die formalen Regeln der intuitionistischen Logik. In Sitzungsberichte der preußischen Akademie der Wissenschaften. phys.-math. Klasse, pages 42 65, 57 71, 158 169, 1930. [Kuhtz and Finkbeiner, 2009] Lars Kuhtz and Bernd Finkbeiner. LTL path checking is efficiently parallelizable. In ICALP, 2009. [Lifschitz et al., 2001] Vladimir Lifschitz, David Pearce,

and Agust ın Valverde. Strongly equivalent logic programs. ACM Trans. Comput. Log., 2(4):526 541, 2001. [Motik et al., 2015] Boris Motik, Yavor Nenov, Robert Piro,

and Ian Horrocks. Incremental Update of Datalog Materialisation: The Backward/Forward Algorithm. In AAAI, 2015. [Pearce, 2006] David Pearce. Equilibrium logic. Annals of Mathematics and Artificial Intelligence, 47(1-2):3 41, 2006. [Ren and Pan, 2011] Yuan Ren and Jeff Z. Pan. Optimising

ontology stream reasoning with truth maintenance system. In CIKM, pages 831 836, 2011. [Turner, 2001] Hudson Turner. Strong equivalence for logic

programs and default theories (made easy). In LPNMR, 2001. [Woltran, 2004] Stefan Woltran. Characterizations for rela-

tivized notions of equivalence in answer set programming. In JELIA, 2004.