Answer Update for Rule-Based Stream Reasoning

1 Introduction

Stream reasoning [Della Valle et al., 2009] emerged from stream processing [Babu and Widom, 2001] to reason about information from data streams in real time, and to perform evaluation continuously in order to obtain latest results. In this way, users may be provided with live results for instant decision making, depending on data streams that often come from sensors and may be combined with other information.

This pertains to many application scenarios, such as in public transport where real-time information about current vehicle locations, together with time tables may be used to reason about expected arrival times and ensuing travel options.

Example 1 Consider Fig. 1 (a), which depicts a tram line ℓ1 and a bus line ℓ2. Kurt is on his way to station m to go to the theater, located near station s. It usually takes the same time for the tram and the bus to get fromm to s. Thus, Kurt could simply take the bus, which is expected to arrive first at m. However, he recalls that there are frequent traffic jams on the bus line. In this case, the tram could be the better option. ■

Unbounded data and high frequency of data arrival pose a challenge, especially to advanced reasoning over streams that aims to solve AI problems such as planning, monitoring, or decision making. The rule-based LARS language [Beck et al., 2015] faces this by using windows, which were introduced in stream processing as partial stream snapshots for efficient evaluation and move on the timeline in query evaluation. Window operators may select data differently from a stream, e.g. all data in a time frame or the last n tuples. LARS has an Answer Set Programming (ASP) like semantics and supports also different means for time reference.

∗This research has been supported by the Austrian Science Fund (FWF) projects P24090 and P26471.

However, while windows reduce the data volume, efficient re-evaluation of a query remains an issue. A full re-evaluation of an (expensive) query may be impractical, the more as often only part of the data may have changed and moreover the final answer (e.g., a plan or decision) remains the same.

