Streaming Multi-Context Systems

1 Introduction

Rooted in McCarthy's seminal work [1993], multi-context systems (MCS) model knowledge bases (KBs) interlinked by bridge rules, cf. [Giunchiglia et al., 1994; Ghidini et al., 2001; Brewka et al., 2007; Bikakis et al., 2010]; in particular, Brewka and Eiter [2007] provided a powerful generic framework to interlink heterogeneous information sources in an equilibrium semantics. Towards handling dynamic data, MCS have recently been extended to reactive MCS (rMCS) [Brewka et al., 2014] and evolving MCS (eMCS) [Goncalves et al., 2014] which feature sequences of equilibria obtained synchronously, and to asynchronous MCS (aMCS) [Ellmauthaler and P¨uhrer, 2015] in which controllers trigger local KB to update and to output rules to push beliefs to other contexts.

However, no extension of MCS has features for handling streaming data [Della Valle et al., 2009; Arasu et al., 2006; Heintz, 2010]. In contrast to processing (sequences of) static data, data stream processing deals with continuous computation, which typically requires some explicit reference to time.

Example 1 Fig. 1 depicts two robots R1 (at node 3) and R2 (at node 9), in an indoor environment (e.g., department store). They must deliver packages P1 (at node 9) and P2 (at node 4) to destinations D1 (node 7) and D2 (node 1), resp. Only R1 can travel from 6 to 7, so he could take the path 3-4-5-8-9 to pick up P1 and then deliver via 9-8-6-7. Similarly, R2 would take 9-8-5-4-2-1. To minimize the combined travel distance, they can coordinate and alternatively pick up the packages close by and exchange them at node 5. Reaching an agreement may be challenging when they are already moving, and e.g. a link is not usable as too many people were recently observed on it. This may be inferred from a time-based window of a stream with position data of people. ■

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

To reason over such asynchronous information exchange systems, communication and local computation time must be considered, and only recently sent/received data will be relevant. Moreover, in general no stable state of information exchange may be achieved, e.g. an agreement on a meeting point for the robots. In the static case, but also in rMCS and in eMCS, computing equilibria is considered to be timeless; in our dynamic setting, however, data (also new requests) keep streaming while any computation is ongoing; this may render the result upon completion invalid. While aMCS account for controlled information exchange, physical computation and transfer time are disregarded and no baseline mechanism to achieve an equilibrium is considered.

To tackle these issues, we introduce Streaming MultiContext Systems (sMCS), with the following contributions.

• To equip MCS for data streams, we base sMCS on managed MCS (mMCS) [Brewka et al., 2014] and extend bridge rules with window atoms for snapshots of input streams at contexts. Although it is possible extending rMCS/eMCS to emulate window atoms, having them as first-class citizens in the formalism allows sMSC while add streaming features to MCS, still retain MCS' principles, namely: bridge rules are simple to import knowledge and contexts are abstract. We discuss this issue in more detail in Section 6.
• Our framework models transfer time of data between and computation time at contexts, to reflect the asynchronous behavior that arises in general, and has an internal execution control at the contexts.

• We define a run-based semantics of sMCS as special sequences of states. In that, we introduce feedback equilibria, which are a non-trivial lifting of the key notion of MCS equilibria to the asynchronous setting, by which local stability in runs can be enforced. They provide semantic middle-ware to overcome potentially infinite loops; e.g., if the robots in Ex. 1 would mutually send proposals and keep adjusting them, they may never agree on a meeting point.
• Finally, we consider reasoning in sMCS and characterize the complexity of ad-hoc queries and prediction. To our knowledge, the latter has not been considered for MCS so far.

2 Streams

To set up a streaming environment, we borrow some formal notions from the LARS framework [Beck et al., 2015]. We assume an underlying set A of ground (propositional) atoms.

Definition 1 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 ↦→ 2A.

Intuitively, a stream S associates with each time point a set of atoms. If S = (T, υ) and S′ = (T ′ , υ′ ) are streams such that T ′ ⊆T and υ′ (t′ )⊆υ(t′ ) for all t′ ∈T ′ , we write S′⊆S and call S′ a substream or window of S.

We call streams that provide input also data streams. To cope with large input volume, one usually considers only recent atoms by applying window mechanisms on streams.

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.

Prominent are time-based window functions, which select the atoms of the latest k time points. Formally, the (sliding) timebased window of size k is τ (k)(S, t) = (T ′ , υ|T ′ ), a substream of S, where S=(T, υ) is any stream and t any time point in T=[t1, t2] and T ′ = [t′ , t] such that t′ = max{t1, t - k}.

To express formulas on streams, LARS offers window and temporal operators. For sMCS, we borrow plain LARS window atoms (briefly window atoms), of the form (a ∈ A and t′ ∈ N):

