Stream Reasoning with LARS

Stream reasoning [7, 10] emerged from stream processing [2] to add logic-oriented features on top of processing continuously changing data. The approach of the influential continuous query language (CQL) [1], which can be seen as extension of SQL for streams, is to first obtain windows, i.e., recent snapshots of streaming data, and then execute queries as on a database. This principle has been adopted, e.g., in the Semantic Web area to extend static queries for streams [3, 12]. In Knowledge Representation and Reasoning (KR) some recent works (e.g. [9, 11]) have addressed incremental reasoning. However, prior to our work, no language extension of Answer Set Programming (ASP; see this issue) for stream reasoning with windows was proposed.

In contrast to temporal reasoning as in Linear Temporal Logic (LTL), which deals with reasoning about infinite sequences of states, LARS [5] places finite streams and windows at the conceptual core. We model a stream S as a pair \((T,\upsilon )\) of a timeline T, which is a closed interval in the natural numbers, and an evaluation function  \(\upsilon\) that maps each \({t \in T}\) to a (possibly empty) set of atoms, i.e., expressions of form \(p(c_1,\dots ,c_n)\) where p is a predicate and \(c_1,\dots ,c_n\) are constants (\(n \ge 0\)). A window function w takes a stream S and a time point \({t \in \mathbb {N}}\) and returns a substream w(S, t) of S called a window. For instance, consider a stream \({S=([0,500],\upsilon )}\), where \({\upsilon (485)=\upsilon (490)=\{ x \}}\) and \(\upsilon (t)=\emptyset\) for all other time points t. A (sliding) time-based window of size 10, applied on S at time 500 yields the window \(([490,500], \upsilon )\), which is also obtained by a tuple-based window of size 1.

LARS formulas extend propositional logic, in particular by window operators , where w is a generic window function. A formula \(\varphi\) is evaluated on a stream S at a time t, where \(\varphi\) means that the evaluation of \(\varphi\) is restricted to the window w(S, t). In contrast to a CQL-style snapshot semantics that drops timestamps of selected data, LARS offers some control: \(\Diamond \varphi\) (resp. \(\Box \varphi\)) holds if \(\varphi\) holds at some (resp. every) time point, and \(@_{t}\varphi\) holds if \(\varphi\) holds at time t in the window.

LARS programs are sets of rules \(\varphi _0 \leftarrow \varphi _1,\dots ,\varphi _n\), where each \(\varphi _i\) is a formula; variables are viewed as schematic placeholder for concrete (ground) values. The following program \(P\) describes a simple cooling system that must keep the temperature below 7 degrees, where atom s(V) stands for a temperature with value V.Rule (1) abstracts away the specific value: for every second T during the last 60, we associate atom high with T if there is a temperature signal s(V) with \({V> 7}\). Rule (2) then triggers cooling if the temperature has always been high in that interval. Finally, Rule (3) infers a warning if one of the last 5 signal values was above 12.

Semantically, LARS programs can be seen as extension of ASP for streams, thus carrying over attractive features like minimal model reasoning, nonmonotonicity and recursion. The closed world assumption (as in databases) allows for reasoning based on the absence of data; in general, the stable model semantics then leads to multiple models. This makes LARS applicable for scenarios which require the generation of alternative solutions like in planning, diagnosis or configuration.

Satisfiability and model checking are in ground LARS PSPACE-complete (for tractable window functions), but in practical settings not harder than in ground ASP. In contrast to LTL, ground LARS programs with time windows yield the full class of regular languages; nonground programs can express also intractable languages.

Besides foundational aspects beyond the scope of this note, we developed Ticker [6], a prototypical stream reasoning engine that comes with two reasoning modes for LARS programs with the above sliding windows.¹

The first mode repeatedly calls the ASP solver Clingo [8] based on a translation. The second, more efficient mode is incremental; it uses truth maintenance systems to adjust the model of a dynamically updated ASP encoding. In Ticker syntax, the above program P reads:The Laser engine [4] is geared for programs with unique models to achieve high performance, by managing incrementally substitution tables using temporal information. Laser was shown to be significantly faster than C-SPARQL, CQELS or Ticker/Clingo in comparable operations, using Python with PyPy 5.8.²

In conclusion, LARS is a framework that extends ASP for stream reasoning with an emphasis on generic windows. Algorithmically, frequently changing data calls for incremental reasoning, as exemplified in the prototype engines Ticker and Laser. Further and future work includes the use of LARS in applications like network management and dynamic reconfiguration.