Example 2 (cont'd) Fig. 1 (b) illustrates actual and expected arrival times of vehicles. A bus appears at station g (busG) at minute 37.2. Based on this, we can immediately conclude the expected arrival time at m (expBusM). This inference does not need to be re-evaluated after the tram appears at b. ■

It is thus desired that re-evaluation can be done incrementally and fast. For expressive (intractable) languages such as LARS, this poses a particular challenge. Aiming at a good trade-off between efficiency and expressiveness, we consider incremental re-evaluation for a class of LARS programs, that is, a new answer stream (model) is computed from the previous answer stream and the new incoming data, under a suitable management of temporal information.

Our contributions can be briefly summarized as follows.

(1) Stream-stratified programs. Towards efficient evaluation, we introduce stream stratified programs, a fragment of LARS programs that can be split along the stream flow into layers that can be evaluated sequentially, where the output of lower layers serves as input stream for the next layer.

(2) TMS extension. We extend techniques from truth maintenance systems (TMS) [Rich and Knight, 1991], which were conceived to maintain models of non-monotonic theories, to deal with the streaming and temporal aspects of LARS on top of ASP. We extend the maintenance method for justificationbased TMS [Doyle, 1979], which amount to logic programs under stable model semantics [Elkan, 1990], in two regards: (i) We introduce an extended set of atoms comprising window and temporal operators, and for temporal data management time labels to record validity information of atoms. (ii) We similarly extend central notions of consequences and affected consequences of TMS [Beierle and Kern-Isberner, 2000].

(3) Generic Windows. Our method works at a generic level, and any concrete window operator can be plugged in if certain basic functions to process incoming data, identify outdated input, and change the temporal status of atoms are available; time- and tuple-based windows have such functions, as well as typical partition-based windows.

The emerging algorithm is nontrivial and inherently involved due to the properties of temporal operators. For space reasons, we must confine to show how the method works and omit the technical details. Notably, for relevant yet less expressive settings it is much simpler.

Our results contribute to the foundations of answer maintenance in expressive stream reasoning languages; to the best of our knowledge, no similar results exist to date. The presented ideas and principles may be transferred to similar languages.

2 Preliminaries

2.1 Streams, Windows and Time Reference

We will gradually introduce the central concepts of LARS [Beck et al., 2015] tailored to the considered fragment. If appropriate, we give only informal descriptions.

Throughout, we distinguish extensional atoms AE for input data and intensional atoms AI for derived information. By A = AE ∪ AI , we denote the set of atoms.

Definition 1 (Stream) A stream S = (T, υ) consists of a timeline T , which is an interval in N, and an evaluation function υ : N ↦→ 2A. The elements t ∈ T are called time points.

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 S′ = (T ′ , υ′ ) be two streams s.t. S′ ⊆ S, i.e., T ′ ⊆ T and υ′ (t′ ) ⊆ υ(t′ ) for all t′ ∈ T ′ . Then S′ is called a window of S.

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

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

Example 3 (cont'd) To model the public transport scenario, we take a timeline T = [1, 30000] with unit 0.1 secs. For readability, we write m for minutes, i.e., T =[1, 50m]. We have the data stream D=(T, υ), where υ can be seen as a set of mappings 37.2m↦→{busG} and 39.1m↦→{tramB}. We implicitly take υ(t) = ∅ for all t ∈ T \ {37.2m, 39.1m}. Fig. 2 depicts the window S′ =(T ′ , υ) of D, where T ′ =[36.7m, 39.7m]. Obtained by applying a time-based window function with a size of 3 min (1801 time points) at time point t = 39.7m = 23820. There, a tuple-based window of size 1 would return ([39.1m, 39.7m], {39.1↦→{tramB}}). Note that D itself does not contain expected arrival times. ■

Window operators ⊞. Window functions can be accessed in formulas by window operators. That is to say, an expression ⊞α has the effect that α is evaluated on the "snapshot" of the data stream delivered by its associated window function w⊞.

By dropping information based on time, window operators specify temporal relevance. For each atom in a window, we then want to control the semantics of its temporal reference.

Time Reference. Let S = (T, υ) be a stream, a ∈ A and B ⊆ A static background data. Then, at time point t ∈ T ,

• a holds, if a ∈ υ(t) or a ∈ B;
• ✸a holds, if a holds at some time point t′ ∈ T;
• ✷a holds, if a holds at all time points t′ ∈ T; and
• @t′a holds, if t′ ∈ T and a holds at t′ .

Next, the set A+ of extended atoms is given by the grammar

where a ∈ A and t is any time point. The expressions of form ⊞ ⋆ a, where ⋆ ∈ {@t, ✸, ✷}, are the window atoms.

Example 4 (cont'd) Given D from Ex. 3, busG holds at t = 37.2m, and thus @37.2mbusG holds at any time point. Let ⊞k denote the window operator associated with a timebased window function of size k. Then, ⊞3m@37.2mbusG and ⊞3m✸busG hold at all time points t ∈ [37.2m, 40.2m]. ■

2.2 LARS Programs

We present a fragment of the formalism in [Beck et al., 2015]. Syntax. A rule r is of the form α ← β(r), where H(r) = α is the head and β(r) = β1, . . . , βj, notβj+1, . . . , notβn is the body of r. Here, α is of form a or @ta, where a ∈ AI , and each βi is either an ordinary or a window atom.

We let B(r) = B +(r)∪B -(r), where B +(r) = {βi | 1 ≤ i ≤ j} is the positive and B -(r) = {βi | j <i≤n} is the negative body or r. A (LARS) program P is a set of rules.

We say an extended atom α occurs in a program P , denoted by α ˆ∈P, if α ∈ H(r) ∪B(r) for some rule r ∈ P. We define the α-rules of P as P H (α) = {r ∈ P | H(r) = α}.

Example 5 (cont'd) Consider the program P in Figure 3. Rule (r1) says that, if within the last 3 min (⊞3m), at some time time T (@T ) a bus appeared at station g (busG) and

• (r1) @T+3mexpBusM ← ⊞3m@TbusG, on.

Figure 3: Program P , encoding the running example

the rule is activated (on) (triggered by (r3) for one 1 min upon request), then the bus is expected to arrive 3 min later at station m (@T+3mexpBusM). Rules (r4) and (r5) express a choice to take a bus or tram at station m, if both are expected to arrive within the next 5 min (⊞+5m). The bus recommendation further depends on the traffic status (not⊞3m✸jam). ■

Semantics. For a data stream D = (TD, vD), any stream I = (T, υ) ⊇ D that coincides with D on AE is an interpretation stream for D. A tuple M = 〈T, υ, W, B〉, where W is a set of window functions and B is the background knowledge, is then an interpretation for D. Throughout, we assume W and B are fixed and thus also omit them.

Satisfaction by M at t ∈ T is as follows: M, t |= α for α ∈ A+, if α holds in (T, υ) at time t; M, t |= r for rule r, if M, t |= β(r) implies M, t |= H(r), where M, t |= β(r), if (i) M, t |= βi for all i ∈ {1, . . . , j} and (ii) M, t ̸|= βi for all i ∈ {j+1, . . . , n}; and M, t |= P for program P, i.e., M is a model of P (for D) at t, if M, t |= r for all r ∈ P. Moreover, M is minimal, if in addition no model M ′ = 〈T, υ′ ,W, B〉 ̸= M of P exists such that υ′ ⊆ υ.

Definition 3 (Answer Stream) An interpretation stream I is an answer stream of program P for the data stream D ⊆ I at time t, if M = 〈T, υ,W, B〉 is a minimal model of the reduct P M,t = {r ∈ P | M, t |= β(r)}. By AS(P,D, t) we denote the set of all such answer streams I.

Example 6 (cont'd) Let D′ = (T, υ′ ) be the data stream which adds to the stream D from Example 3 the input 39.7m ↦→ {request}. We get two answer streams I1 = (T, υ1) and I2 = (T, υ2) of P for D′ at t = 39.7m, which both contain, in addition to the mappings in υ′ , 40.2m ↦→ {expBusM} and 44.1m ↦→ {expTrM}. Answer stream I1 additionally contains the recommendation t ↦→ {takeTrM} and I2 suggests t ↦→ {takeBusM}, since both vehicles are expected to arrive in the next 5 minutes. ■

2.3 TruthMaintenance Systems

Truth maintenance systems (TMS) [Rich and Knight, 1991] aim to implement nonmonotonic reasoning. We recall the general idea of justification-based TMS (JTMS) [Doyle, 1979], using notation as in [Beierle and Kern-Isberner, 2000].

A TMS T = (N,J) consists of a set N of nodes and a set J of justifications J of the form 〈I|O→n〉, where I = {in1, . . . inl} and O = {o1, . . . , om} are sets of nodes. Intuitively, n is by J in (true), if all ini's are in and no oj's are in (they are all out), i.e., J "fires." A model M of T labels each node n with status in or out. Notably, the admissible models of T correspond to the answer sets (stable models) of the logic program PT = {rJ | J ∈ J} where rJ is the rule n ← in1, . . . , inl, not o1, . . . , not om [Elkan, 1990].

Given an admissible model M of T and a new justification J0 = 〈I0|O0 → n0〉, the TMS algorithm aims to update M to an admissible model M ′ of T ′ = (N,J ∪ {J0}). In that, key notions for nodes n are the following. The consequences (Cons(n)) are nodes with a justification that involves n. The support consists of a set (Supp(n)) of nodes witnessing the (in)validity of n. Finally, the affected consequences (ACons(n)) are nodes whose support involves n.

Briefly, if J0 fires in M and n0 was not in, only the nodes in ACons(n0) are re-evaluated (after setting their status to unknown) proceeding along the dependencies, where Supp is updated. For a node n, its justifications are checked whether they are (i) founded (in)valid, or (ii) unfounded (in)valid. In case (i), the new status of n (in or out) is settled, as definitely some (resp. no rule) will fire; if not, in case (ii) a guess is made and propagated, with backtracking on failure.

3 Stream-stratified Programs

Stratification [Apt et al., 1988] is a well-known method to split a logic program with acyclic negation into strata that can be evaluated successively. We carry this over to stream inputs and define stream stratification, which will allow us to evaluate and predict the temporal validity of atoms hierarchically.

In the sequel, A+sub (P ) are the extended atoms α occurring in P , plus the extended atoms of form @ta and a inside α.

Definition 4 The (stream) dependency graph of a program P is a directed graph GP = (V,E), where V = A+sub (P) and E contains edges

The intuition of an edge α→⪰ β is that the truth value of α depends on the one of β. The label ⪰∈ {≥,=,>} indicates the possibility to slice the program into parts (strata) that can be evaluated levelwise. For instance, ⊞✸a can only be evaluated after the value of the ordinary atom a is known. This dependency would be reflected by an edge ⊞✸a →> a. On the other hand, @ta must be co-evaluated with a.

Example 7 Let P ′={@tx←⊞3 @ty}. Then, GP ′ =(V,E), where V = A+sub (P ′ ) = {@tx, x, ⊞3@ty, @ty, y} and

Based on this, we define the notion of stream stratification.

Definition 5 (Stream stratification) Let P be a program with stream dependency graph GP = (V,E). A mapping λ: A+(P) → {0, . . . , n}, k ≥ 0, is called a stream (s-)stratification for P , if α →⪰ β ∈ E implies λ(α) ⪰ λ(β) for all ⪰∈ {≥, =, >}. We call P stream (s-)stratified, if it has a stream stratification.

Stream stratification captures the intuition that the dependency graph has no cycle with an edge α→> β, i.e., no recursion through window operators. Using standard methods, we can decide in linear time whether P is s-stratified, i.e., check that no strongly connected component of GP contains an edge α →> β and if so, compute an s-stratification λ.

Example 8 (cont'd) Program P ′ of Ex. 7 is s-stratified. We take λ(@ty)=λ(y)=0 and λ(⊞3@ty)=λ(@tx)=λ(x)=1. ■

From λ, we naturally obtain a partition of P into strata P0, . . . , Pn by Pi = {r ∈ P | λ(H(r)) = i}. Without loss of generality, we may assume that each Pi is non-empty.

Example 9 Figure 4 depicts a partial s-stratification of the program P in Ex. 5 and the induced three strata P0, P1, P2. ■

Like in usual stratified logic programs, we can evaluate an sstratified program P stepwise, i.e., stratum per stratum, where the results of the previous strata serve as input to the current stratum. This is formally captured by the following result.

Proposition 1 Let D be a data stream and let P be an s-stratified program with strata P0, . . . , Pn. Define I P,t 0 =AS(P0,D, t) and I P,t k+1= ⋃I∈I P,t k AS(Pk+1, I, t) for 0 ≤ k < n. Then, we have I ∈ AS(P, D, t) iff I ∈ I P,t n .

Intuitively, at each layer k, s-stratification ensures that inferences of P0 ∪ · · · ∪ Pk will not be retracted by adding Pk+1, and new inferences come exclusively from Pk+1.

4 TMS Extension

We now present technical ingredients of our update algorithm for answer streams, which are reflected in a TMS extension suitable for incremental evaluation of temporal information.

Towards an according TMS data structure M, we introduce a label of an extended atom α as L(α) = (s, T ) where s ∈ {in, out, unknown} is the status of α and T is a set of time intervals, meaning that α has status s during each interval in T . (We will write [t1, t2] instead of {[t1, t2]}.) Given a partial labeling of atoms, i.e., some atoms have status unknown, we define different types of (un)founded (in)validity of rules, where for readability, we use obvious abbreviations. For instance, "B+(r) some out" means that some atom in the positive body of r has status out:

Informally, fVal(r) (resp. fInval(r)) fully determines satisfaction (resp. falsification) of the rule body based on the atoms appearing in r. On the other hand, ufVal (r) also holds for partial labelings and thus leaves falsification open.

We extend the TMS notions in Section 2.3 to deal with the temporal and streaming aspects in our setting as follows.

Consequences. Let P0, . . . , Pn be the strata of P. To capture the structural dependencies between atoms a ∈ A and extended atoms α ∈ A+ in P , we define the consequences

Cons(α) = Consh(α) ∪ Consw(α) ∪ Cons@(α), where

• the head consequences are all heads of rules with α in the body, i.e., Consh(α) = {H(r) | ∃r ∈ P, α ∈ B(r)},
• the window consequences are Consw(a) = {⊞ ⋆ a ˆ∈ P}, where ⋆ ∈ {✸, ✷} and a ∈A; and Consw(@tβ) = {⊞@tβ},
• the @-consq. are Cons@(@t′a) = {a} if @t′a ˆ∈ P , else ∅. Cons ∗ (α) denotes the transitive closure of Cons(α). 1

Support. The support of α is defined by

where Supp + and Supp - reflect the support in TMS, i.e., the witnessing of the status of an atom via rules. Formally:

• Supp +(α) is the positive support of α, which is empty if s(α) ̸= in and otherwise the union of the bodies B(r) of all rules r ∈ P H (α) that are founded valid at t;
• Supp -(α) is the negative support of α, which is empty if s(α) ̸= out. Else, if no rule r ∈ P H (α) is founded valid, it contains for each r ∈ P H (α) either an atom βi ∈ B +(r) with status out or an atom βi ∈ B -(r) with status in;
• Supp @(α) is the @-support of α, which is empty if α is a non-ordinary atom or s(α) = out; otherwise, it contains all atoms @t′α with s(@t′α) = in. Intuitively, @-support captures label witnesses for an ordinary atom α of the form @t′ α.

Affected consequences. The affected consequences of α are ACons(α) = {β ∈ Cons(α) | α ∈ Supp(β)} ∪ Cons@(α), i.e., all consequences that have α in their support and the or-

dinary atom extracted from α in case it is an @-atom. Furthermore, ACons ∗ (α) is the transitive closure of ACons(α). Given a set A of ordinary atoms, we define the affected consequences of A at a time point t as

Distinguishing t > 0 from t = 0 is due to the fact that when starting from scratch at t = 0, no support of atoms is established and likewise no affected consequences; we thus rely

Algorithm 1: AnswerUpdate(t, D, var M)

Input: Time point t, data streamD, TMS structureM reflecting an answer stream for an s-stratified program P = P0, . . . , Pn on D at time t′ < t Output: Update of M reflecting an updated answer stream for P at time t or fail foreach stratum ℓ := 1 → n do C := ∅ and L′ := current labels foreach 〈α, ω〉 ∈ Expired(ℓ, t′ , t) do ExpireInput(α, ω, t) and C := C ∪ {ω} foreach 〈α, ω, t1〉 ∈ Fired(ℓ, t′ , t) do FireInput(α, ω, t1) and C := C ∪ {ω} UpdateTimestamps(C, L′ , ℓ, t) SetUnknown(ℓ, t) repeat if SetRule(ℓ, t) fails then return fail if MakeAssignment(ℓ, t) fails then return fail until no new assignment made SetOpenOrdAtomsOut(ℓ, t) PushUp(ℓ, t)

on the syntactic dependencies given by Cons. The affected consequences of A at t restricted to a stratum ℓ are

Example 10 Consider a program P ′ containing only the following ground instance r′2 of rule (r2) in Example 5:

We have the following consequences:

Suppose we are given the following labels:

Then, r′2 is founded valid, i.e., fVal(r′2 ) holds, and we have:

5 Answer Update Algorithm

This section presents the AnswerUpdate algorithm. Let P be an s-stratified LARS program and D be a data stream. Given a time point t, a time point t′ < t, and an answer stream of P for D at t′ , reflected in a TMS data structure M. AnswerUpdate modifies M such that a new (updated) answer stream at time t is reflected in it. To this end, it iterates over the strata of the program P and updates the status of atoms and their temporal validity. At each stratum ℓ, we have to consider two orthogonal aspects:

(O1) For extended atoms with unchanged status, we only update the time labels and set a label to the maximal extent for which the status can be guaranteed. For window atoms, this guarantee comes, e.g., from reappearance of the same tuple in the data stream in case of ✸, or from absence of tuples in case of ✷. For atoms in rule heads, the label update depends on label updates of window atoms in the bodies.

(O2) Re-evaluate the status of atoms affected by the change in the input. This is inspired by the TMS algorithm, which tries to keep the answer untouched as much as possible.

Expire/Fire Input. The algorithm collects two sets Fired(ℓ, t′ , t) of firing atoms and Expired(ℓ, t′ , t) of expired (extended) atoms between time points t′ and t at stratum ℓ. Intuitively, Fired(1, t′ , t) is collected from υ(t′ + 1) to υ(t), i.e., the window atoms of the tuples from the input stream fire at stratum 1. For ℓ > 1, Fired(ℓ, t′ , t) is computed from the atoms concluded at lower strata. Expired(ℓ, t′ , t) is calculated by a supportive function of each window atom, taking into account the current time point, the content of the window and the fired input. Both functions return an atom α and a window atom ω in which α expires/fires. Fired(ℓ, t′ , t) also returns a time point t1 ≤ t at which the firing happens. Then, ExpireInput and FireInput update the labels of window atoms at ℓ. Note that FireInput can be optimized by not firing incoming inputs that are not anymore relevant at t. The affected window atoms are collected in a set C.

Time and status adjustment. The processing continues to determine the labels of rule heads wrt. the orthogonal aspects (O1) and (O2). For (O1), UpdateTimestamps finds window atoms in C having unchanged labels (by comparing with L′ ), based on that identifies rules where the applicability does not change and thus the time label of the head can be extended. For (O2), the TMS method is applied to set the labels of remaining atoms. We set the labels of atoms (except window atoms) affected by incoming and expiring atoms to unknown (SetUnknown), identify founded (in)valid rules and set the status of respective head (SetRule), and make assignments for head and unknown body atoms in an unfounded (in)valid rule (MakeAssignment). SetRule and MakeAssignment detect inconsistency when they set the label of an atom to in/out but that label was already set to out/in for the same interval. The algorithm then stops and outputs 'fail.'

The repeat loop ensures that rules that become founded will be processed by SetRule. After the loop, ordinary atoms that do not occur as rule heads may still be unknown, if some of their @-atoms do occur (e.g., expTrM). Such atoms are labeled (out , [t, t]) in SetOpenOrdAtomsOut. Finally, rule heads are pushed as input to the next stratum by PushUp(ℓ, t).

Initialization. The first answer stream reflects the initial state with an empty input stream at time 0. To obtain it, we set in M all atom labels to (out, [0, 0]) and all transitive consequences of the input atoms except window atoms to unknown. We then call AnswerUpdate(0, D0,M), where D0 = ([0, 0], {}). This results in a labeling at time 0 and supports for atoms in it; from t ≥ 1, the sets of affected consequences are in place for calling AnswerUpdate(t, D,M).

Example 11 (cont'd) Consider the program in Example 5. The initialization sets all labels to (out , [0, 0]) and thus a negative support for all rule heads. Maintenance starts with an empty answer stream and waits for input.

Simple Updates. At t = 37.2m, busG arrives as first atom. In the window obtained by ⊞3m, atom @37.2mbusG will hold for 3 min. This is reflected in the algorithm by FireInput which sets L(⊞3m@37.2mbusG) = (in, [37.2m, 40.2m]). The relevant ground rule of (r1),

should not fire, since on cannot be derived. Indeed, the status of on is still out and so is @40.2mexpBusM after SetRule. At t = 39.1m, atom tramB arrives, and we have L(⊞5m@39.1tramB) = (in, [39.1m, 44.1m]). Similarly, ground rule (r′2 ) (shown in Example 10) cannot fire, i.e., @44.1mexpTrM will be out.

Update with rule firing. As shown in Fig. 2, Kurt sends his first request at t = 39.7m. FireInput sets the label of ⊞1m✸request to (in, [39.7m, 40.7m]). By SetRule, this label is then first carried over to predicate on due to rule (r3). Furthermore, the labels of @40.2mexpBusM and @44.1mexpTrM are set to (in, [39.7m, 40.2m]) and (in, [39.7m, 40.7m]) due to rules (r1) and (r2), respectively, where according ground rules are now founded valid.

Pushing these conclusions to the next stratum updates L(⊞+5m✸expBusM) to (in, [39.7m, 40.2m]) and L(⊞+5m✸expTrM) to (in, [39.7m, 44.1m]).

Choices. The last two rules of P are still unfounded valid, since the status of the negative atoms is unknown. The choice of MakeAssignment to take the bus materializes as status in for takeBusM and out for takeTrM.

Nonmonotonic negation. Later at time t = 40.0m a traffic jam report comes in as υ(40.0m) = {jam}, thus at stratum 2, rule (r4) is unfounded invalid due to the negation of the window atom ⊞3m✸jam which is set to in by FireInput. The head cannot be concluded anymore, and MakeAssignment flips the previous statuses of takeBusM and takeTrM.

Efficient adjustment. Kurt sends another request t = 40.1m, so FireInput sets L(⊞1m✸request) = (in, [40.1m, 41.1m]) and C = {⊞1m✸request}, since it was in before. Thus, UpdateTimestamps updates the time label tm(on) to [39.7m, 41.1m] due to rule (r3) and furthermore updates tm(@44.1mexpTrM) to [39.1m, 41.1m] due to rule (r2). The rest on stratum 2 proceeds similarly as before. ■

Correctness. Algorithm AnswerUpdate computes new labels for atoms in an s-stratified program P that get affected by the update of the input stream D at a time point t. Its correctness relies on the generic subroutines FireInput, ExpireInput to faithfully reflect the functionalities of an associated window function w. Under this assertion, the new labeling inM can be translated into an answer stream from AS(P, D, t). In particular, for time-based windows, which have simple supportive subroutines, this is formally stated as follows.

Proposition 2 Let D = (T, υD) be a data stream, P be an s-stratified program, and W = {w1 τ , . . . , wn τ } be time windows. Let t, t′ ∈ T s.t. t′ < t and suppose M reflects some I ∈ AS(P,D|t′ , t′ ), where D|t′ is the restriction of D up to t′ . Then, if AnswerUpdate(t,D,M) does not return fail, it updates M such that for some answer stream (T, υ) ∈ AS(P,D, t), every t′′ ∈T satisfies υ(t′′ ) = υD(t′′ ) ∪ {a ∈ AI | s (a) = in ∧ t′′ ∈ tm(a)}.

6 Discussion

The above TMS extension amounts to the (corrected) TMS procedure if (i) no windows and temporal operators are used, or (ii) all windows are time-based and select only the current time point, since this essentially eliminates the timeline.

Runtime complexity. The runtime of AnswerUpdate depends on the program size |P| (number of rules), the number n of strata, the number of extended atoms |A+|, the stream size, and the specific window functions. For the practically important time- and tuple-based windows, status labels can be maintained efficiently. In the worst-case, UpdateTimestamps runs in O(|P|2 ·|A+|) time but can be made sub-quadratic in |P | using suitable data structures to store the relation between atoms, window atoms, rules, etc. Other subroutines are less costly. Window sizes are small and thus a constant factor.

Head-@-free programs. The useful @-atoms in rule heads complicate evaluation, as intuitively intentional streams must be handled at each stratum. Excluding head occurrences of @ yields a fragment with simple and faster algorithms, where intensional facts are only derivable at the query time. Such head-@-free programs P can be split into a lower part Pl with acyclic rules using windows on extensional facts, and an upper part Pu consisting of ordinary rules; by using ExpireInput and FireInput, the rules of Pl can be evaluated in a deterministic way, and those of Pu by using either an ASP solver or the incremental TMS extension to carry over the time labels.

Completeness. Algorithm AnswerUpdate might fail, even if some answer stream for P wrt. D at the query time t exists. To gain completeness, one needs to use proper backtracking in case an inconsistency (a conflict) is encountered. The backtracking technique in TMS can be extended for this purpose, by finding a 'nogood' assignment that leads to the conflict and going for a different guess from there. Notably, if P has no cyclic negation, no backtracking is needed. Furthermore, one can similarly employ extended backtracking to compute other answer streams. However, this is beyond the scope of this paper and subject for future work.

7 RelatedWork and Conclusion

In ASP, incremental evaluation as in iclingo (see potassco.sourceforge.net) aims at time slicing; reactive ASP as in oclingo [Gebser et al., 2012] considers k-expanded logic programs, which are incrementally evaluated over a single sliding window of size k by incorporating always the next time point. In contrast, we build an answer stream at time t by adapting one from t′ < t. Furthermore, the more expressive language LARS makes temporal data management much more demanding.

ETALIS [Anicic et al., 2012] is a monotonic rule formalism for complex event processing to reason about intervals. No incremental evaluation or windows are considered.

StreamLog [Zaniolo, 2012] extends Datalog for stream reasoning based on XY -stratification, which guarantees a single model on a stream. As in s-stratified programs, rules concluding about the past are excluded. However, neither windows nor incremental evaluation have been considered.

The DRed algorithm [Gupta et al., 1993] for incremental Datalog update deletes all consequences of deleted facts and then adds all rederivable ones from the remainder. It was adapted to RDF streams in [Barbieri et al., 2010], where tuples are tagged with an expiration time. Our more expressive TMS approach makes time management more difficult.

[Ren and Pan, 2011] explored the use of TMS techniques for incremental update in ontology streams. However, windows and time reference were not considered, thus no temporal management is needed, and the setting is monotonic. Model update was also considered in the context of CTL. In [Zhang and Ding, 2008], minimal change criteria were identified and an update algorithm was presented.

Related to our work is also belief revision, which deals with changing a belief set [Alchourr´on et al., 1985] or knowledge base [Katsuno and Mendelzon, 1991] to accommodate new information without introducing inconsistency. In [Dixon and Foo, 1993] it was shown how Assumption-based Truth Maintenance Systems (ATMS) can be simulated in the AGM logic of belief [G¨ardenfors, 1988] by means of an epistemic entrenchment relation (i.e., a total pre-order over sentences) to encode justifications of beliefs. Belief revision and belief update have also been studied in relation to logic programs under the answer set semantics in [Delgrande et al., 2008] and [Slota and Leite, 2014].

Outlook. We have presented a generic algorithm for incremental answer update of logic programs for stream reasoning with ASP like semantics, based on stream stratification and an extension of TMS techniques by temporal data management. Further issues concern instantiation of the algorithm for typical window functions and optimization, as well as identifying program classes amenable to highly efficient answer update.