A streaming atom is either an atom or a window atom. Entailment of a streaming atom from a stream S = (T, υ) at a time point t is defined as follows, where S′ = (T ′ , υ′ ) = w(S, t):

S, t ⊩ ⊞w✸a iff a ∈ υ′ (t′ ) for some t′ ∈ T ′

S, t ⊩ ⊞w✷a iff a ∈ υ′ (t′ ) for all t′ ∈ T ′

S, t ⊩ ⊞w@t′a iff a ∈ υ′ (t′ ) and t′ ∈ T ′

For a streaming atom α, S, t ⊩ notα iff S, t ̸⊩ α. Furthermore, let S, t ⊩ ⊤ for all t ∈ T , where ⊤ is a special atom. For convenience, we abbreviate ⊞τ(k) with ⊞k .

Example 2 Let block(X, Y ) states that a link (X, Y ) is blocked; then ⊞3✷block(a, b) holds at t if the link (a, b) has been always blocked in the last 3 time units. ■

For any window atom α of form (1), let at(α) be the ordinary atom extracted from α, that is, at(α) = a.

3 StreamingMulti-Context Systems

We now define streaming Multi-Context Systems as a generalization of mMCS [Brewka et al., 2011] to handle streaming data. The main idea is that contexts, interlinked by bridge rules, continuously receive input from neighbors, compute, and then send output to other contexts. To govern data flows coming to contexts, we extend bridge rules with window atoms.

To better highlight the issues relevant for this paper, we confine to mMCS in which (1) each context has a single logic rather than a logic suite, (2) the management functions are deterministic. An extension to arbitrary mMCS is not difficult but technically somewhat involved.

First, we recall the notion of logics and contexts in mMCS. A logic L is a triple 〈KBL, BSL, ACCL〉, where KBL is the set of admissible knowledge bases (KBs) of L, BSL ⊆ 2BSL is the set of possible belief sets over a set of beliefs BSL, and ACCL : KBL → 2BSL represents the semantics of L by assigning to each kb ∈ KBL a set of acceptable belief sets.

Without loss of expressiveness, we consider a setting in which beliefs are ordinary ground atoms.

A context has the form C = 〈L, ops, mng〉, where L is a logic, ops is a set of operations, and mng : 2ops ×KBL → KBL is a management function. For an indexed context Ci we write Li, opsi, and mngi to denote its components.

Important in a streaming environment are sensors that continuously emit readings: this can be modeled by sensor logics of the form LD=〈{∅},BSD,ACCD〉, where ∅ is a dummy local KB, D is a value domain (possible readings) and BSD={s ⊆ D | |s| ≤ 1}, ACCD(∅)=BSD. Intuitively, either the empty set or a set with a single value from D can be an acceptable belief set of LD.

We now extend bridge rules with streaming bridge atoms.

Definition 3 Let C = 〈C1, . . . , Cn〉 be a tuple of contexts. A streaming bridge rule r for Ci over C is of the form

where op ∈ ops i and each βℓ = (cℓ:αℓ) is a bridge atom where cℓ ∈{1, . . . , n} and αℓ is a streaming atom for Ccℓ , i.e., αℓ ∈BSLcℓ or at (αℓ) ∈BSLcℓ . We denote by H (r) = op the head and by B(r) = {β1, . . . , βj, not βj+1, . . . , not βm} the body of r.

Sensor contexts are contexts with sensor logics, no bridge rules, no operation, and the management function satisfying that mng(∅, ∅) = ∅. We can now define streaming multicontext systems.

Definition 4 A streaming multi-context system (sMCS) M = 〈C, BR, KB〉 consists of

• a tuple C = 〈C1, . . . , Cn〉 of contexts,
• a tuple BR = 〈br1, . . . , brn〉 of sets bri of streaming bridge rules for Ci over C,
• a tuple KB = 〈kb1, . . . , kbn〉 of KBs kbi ∈ KBLi .

Example 3 Fig. 2 shows Ex. 1 as sMCS M = (C1, . . ., C6):

• Ci, 4≤i≤6, is a sensor context that feeds data to Ci-3; C4 (resp. C5) tells the current position pos(X, Y, L) of robot R1 (R2 ), meaning it is at L% on the way from X to Y . C6 provides data n(X, Y, N) that N people were sensed on the link (X, Y ).

C1

C2

• C3 takes the sensor data fromC6, reasons about blocked links and sends this information to C1 and C2.
• C1 (resp. C2) aims to find a shortest route fromR1 's (resp. R2 's) position to its destination respecting blocked links and in C2 possible meeting points m(X).

Focusing on the streaming aspects, we omit the details of the local planning logics at C1, C2 , except a notice that if a new plan proposes the same meeting point as the previous plan, then this information is not resent to the other context. ACCplanning in C1 can either remember the latest proposed meeting point on its own, or self-import this information by adding the following bridge rule into br1:

We now give a brief explanation on the bridge rules. Intuitively, update(p(X)) drops the facts of predicate p and then adds a new ground fact p(X), while remove(p(X)) removes p(X). The bridge rules of br1 and br2 with remove in the head drop blocking information for a link (X, Y ), if it was not continuously reported blocked in the last 3 time units.

The bridge rule in br3 informs kb3 about crowded links using facts cr(X, Y ). To keep C3's local reasoning simple for the moment, such links are viewed as blocked. ■

3.1 Semantics of StreamingMCS

We define the semantics of sMCS in terms of runs, which are sequences of states with constraints on the information exchange between contexts and their local semantics, as well as on the time spent for that. Before going into the details of the semantics, we recall two important aspects of stream processing, namely execution modes and execution policies.

In stream processing, there are two execution modes:

• Pulling: an engine periodically executes, e.g. every 5 seconds, regardless of when input arrives; this amounts to time-driven evaluation.
• Pushing: an engine executes immediately when input arrives; this is also known as eager mode, and amounts to data-driven resp. event-driven evaluation.

However, an engine might still be busy with a current computation while an execution should be triggered according to its execution mode, for example, when the time reaches a period in pulling mode or when a new input arrives in pushing mode.

An engine can follow either the ignore or restart policy in such situations. The former means that the engine continutes its computation while the latter means that it abandons the current computation and starts with a new one according to the respective execution mode.

The combination of "pushing" and "ignore" can lead to situations in which an execution is carried out immediately after a previous execution finished because some input arrived during the previous execution. That is, the actual start of an execution is different from the intention to start it according to the execution mode. We introduce in the following the notion of states to model such situation.

States. A state of context Ci is a triple si=(si, oi, kbi) where

• si ⊆{IE, SE} is the execution status: IE means an intent to start an execution, either proactively (pulling), or reactively on new input (pushing); SE means a computation actually starts. Sensor contexts always have status {IE, SE};
• oi ∈ BSLi ∪{ϵ} is the output, which is streamed to other contexts, unless oi = ϵ (meaning that nothing will be sent to other contexts);
• kbi ∈ KBLi is the local KB (which can evolve).

A (global) state of M is any tuple s = (s1, . . . , sn) of states si of context Ci, 1 ≤ i ≤ n. By si(t′ ) = (si(t′ ), oi(t′ ), kbi(t′ )) we denote the state of Ci at time t′ . Towards runs, we define:

Definition 5 Given a timeline T , a state sequence of M up to t ∈ T is any sequence s = s(0), . . . , s(t) of global states s(t′ ) = (s1(t′ ),. . . , sn(t′ )).

Arbitrary state sequences may not align belief output with respective KB evaluation. For that, input from bridge rules must be respected, as well as the actual start of computations: if an intent arises while Ci is busy, it may (by some policy) restart the computation or ignore the intent until the current computation ends. Runs will enforce these conditions to faithfully capture the evolution of sMCS. We next address the issue of input.

Input streams of contexts. Any state sequence s = s(0), . . . , s(tend) naturally induces an output stream Sk =(T, υk) of Ck, where T = [0, tend] and υk(t)=ok(t) for all t∈T. However, due to transfer time this output is not immediately available as input at other contexts Ci. To simplify presentation, we assume in our basic model that this transfer takes ∆ki units of time. This can be generalized to functions with different parameters, e.g., the time point t or the size of ok(t). We define input streams as follows.

Suppose that Ci accesses Ck, i.e., some bridge rule r ∈ bri has some atom (k:α) in the body. Then the input stream of Ci from Ck at time t based on s is Ss,t ki = (T, ιυs,t ki ), where

Intuitively, due to the delay ∆ki, no output of Ck can be expected at Ci from time points 0 to ∆ki; for further time points up to t, Ci receives the output from Ck with delay.

We also omit s and/or t if clear from the context.

Example 4 (cont'd) Consider contexts C1,C2,C3, and C6 with output streams Si = ([0, 20], υi), where υ3(10) = {block(5, 6)}, υ1(2) = {m(5)}, υ1(14) = {m(6)} and υ6(t′ ) = {n(5, 6, 15)} for t′ ∈ {4, . . . , 8}. Let t=20; then

• for ∆12=1, S12 has ιυ12(3)={m(5)}, ιυ12(15)={m(6)};
• for ∆31=1, S31 has ιυ31(11) = {block(5, 6)};
• for ∆63=1, S63 has ιυ63(t′ )={n(5, 6, 15)}, 5≤t′ ≤9.

A bridge rule r ∈ bri is applicable wrt. a state sequence s at t (in symbols, s ⊩it r), if Ski, t ⊩ α for every (k : α) ∈ B(r) and Ski, t ̸⊩ α for every not (k : α) ∈ B(r). We denote with appi(s, t)={H (r) | r∈br i ∧ s |=it B(r)} the heads of all applicable bridge rules of Ci wrt. s at t.

Evaluation time. As for asynchronous execution, we adopt that besides the transfer times ∆ki, functions fi measure the time that Ci needs to (1) evaluate the bridge rules, (2) run the management functions for local KB update, and (3) evaluate the updated KBs. Clearly, such functions may depend on various parameters, and different levels of detail are possible. As a baseline, we assume that fi assigns each pair (bri, kbi) a natural number. This can be generalized with further parameters (e.g., time) and/or intervals bounding the evaluation times; the latter allows us to express uncertainty and reduces to the baseline via all induced point measurements. Alternatively, probabilistic estimations can be considered. For sensor contexts, we simply may adopt fi=0.

From state sequences to runs. Given a state sequence s, a context Ci, and a time point t, the latest time point when Ci was triggered to execute is denoted by (max ∅ = -1):

Runs are state sequences where context output stems from its local KB and the input at the closest triggered time. Formally, Definition 6 A run for an sMCS M is a state sequence s=(s0, . . . , stend ) such that oi(0) = ϵ, kbi(0) = kbi, and for all t ∈ [1, tend ]:

where:

• (i) kbi(t) = mngi(appi(s, tex ), kbi(tex )),
• (ii) tex = tr(s,Ci, t),
• (iii) t = tex +fi(bri, kbi(tex )),
• (iv) kbi(t′ ) = kbi(tex ) for all t′∈(tex , t).

Intuitively, when a context Ci produces some output oi(t) at a time point t, this output must be computed on (i) the updated local KB based on input stream at (ii) the closest triggered time point tex . Furthermore, the distance from tex to t must be (iii) the computation time of the respective input. Finally, during computation, the update of the local KB is hidden to the outside of the context (iv).

Example 5 (cont'd) Fig. 3 illustrates a run of the sMCS where subscript i denotes output of Ci, i = 1, 2 (we focus on the robots). We have ∆12=∆31=1 and ∆ij=0 otherwise; f1(br1, kb1)=2, f2(br2, kb2)=4, and f3(br3, kb3)=1 for all kbi ∈ KBLi . Contexts C1, C2, C3 operate in pushing mode; C1 ignores new input if it is busy, while C2 and C3 restart.

The sensor contexts C4, C5 stream data at times 5k, k ≥0, C6 streams data at each time point. As ∆41=∆52=0, C1 and C2 receive input and intend to start execution at times 5k.

At t=2, C1 finds a plan to meet at node 5. This arrives at C2 at t=3, and C2 restarts its computation. At t=5, the contexts start executions wrt. new incoming data. C2 again aborts its previous computation. At t=7 and t=9, resp., the contexts come up with plans to meet at node 5.

Assume C3 sends block(5, 6) at t = 10, which C2 receives at 10 and C1 at 11 (both started to execute at 10). C1 ignores block(5, 6) at time 11 and starts executing with this input at time 12; this results in a new plan of C1 at t=14 to meet at node 6. A respective request arrives at C2 at t=15. C1 and C2, with input fromC4,C5, start executions at t=15 that end at time 17, resp. 19, and yield plans to meet at node 6. ■

To capture step-wise runs with equilibria semantics in the sense of rMCS and eMCS, we need to model an idealized setting in which contexts have unlimited power to compute equilibria between two consecutive time points (akin to flipflops in clocked hardware circuits). We can achieve this with a computation time so small such that the ACC function can be run finitely often (as an algorithm to compute an equilibrium will do) between two consecutive time points. Formally, we let the transferring time be 0 and the computation time be an infinitesimally small value ε such that (i) t < t + ε and (ii) ε + ε = ε; thus t + n× ε = t + ε, for each integer n > 0.

We now adapt the definition of input streams Ss,t ki to Ss,t,ε ki with ε by adapting Equation (3) with ∆ki = 0 as follows:

Moving output ok(tin + ε) to ιυs,t,ε ki (tin) is just a technique to respect the cyclic dependency between contexts in defining equilibria. Another approach that "shifts" the time line with ε is possible but more cumbersome (as non-integer time lines must be introduced) and thus not further considered here.

Then, we adapt the applicability relationship ⊩it to ⊩it,ε by substituting Ss,t ki with Ss,t,ε ki , and respectively, adapt appi(s, t) to app εi (s, t). Finally, idealized runs can be defined as follows: Definition 7 An idealized run for an sMCS M is a state sequence s = (s0, . . . , stend ) such that oi(0) = ϵ, kbi(0) = kbi, and for all t ∈ [0, tend):

• oi(t + ε) ∈ ACC(kbi(t + ε)) and
• kbi(t + ε) = mngi(app εi (s, t), kbi(t)).

Intuitively, at t+ε we have infinite power to respect the cyclic dependency and thus to compute equilibria. The result at this step is then placed at the next time point t + 1.

Note that simply setting ∆ki = fi = 0 in Definition 6 does not help us defining idealized runs from runs, as the latter are stateful with changing local KBs. Here, the introduction of ε is necessary as it fulfills the intuition that even in idealized settings computation still takes time, but infinitesimally small so that one can compute equilibria between to consecutive time points.

Our sMCS relate to mMCS, eMCS and rMCS as follows. First, sMCS generalize mMCS.

Proposition 1 Let M be an sMCS where contexts run in pulling mode and bridge rules have no window atoms. Then M can be viewed as an mMCS M m that outputs in idealized runs at each time an equilibrium obtained by M m .

Given an rMCS (resp. eMCS) M, we can construct a corresponding sMCS M s by turning sensors (resp. observation contexts) into sensor contexts and their observations into respective output streams. This allows one to capture rMCS.

Proposition 2 The runs of an rMCS M [Brewka et al., 2014] amount to the idealized runs of its corresponding sMCSM s .

For eMCS, however, this construction needs some condition. 1

Proposition 3 Let M be an eMCS such that op(a)←B is in bri iff next(op(a))←B is in bri. Then, the evolving equilibria of M amount to idealized runs of the sMCS M s .

Here, next(op(a)) belongs to the evolving operational formulas introduced in eMCS. Intuitively, such operations update the local KBs while operations op(a) are only used to provide the KB for computing the equilibria at a single step.

4 Feedback Equilibria

As shown in Prop. 1, traditional mMCS equilibria can only be achieved with idealized runs, which impose extreme conditions. Yet they apply if the stream granularity is significantly larger than evaluation and transfer time at resp. between contexts, such that an equilibrium computation can be carried out between two consecutive time points. Asynchronous runs are closer to practice. However, total asynchrony can evoke uncomfortable situations if contexts depend on each other.

Example 6 (cont'd) Suppose also C2 suggests a meeting point and C1 has a further bridge rule update(m2(X)) ← (2:m(X)) to import the suggestion to kb1. Moreover, the local planning logic checks whether the suggestions of the two robots match; if not, another round of planning is carried out and new suggestions are sent. Then if f1(br1, kb1)=2, f2(br2, kb2) = 3 for all kbi ∈ KBLi (i = 1, 2), ∆12 = 1, and all other costs are 0, the contexts might get stuck in a loop just to agree on a meeting point, as depicted in Figure 4. ■

1 Extending sMCS to fully capture eMCS is not difficult but rather technically involved (by introducing streaming bridge rules with the next operator and keeping two local KB states as in eMCS). This is, however, not the main goal of this paper.

In practice, it is important to avoid that subsystems of an sMCS run into a (possibly infinite) loop due to asynchronous information exchange. For this we may want to obtain stability, i.e., a local equilibrium of such subsystems; however, how to accomplish this is not straightforward.

The key idea is to respect that an equilibrium is intrinsically timeless, and to dispense streaming data from outside for its computation; this is a trade-off for success, comparable to ignoring requests during fast interrupt handling in CPUs.

We consider strongly connected components (SCCs) in an sMCS M, i.e., in the graph G(M) whose nodes are the contexts Ci of M and with edges Ci → Cj if Ci accesses Cj . We extend the run semantics of sMCS as follows:

(⋆) Ci can request stability of the SCC in which it occurs, denoted Ci. When Ci raises this request at time t = tex +∆ after it started execution at tex , the system restarts all other contexts in Ci to compute with their input at tex and allows them to disclose output in Ci until reaching an equilibrium.

(⋆⋆) Later at tout ≥t, Ci reports an equilibrium, or restarts its contexts with input at time tout if no equilibrium exists.

From t to tout , the contexts in Ci are in an internal solving mode and output no beliefs to contexts outside Ci; the latter still run asynchronously, unless stability is requested elsewhere. If simultaneous stability requests arise in Ci, one is nondeterministically followed. We formalize this as follows.

Definition 8 Let C = {Ci1 , . . . , Ciℓ } be an SCC of an sMCS M. A belief state of C is a tuple (BSi1 , . . . ,BSiℓ ) of belief sets BSij ∈ BSij , 1≤j ≤ℓ; it is an feedback equilibrium of C wrt. a run s of M at time t if for all j ∈ [1, ℓ] :

Intuitively, a feedback equilibrium of C at t is achieved by running its contexts in idealized mode with ε computation time. Thus, input to C is fixed at t, and cyclic information flow inside C is respected.

Based on this, we define stability of runs as follows where a special atom ρ denotes a stability request and a new status EQ the equilibrium computation mode.

Definition 9 Given an SCC C={Ci1 , . . . , Ciℓ } of an sMCS M, a run s of M on a timeline T = [0, tend ] is locally stable wrt. C, if whenever at time t, the set req(C, t) := {Cij ∈C | ρ ∈ oij (t)} is nonempty, then either

• (i) C has at tex wrt. s either (a) a feedback equilibrium (BSi1 , . . . ,BSiℓ ) such that oij (tout)=BSij for j ∈

[1, ℓ], or (b) no feedback eq. and sij (t′ )={SE}, for j∈[1, ℓ], and

or

Furthermore, s is locally stable, if it is locally stable wrt. every SCC of M.

Example 7 (cont'd) Reconsider Fig. 4. In a locally stable run, C1 realizes at t=3 that C2's suggestion does not match his sent at t=2. It can request local stabilization for its SCC C1={C1,C2} to find an equilibrium wrt. the input to C1 at tex =0. At some tout >3, an equilibrium is computed which guarantees an agreed meeting point, e.g. at node 6. ■

In practice, we may bound tout such that the SCC C will be reset at tout the latest: if stabilization takes too long, the result may be outdated (in particular, for reasoning on recent data).

5 Reasoning with StreamingMCSs

For reasoning from an sMCS M=(C1, . . . , Cn), we assume sensor contexts are D=Cj , . . . , Cn. A reading for M up to t is a state sequence r=r(0), . . . , r(t) such that o r i (t′ ) = ∅ for all i ∈ [1, j) and t′ ∈ [0, t]. Models are defined as follows.

Definition 10 Given an sMCS M with sensor contexts D, a run s for M is a model wrt. a reading r up to t, if |s| = |r| and o s i (t′ ) = o r i (t′ ) for all Ci ∈ D and t′ ∈ [0, t].

We consider brave reasoning: given M, a reading r up to t, a context Ci and an atom a, decide if a is true at time t in some model s of M wrt. r, i.e., a ∈ o s i (t) holds; we denote this by M, r |=b Ci(a). Model existence (consistency) and cautious reasoning easily reduce to this problem resp. its complement.

Setting. We assume that (a) each Ci periodically decides in constant time, by looking at its input stream, whether to execute, and is in permanent ignoring or restarting mode; (b) algorithms are available (given as code) to evaluate the bridge rules bri, to update the local kbi by the management function mngi, and to compute some BSi ∈ ACCi(kbi) (where each possible BSi may result); unless stated otherwise, the algorithms for bri and mngi run in polynomial time. The instance size is dominated by the sizes of r, all bri and kbi, and of the underlying atom set A (which is part of the input).

For reasoning with ordinary runs, we can show:

Theorem 1 Deciding M, r |=b Ci(a) is NP-complete, and NP-hard even if M is acyclic, the br i are not-free and without window atoms, and one of the following is not bounded by a constant: (i) |M|, (ii) the size of the input streams Ski, (iii) the size of the local KBs kbi.

Informally, we can guess a model s for r that witnesses M, r |=b Ci(a) and simulate the run from 0 up to t matching s, using the algorithms for bri, mngi and ACCi: naturally the streaming time maps to physical time by a (constant) factor. Note that the precise KB formats (propositional, non-ground) is here irrelevant. The NP-hardness is shown by various reductions from SAT. For determined contexts, tractability results.

Proposition 4 Deciding M, r |=b Ci(a) is in P, if M is deterministic, i.e., |ACCi(kbi)|≤1 holds for all Ci and kbi.

Locally stable runs. We denote by M, r |=bs Ci(a) the restriction of M, r |=b Ci(a) to locally stable models. As computing locally stable runs requires to recognize given acceptable belief sets, we suppose that deciding BSi ∈ ACCi(kbi) has complexity in C. We then obtain the following result.

Theorem 2 Deciding M, r |=bs Ci(a) is in NP NPC . It is NP NP -complete for M in which the contexts use (normal) logic programs with supported resp. stable model semantics.

Intuitively, local stability forces us to know for a correct reset that no equilibriumBSC exists for a SCC C; as this rises depending on the guessed prefix of the run, we resort to an oracle for coNPC = NPC in the general setting (which proceeds with guess and check for an equilibrium). The NP NP -hardness is shown by a reduction from QBF solving.

However, the following setting is tractable for x∈{b, bs} ("small" is bounded by a constant):

Theorem 3 Deciding M, r |=x Ci(a) is in P, if (i) |M| is small, (ii) the input streams Ski are accessed via small-length windows, (iii) bri, mngi, and ACCi(kbi) are in logspace where |ACCi(kbi)| is polynomially bounded, and (iv) any kbi(t′ ) results as mngi(chg, kbi(0)) for some small-size chg.

Simple simulation does not work here. Informally, we can reduce the problem to reachability in a graph in polynomial time, whose nodes describe possible (adorned) states of a run. Further restrictions in (ii) allow to achieve NLSpace.

In the setting above, we have assumed that some algorithm to compute BSi ∈ACCi(kbi) is available. Alternatively, one could assume that, as for locally stable runs, only an oracle for deciding BSi ∈ACCi(kbi) is available. However, tractability gets lost resp. becomes unknown even for deterministic MCS and a LSpace oracle, as variants of integer factorization can be expressed via ACCi(kbi) such that problems in the class UP that are unknown to be in P can be solved.

5.1 Prediction

An important further reasoning task is prediction, i.e., to reason about the future states of an sMCS. We may ask whether M, r′ |=b Ci(a) holds for some extension r′ of r up to a given time point t′ ≥ t, i.e., |r′ |=t′+1 and r′ |≤t =r|≤t; we denote this by M, r |=t′ x Ci(a), for x ∈ {b, bs}. Then

Proposition 5 Deciding M, r|=t′ bsCi(a) is in NExpTimeC and deciding M, r|=t′ b Ci(a) isNExpTime-complete.

A witnessing model s for a suitable extension r′ of r is exponentially bounded in t′ , which can be guessed and verified. For locally stable runs, an SCC C has single exponential many candidate equilibria BSC, which can be checked with the C oracle one by one; this yields NExpTimeC membership. The NExpTime-hardness is via a Turing machine encoding.

Whether M, r |=t′ x Ci(a) holds for some arbitrary t′ ≥t, denoted by M, r |=∞x Ci(a), is clearly undecidable. This is because (U1) the local KBs and (U2) the data streams can increase unboundedly; (U3) pathologic window functions w(S, t) resp. management functions mngi({op(t)}, kbi) can exploit the time argument t to run unbounded computations.

Decidability thus requires tailored restrictions; without specific logics and contexts, the (traditional) generic nature of MCS permits only abstract computational conditions.

The following assumptions are practical: for (U1), the size of each kbi(t′ ) is polynomial in |kbi(0)| (this limits storing actual time stamps in kbi); for (U2), the bridge rules use windows to recent input; and for (U3), absolute time t to evaluate window resp. management functions is not crucial.

Capturing the latter is nonobvious, as time should still play a role for evaluating windows and storing data in the kbi. Fortunately, we can identify benign practical conditions.

A window function w(S, t) is regular, if (i) w(S, t)(t′ ), i.e., the data in the window w(S, t) at time t′ , depends only on S from t′ , t′+1 etc. onwards, and (ii) for some l ≥ p ≥ 0 polynomial in |kbi(0)|, we have w(S, t) = w(S′ , t + p) for every time t and streams S, S′ that coincide on the past (future) l time points around t resp. t+p having data. Informally, (i) enables us to drop past data; in (ii), p reflects that w is periodic and l is a limit for evaluation. Time-based but also other common windows (e.g., based on tuples) are regular.

However simply memorizing the data within the limit with their actual time points is not feasible under a space constraint wrt. |kbi(0)|. For schematic bridge rules as in the running example, where time reference is confined to the evaluation time (⊞0@Z⊤), or with a fixed offset os to it (Z±os), which we call plain, this can be avoided.

Lemma 1 If bri is plain and any window occurring in it is regular, a sufficient fragment of each input stream Ski to evaluate br i can be maintained in polynomial space.

We consider each Ci has only timeless operators, schematic operators have only few (constantly many) variables.

Theorem 4 Deciding M, r |=µx Ci(a) is PSpace-complete for µ∈{t′ ,∞}, if (i) each kbi always has polynomial size, (ii) context evaluation (i.e., of bri, mngi, ACCi) is in polynomial space, and (iii) all bridge rules bri are plain.

Informally, the problems are in PSpace as a witnessing model s can be stepwise guessed and verified by simulating a run in polynomial space, using windows on the various streams. Equilibrium computation is also feasible in polynomial space. PSpace-hardness is immediate by a Turing machine encoding. We note that the results above are unaffected if one changes from the setting with an algorithm to compute some BSi ∈ ACCi(kbi) to an oracle for BSi ∈ ACCi(kbi) in PSpace.

6 RelatedWork

As already mentioned, rMCS [Brewka et al., 2014], eMCS [Goncalves et al., 2014] and aMCS [Ellmauthaler and P¨uhrer, 2015] define semantics via sequential application of static logics on stepwise evolving KBs and observations; rMCS and eMCS can model logical time, which synchronously increases if a global equilibrium is reached; hence neither computation nor transfer time is considered, different from the asynchronous model of sMCS. Asynchrony in aMCS is due to peculiar output rules and controllers (abstract components to handle computation and transfer times) which decide when computation starts at a context.

Streaming bridge rules with window operators as first-class citizens equip sMCS with light-weight, dedicated stream reasoning. To emulate this feature, rMCS, eMCS would require non-trivial extensions in either bridge rules or the local logic:

· To do it on the bridge rules, exchanged beliefs first need to be tagged with timestamps, that is, ordinary MCS beliefs of the form b(c) should now be b(c, t) where t represents a timestamp. Streaming atoms with time-based window operators of the form (i : ⊞k b(c)) in sMCS can be emulated by an auxiliary bridge rule:

where o is a special observation that sends out the clock ticks at every time point.

For tuple-based window operators [Beck et al., 2015], a more involved translation with three auxiliary bridge rules are required [Beck et al., 2017].

Moreover, this approach requires rMCS, eMCS to split bridge rules into two kinds: those whose heads are imported to the local KB and those whose heads are just used to emulate the window operators (thus called auxiliary bridge rules). This creates further complication in defining the applicability of bridge rules, and somehow departs from the original idea of bridge rules as a means for quick filtering of neighbor beliefs into contexts.

· Another approach is to keep bridge rules as in rMCS, eMCS, but introduce the windowmechanism in the local logic. This works straightforwardly with ASP semantics as one can simply take e.g. contexts with LARS [Beck et al., 2015] as the local logic. However, for other logics such as description logics, an extension with window operators has not been investigated and is non-trivial. In other words, this approach is limited in the sense that not every existing logic can be readily put in such as streaming setting. It also interferes with the local logic of the contexts, which departs from the principle of MCS to keep the setting as abstract as possible.

Still, the capacity of management functions can be exploited to do the stream handling. However, from the implementation point of view this approach pushes all functionalities into the contexts; having window operators at the bridge rule level separates streaming features from reasoning features into different layers of an architecture. This makes implementing and maintaining sMCS easier, and moreover stream management (as needed e.g. in local equilibrium computation, or when contexts are busy) can be done more transparently and effectively.

Finally, we have provided feedback equilibria and local stability, which have no counterpart in related MCS extensions.

Clearly scenarios similar to the running example can be modeled as multi-agent systems. However, one will need to specify a suitable negotiation protocol among agents to achieve an equilibrium. The ensuing communication need and effort can be saved with an sMCS, as obtaining a (local) equilibrium is provided as primitive at a low level in the system.

Ameloot et al. [2015] used distributed Datalog under stable model semantics to describe the semantics of distributed systems (e.g., replicated databases) with asynchronous communication of indefinite delay between nodes, which are modeled as stratified datalog programs on fact bases. They gave an operational counterpart and refined the Dedalus approach [Alvaro et al., 2010]. However, neither streaming aspects (e.g., windowing) were an issue, nor heterogeneity (e.g., KB semantics with multiple possible outputs); furthermore, no equilibria were considered. Alternatively one can model (distributed) state transition systems using temporal logics and assess properties via model checking. However, temporal logics are typically propositional; thus efficient modeling of sMCS in them with its features of (arbitrary) window operators, local KBs in expressive logics, asynchronous computation and feedback equilibria is a challenging issue, and remains for future work.

7 Conclusion

We have introduced streaming MCS as an extension of managed MCS with window operators as first-class citizens in the bridge rules. sMCS have a run-based semantics that accounts for asynchronous, distributed execution. For this setting, we defined the notion of equilibria, a central and key notion in MCS which has not been investigated in aMCS. We have presented the complexity of reasoning in sMCS: ad-hoc query answering is NP-complete while prediction is PSpace-complete in relevant settings, but undecidable in general.

For future work, we would like to (i) explore other refined notions of feedback equilibria, for example, equilibria that can be constructively computed in an operational way, (ii) study uniformed complexity of reasoning with sMCS, (iii) implement a prototype of sMCS based on the DMCS system [DaoTran et al., 2015] for MCS evaluation, and (iv) investigate the transferability of some notions (computation/transfer time, feedback equilibria) into the aMCS framework.

Acknowledgment

We are grateful to the reviewers for their comments, which helped to improve this paper.