=Paper=
{{Paper
|id=Vol-1193/paper_47
|storemode=property
|title=A Stream-Temporal Query Language for Ontology Based Data Access
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_47.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/OzcepMN14
}}
==A Stream-Temporal Query Language for Ontology Based Data Access==
<pdf width="1500px">https://ceur-ws.org/Vol-1193/paper_47.pdf</pdf>
<pre>
         A Stream-Temporal Query Language for
              Ontology Based Data Access?

              Özgür L. Özçep, Ralf Möller, and Christian Neuenstadt

                       Institute for Softwaresystems (STS)
                        Hamburg University of Technology
                               Hamburg, Germany
         {oezguer.oezcep,moeller,christian.neuenstadt}@tu-harburg.de



        Abstract. The paper contributes to the recent efforts on temporalizing
        and streamifiying ontology based data access (OBDA) by discussing as-
        pects of rewritability, i.e., compilability of the TBox into ontology-level
        queries, and unfoldability, i.e., transformability of ontology-level queries
        to queries on datasource level, for the new query-language framework
        STARQL. The distinguishing feature of STARQL is its general stream
        windowing and ABox sequencing strategy which allows it to plugin well
        known query languages such as unions of conjunctive queries (UCQs)
        in combination with TBox languages such as DL-Lite and do temporal
        reasoning with a sorted first order logic on top of them. The paper dis-
        cusses safety aspects under which STARQL queries that embed UCQs
        over DL-Lite ontologies can be rewritten and unfolded to back-end re-
        lational stream query languages such as CQL. With these results, the
        adoption of description logic technology in industrially relevant applica-
        tion areas such as industrial monitoring is crucially fostered.

        Keywords: streams, OBDA, monitoring, unfolding, safety


1     Introduction
The work described in this paper is part of recent efforts on streamifying OBDA
[12,6,7,18] and, to some extent, also temporalizing OBDA [5,4]. Streams, as po-
tentially infinite sequences of elements, cannot be processed as a whole. Hence
blocking operators such as the classical grouping operator and aggregation oper-
ators cannot be applied to it. The simple but fundamental idea of circumventing
this problem is to apply on streams a (small) window the content of which is
updated as new elements from the stream arrive at the query answering system.
    Stream window operators play an important role also in the new query lan-
guage framework STARQL (Streaming and Temporal ontology Access with a
Reasoning-based Query Language, pronounced Star-Q-L, [17,16]). Its framework
character relies in the facts that 1) it can embed queries of various query lan-
guages, 2) refer to ontologies in various DL languages, and 3) use a first order
?
    This work has been supported by the European Commission as part of the FP7
    project Optique.
logic (FOL) fragment for temporal reasoning over ABox sequences constructed
within the query. In this paper, we focus on the latter aspect assuming for the
first two unions of conjunctive queries (UCQs) w.r.t DL-Lite ontologies.
    In STARQL, the idea of processing over windows is pushed further by ex-
tending these with sequencing operators that set up at every time point a finite
sequence of ABoxes on which temporal reasoning can be applied. STARQL does
not assume a stream of ABoxes which hold universally but rather modifies/ex-
ploits the given ABox streams to build its own stream of finite ABox sequences.
This sequencing strategy, among other things, distinguishes STARQL from the
approaches in [12,6,7,18]. It is a natural addition to the window operators that
sets up at every time point a context in which temporal reasoning can be applied.
    In this paper, we consider an instantiation of STARQL where Intra-ABox
reasoning within sequences is handled by answering UCQs over DL-Lite ontolo-
gies w.r.t. the certain answer semantics. (Which logic from the DL-Lite family
to choose does not matter, as long as it allows for FOL rewriting.) Within Inter-
ABox reasoning certain answers from the different ABoxes are related and con-
strained with an outer temporal FOL formula. This is challenging if one allows
in the FOL template negation, disjunction and all quantifiers in combination
with concrete domains, as these, if not constrained, would immediately lead to
infinite sets of answers, in particular w.r.t. concrete domain values.
    STARQL uses a new adornment technique for variables to guarantee safe-
ness. We demonstrate the safety mechanism which will guarantee that the FOL
template language is domain independent [1] and as such can be rewritten as
SQL query. This opens the door for (rewriting and) unfolding STARQL queries
into queries of domain independent languages such as the relational stream query
language CQL [3]. Based on CQL, practical systems have been developed. Thus,
this paper provides the foundation for expressive ODBA stream querying.


2   The STARQL framework

We describe the syntax and the semantics for a fragment of STARQL (see [17]
for the full version).
    Our running example for illustration purposes is a measurement scenario in
which there is a (possibly virtual) stream SMsmt of ABox assertions. Its initial
               ≤5s
part, called SMsmt   here, contains timestamped ABox assertions giving the value
of a temperature sensor s0 at 6 time points starting with 0s.
           ≤5s
          SMsmt = {val (s0 , 90◦ )h0si, val (s0 , 93◦ )h1si, val (s0 , 94◦ )h2si
                      val (s0 , 92◦ )h3si, val (s0 , 93◦ )h4si, val (s0 , 95◦ )h5si}

Assume further, that a static ABox contains knowledge on sensors telling, e.g.,
which sensor is of which type. In particular, let BurnerT ipT empSens(s0 ) be in
the static ABox. Moreover, let there be a pure DL-Lite TBox with additional
information such as BurnerT ipT empSens v T empSens saying that all burner
tip temperature sensors are temperature sensors.
     We want to formalize the following information need: Starting with time point
0s, output every second those temperature sensors whose value grew monotoni-
cally in the last 2 seconds. A possible STARQL representation of the information
is illustrated in the following listing.
CREATE STREAM S_out AS
CREATE PULSE AS START = 0s , FREQUENCE = 1 s
SELECT { ? s rdf : type MonInc } < NOW >
FROM S_Msmt [ NOW -2 s , NOW ] - >1 s
USING    STATIC ABOX < http :// Astatic > , TBOX < http :// TBox >
WHERE { ? s rdf : type TempSens }
SEQUENCE BY StdSeq AS SEQ
HAVING FORALL i < j IN SEQ ,? x ,? y :
 IF ({ ? s val ? x } <i > AND { ? s val ? y } <j >) THEN ? x <= ? y




Syntax The example demonstrates much of the syntactical possibilities within
STARQL whose grammar is sketched in Fig. 1. The rules for the HAVING clause
are not given there but are discussed in more in the following sections.
    After the create expressions for the stream and the output frequency the
queries’ main contents are captured by the select expressions. The head of the
select expression describes the output format of the stream giving a RDF basic
graph pattern (BGP) with an attached time expression, here < N OW >, for
the evolving time. The general motivation for this approach is similar to the
CONSTRUCT operator in the SPARQL query language. So the actual result in the
monotonicity example is a stream of ABox assertions of the form M onInc(s0 )hti.
 ≤5s
Sout = {M onInc(s0 )h0si, M onInc(s0 )h1si, M onInc(s0 )h2si, M onInc(s0 )h5si}

Within the WHERE clause one can bind variables w.r.t the KBs mentioned in the
USING clause by using UCQs. We assume an underlying DL-Lite Logic for the
static ABox, the TBox and the UCQs which allows for concrete domain values,
e.g. DL-LiteA [8]. In this example, instantiations of the sensors ?s are fixed w.r.t
to a static ABox and a TBox given by URIs.
    The heart of the STARQL queries is the window operator in combination with
the sequencing mechanism. In the example, the operator [NOW-2s, NOW]->1s
describes a sliding window operator, which collects the timestamped ABox as-
sertions in the last two seconds and then slides 1s forward in time. Every tempo-
ral ABox produced by the window operator is converted to a sequence of (pure)
ABoxes. At every time point, one has a sequence of ABoxes on which temporal
(state-based) reasoning can be applied. This is realized in STARQL by a sorted
first order language template in which timestamped UCQs conditions (notated
here as BGP) are embedded. In the example above, the HAVING clause expresses
a monotonicity condition stating that for all values ?x that are values of sensor
?s w.r.t the ith ABox and for all values ?y that are values of the same sensor ?s
w.r.t. the j t h ABox, it must be the case that ?x is less than or equal to ?y.
          createExp −→ CREATE STREAM name AS [pulseExp] selectExp | pulseExp
           pulseExp −→ CREATE PULSE AS START = startTime, FREQUENCE = freq
           selectExp −→ SELECT selectHead(x, y) FROM listWinStreamExp
                         [USING listOfRessources] WHERE whereClause(x)
                         SEQUENCE BY seqMethod [HAVING safeHavingClause(x, y)]
    selectHead (x, y) −→ sparqlTriple(x, y) <time 1 > . {selectHead (x, y) <time 2 > }
  listWinStreamExp −→ (name | selectExp)windowExp[ , listWinStreamExp]
         windowExp −→ [ timeExp1 , timeExp2 ]->slideConst
    listOfRessources −→ typedRessourceList[ , listOf Ressources]
 typedRessourceList −→ STATIC ABOX listofURIstoStaticABoxes |
                         TEMPORAL ABOX listofURIstoTemporalABoxes |
                         TBOX listofURIstoTBoxes
    whereClause(x) −→ Ψ (x)      (with Ψ (x) a UCQ with distinguished variables x)
         seqMethod −→ StdSeq | SeqMethod (∼)


              Fig. 1: Syntax for STARQL (without HAVING clauses)


Semantics STARQL queries have streams of ABox assertions as input and
output. That means that the definition of the semantics for STARQL has to
explicate how the output stream of ABox assertions is computed from the in-
put streams. Using the compositionality principle, the semantics definition for
SPARQL can be accomplished by defining the semantic denotations for the sub-
structures of the query (be it subqueries or other data structures) and then by
composing them to the denotation of the whole query. We are going to sketch the
semantics of the window operator, of the sequencing, and of the HAVING clause.
    A stream of ABox assertions is an infinite set of timestamped ABox as-
sertions of the form axhti. The timestamps stem from a flow of time (T, ≤)
where T may even be a dense set and where ≤ is a linear order. Let S be
a stream name with its denotation JSK being such a stream of timestamped
ABox assertions. We declare the denotation of the windowed stream ws =
S winExp = S [timeExp1 , timeExp2 ]->sl as a stream of temporal ABoxes,
where a temporal ABox is a set of timestamped assertions.
    Let λt.g1 (t) = JtimeExp 1 K and λt.g2 (t) = JtimeExp 2 K be the functions corre-
sponding to the time expressions. The pulse declaration defines a subset T 0 ⊆ T
of the time domain. T 0 is the set of timestamps of the stream of temporal ABoxes
JwsK. Let T 0 be represented by the increasing sequence of timestamps (ti )i∈N ,
where t0 is the starting point fixed in the pulse declaration.
    Now, one defines for every ti the temporal ABox Ãti such that (Ãti , ti ) ∈
JwSK. If ti < sl − 1, then Ãti = ∅. Else set first tstart = bti /slc × sl and
tend = max{tstart − (g2 (ti ) − g1 (ti )), 0}, and define on that basis
              Ãti = {(ass, t) | (ass, t) ∈ JSK and tend ≤ t ≤ tstart }
So in the example above, timeExp 1 = N OW − 2s, timeExp 2 = N OW and
sl = 1s; the example’s results for second 4s and 5s are the following.
            Time Temporal ABox
            4s   {val (s0 , 94◦ )h2si, val (s0 , 92◦ )h3si, val (s0 , 93◦ )h4si}
            5s   {val (s0 , 92◦ )h3si, val (s0 , 93◦ )h4si, val (s0 , 95◦ )h5si}
If the STARQL query refers to more than one stream, than these are joined
by timewise union of the temporal ABoxes of the windowed streams, which is
possible as the pulse declaration synchronizes all streams of temporal ABoxes.
    The stream of temporal ABoxes is the input for the sequencing operator
which produces for every time point of the pulse a sequence of (pure) ABoxes.
The sequencing methods used in STARQL refer to an equivalence relation ∼ to
specify which assertions go into the same ABox. The equivalence classes [x]∼
for x ∈ T form a partition of T . We restrict the class of admissible equivalence
relations tho those ∼ that respect the time ordering, i.e., the partition of ∼
equivalence classes should be convex intervals on the time domain.
    Now, we define the sequence of ABoxes generated by seqM ethod(∼) on the
stream of temporal ABoxes as follows: Let (Ãt , t) be the temporal ABox at t.
Let T 0 = {t1 , . . . , tl } be the time points occurring in Ãt and let k the number of
equivalence classes generated by the time points in T 0 . Then define the sequence
at t as (A0 , . . . , Ak ) where for every i ∈ {0, . . . , k} the pure ABox Ai is
            Ai = {axht0 i | axht0 i ∈ Ãt and t0 in ith equivalence class}
In the example above, the equivalence is the identity (keyword StdSeq for stan-
dard sequencing), so that the resulting sequence of ABoxes at time point 5s is
trivial as there are no more than two ABox assertions with the same timestamp:
{val (s0 , 92◦ )}h0i, {val (s0 , 93◦ )}h1i, {val (s0 , 95◦ )}h2i.
    STARQL’s semantics for the HAVING clauses relies on the certain answer
semantics (see [8]) for the embedded UCQs. The idea is to view the tuples in
the certain answer sets as members of a sorted FOL structure It . Assume that
the sequence of ABoxes at some given time point t is seq = (A0 , . . . , Ak ). Then
the domain of It consists of the index set {0, . . . , k} as well as the set of all
individual constants and all value constants of the signature. Now, if the HAVING
clause contains, for example, the state tagged condition query val(s, x)hii (with
embedded UCQ val(s, x)), then we introduce for it a ternary relation symbol R
and replace val(s, x)hii by R(s, x, i) in the HAVING clause. This symbol is denoted
in It by the certain answers of the embedded query extended with the index i:
RIt = {(a, b, i) | (a, b) ∈ cert(val(s, x), Ai ∪ Astatic ∪ T )}. Constants are denoted
by themselves in It . This already fixes a structure It with finite denotations of
its relation symbols. The evaluation of the HAVING clause is then nothing else as
evaluating the FOL formula (after the substitutions) on the structure It .

3    A Safe Fragment for HAVING clauses
As demonstrated with the monotonicity example, STARQL allows a sorted FOL
to reason on the ABox sequences. The semantics for the HAVING clauses rests on
the structure It whose domain ∆It does not consist only of the individual and
value constants in the interpretations of the relations, the so called active domain
according to database terminology [1], but the whole set Dom of individual
constants, value constants and the indices produced in the sequencing. With a
safety mechanism on the HAVING clause it can be guaranteed that the evaluation
of the HAVING clause on the ABox sequence depends only on the active domain.
    Figure 2 contains the grammar for the HAVING clause language with its safety
mechanism realized by variable guards/adornments. The safe having clauses (de-
noted by safeHavingClause, which is the start symbol of the grammar) contain
only those variables for individuals that have guard status +. We illustrate the
meaning of the rules with Rule (1) for the OR case and then go in more detail
w.r.t. adornments.
                              1   2              1              2
                      hCl (z g ∨g ) −→ hCl (z g ) OR hCl (z g )                      (1)

A having clause hCl may be constructed as (produces) a disjunction of two
having clauses under some conditions on the variables occurring in them. If
during production a clause hCl (z g ) with variables z and some adornment g for
                                                                        1              2
them is reached, then Rule (1) justifies the production of hCl (z g ) OR hCl (z g )
                                                         1    2
if the adornment g can be represented as g = g ∨ g , i.e., if g is the result of
applying a function ∨ on the adornment lists g 1 , g 2 .
    The adornments g = g1 , . . . , gn are lists of guard status gi (g-status for short),
where gi ∈ {+, −, −−, ∅}. We use z g as an abbreviation for z1g1 , . . . , zngn where
z = z1 , . . . , zn and g = g1 , . . . , gn . We assume the ordering ∅  −−  −  +
on the guards. This ordering is relevant for the calculation of gmax in the rule
of Fig. 2 where the clause is constructed from an arbitrary clause hCl and an
identity atom. The special case of gi = ∅ is a convenience notation meaning for
x∅ that x does not occur at all in the formula.
    The meanings of the functions ¬, ∨, ∧, → over vectors of g-status are fixed
by the tables in Figure 3. Combinations with the g-status ∅ is handled in
an extra table 3b. So for example, assume that one has produced a HAVING
clause F (x−−        +   −
               1 , x2 , x3 ), where x1 has g-status −−, x2 has g-status +, and x3
has g-status −. Then rule (1) and the tables allow, e.g., the production of
F1 (x−−      +     −           +     +     ∅
     1 , x2 , x3 ) OR F2 (x1 , x2 , x3 ). Let us verify this for the variable x1 : Its g-
status −− in F1 and its g-status + in F2 combines to the g-status −− = − − ∨+
in F—according to the entry for the pair (−−, +) in the table of ∨.
    Now, we will show how to transform HAVING clauses to the relational algebra
(SQL). In particular this will show that the HAVING clause language is domain
independent as relational algebra is domain independent. For a formula F let
SRN F (F ) be the formula in safe range normal form (SRNF) [1, S.85] resulting
from applying the following normalization rules
 – Rename variables such that no variable symbol occurrence is bound by dif-
   ferent quantifiers and such that no variable occurs bound and free
 – Rewrite IF F THEN G to NOT F OR G.
 – Eliminate double negations
 – Eliminate FORALL quantifiers by FORALL z ; NOT EXISTS z NOT.
        safeHavingClause(z) −→ hCl(z + )                (for z ∈ V arval ∪ V arind )


                      term(i+ ) −→ i
                         term() −→ max | 0 | 1
           stateAtom(y + , i+ ) −→ Ψ (x, y) <i>
                                          (for a UCQ Ψ (x, y) and
                                          x ⊆ X, y ⊆ V arind ∪ V arval \ X)
       stateAtom(x−− , y −− ) −→ x = y               (for y, x ∈
                                                               / X ∪ V arval )
                               +
               stateAtom(x ) −→ x = a | a = x
                                          (for a ∈ (X ∩ V arind ) ∪ Constconst , x ∈ V arind \ X)
                    vAtom(z1+ ) −→ z1 = v | v = z1
                                  (for z1 ∈ V arval \ X and v ∈ Constval )
                           +
                    vAtom(z1 ) −→ z1 = z2 | z2 = z1
                              (for z1 ∈ V arval \ X, and z2 ∈ X ∩ V arval )
                  −−   −−
           vAtom(z1 , z2 ) −→ z1 op z2
                                          (for op ∈ {<,<=, >, >=, =}; z1 , z2 ∈ V arval \ X)
                  vAtom(z1−− ) −→ z1 op z2             (for op ∈ {<,<=, >, >=}, z1 ∈ V arval \ X,
                                                        z2 ∈ V alconst ∪ (X ∩ V alvar )
    stateArithAtom(ig11 , ig22 ) −→ term1 (ig11 ) op term2 (ig22 )
                                          (for op ∈ {<,<=, =, >, >=})
stateArithAtom(ig11 , ig22 , ig33 ) −→ plus(term1 (ig11 ), term2 (ig22 ), term3 (ig33 ))


                       hCl (z g ) −→ stateAtom(z g ) | vAtom(z g ) | stateArithAtom(z g )
                           1    2                1                 2
                  hCl (z g ∨g ) −→ hCl (z g ) OR hCl (z g )
                           1    2                1                     2
                  hCl (z g ∧g ) −→ hCl (z g ) AND hCl (z g )               (both conjuncts are
                                          not of form x = y for x, y ∈ V arind ∪ V arval )
     hCl (z1gmax , z2gmax , z3 g3 ) −→ hCl (z1g1 , z2g2 , z3 g3 ) AND z1h1 = z2h2
                                          (for gmax = max{g1 , g2 , h1 , h2 })
                               ¬g
                      hCl (z        ) −→ NOT hCl (z g )
                          1     2                      1                   2
                  hCl (z g →g ) −→ IF hCl (z g ) THEN hCl (z g )
                          1     2                                  1                       2
                  hCl (z g →g ) −→ FORALL y IF hCl (z g , y + ) THEN hCl (z g , y g )
                           1    2                              1                    2
                  hCl (z g ∧g ) −→ EXISTS y hCl (z g , y + ) AND hCl (z g , y g )


Fig. 2: Grammar for HAVING clauses
(the set of variables X is the set of variables that are bounded by the WHERE
clause in the STARQL query)
  g1 g2 ¬g1 g1 ∧ g2 g1 ∨ g2 g1 → g2
  −− −− −− −−         −−      −−
  −− − −− −−           −       −
  −− + −− +           −−      −−                g1 g2 g1 ∧ g2 g1 ∨ g2 g1 → g2
  − −− + −−            −      −−
                                                −− ∅    −−      −−      −−
  − − +        −       −       −
                                                 − ∅     −       −      −−
  − + +        +       −       +                 + ∅     +      −−       −
  + −− −       +      −−       −                 ∅ −− −−        −−      −−
  + − −        +       −       −                 ∅ −     −       −       −
  + + −        +       +       −                 ∅ +     +      −−      −−

(a) Variables existent in both subformulas   (b) Variable missing in one subformula

                          Fig. 3: Combination of Guards


 – Push NOT through using de Morgan rules
Please note that these rules are applied in some order until they cannot be
applied anymore. A formula F is said to be in SRNF iff F = SRN F (F ).
    Domain independence for formulas in SRNF are handled in the literature [1]
also by a guard concept. This is realized by a function rr as follows. (Note that
we use set operations on lists of variables in the canonical way.)
1. rr(r(t1 , . . . , tn )) = variables in t1 , . . . , tn .
2. rr(x op y) = ∅ for x, y ∈ V arval , op ∈ {<, >, ≤, ≥}
3. rr(x op v) = rr(x op v) = ∅ for x ∈ V arval , v ∈ Constval , op ∈ {<, >, ≤, ≥}
4. rr(x = a) = rr(a = x) = {x} (for x ∈ V arval , a ∈ Constval or
                                         x ∈ V arind and a ∈ V arind )
5. rr(F AND G) = rr(F )∪ rr(G)
                                  rr(F ) ∪ {x, y} if rr(F ) ∩ {x, y} =
                                                                     6 ∅
6. rr(F AND (x = y)) =
                                  rr(F )                else
7. rr(F OR G) = rr(F ) ∩ rr(G)
8. rr(NOT F ) = ∅           
                              rr(F ) \ x if x ⊆ rr(F )
9. rr(EXISTS xF ) =
                              return ⊥ else
The definition of rr in [1] are simpler than our adornment technique used in
the grammar because of two main reasons: the authors in [1] assume that the
formula is already in SRNF form, whereas we do not. Moreover, we define the
HAVING clause grammar in the context of the grammar for STARQL queries.
So, we have to take care of variables X that are already bounded by the WHERE
clause. This leads to many sub-cases in our grammar.
    A formula F in SRNF is called range restricted iff f ree(F ) = rr(F ) and
no subformula returns ⊥. A well known theorem states that range restricted
formulas in SRNF are exactly as expressive as relational algebra—which is known
to be domain independent. Hence it is well known that safe range formulas are
domain independent (in particular all sets of answers are finite).
   Relating our set of g-status with the set of g-status used in [1] leads to the
desired theorem.
Theorem 1. All safe HAVING clauses (considered as queries on the DB It of
certain answers within the actual ABox sequence at t) are domain independent.
   Let saf ehCl(u+ ) be a safe HAVING clause. Let saf ehClN F (u) be the for-
mula resulting from applying the SRNF normalization rules. The status of all
the guards are not changed by the rules. Now, we see that for all subformulas
G(x+ , y − , z −− ) in saf ehClN F (u) we have
(*) rr(G) = x (= all variables in G with g-status +)
     The proof of (∗) is by structural induction on construction of the formula
saf ehcLN F (u). Let G(x+ , y − , z −− ) be an atomic clause. Then rr(G) = x
follows from looking at the adornments of the atomic clauses G in Fig. 2 and
checking that only those with g-status + are in rr(G). Hereby, variables x ∈ X,
whereX is defined in the grammar, are treated as constants in the definition of
rr(·). The case of conjunction is clear too as any + g-status combines with any
other g-status to +. Now take negation G = NOT F (x+ , y − , z −− ). The defini-
tion of rr for the negation case says rr(G) = ∅. Actually we know that F is
an atomic formula. Looking at all variables for these formulas in the grammar
we see that no one of these as g-status −, hence actually y = ∅ and we have
G(x− , z −− ), so there is no variable in G with g-status +, hence indeed we get
that rr(G) = ∅ = the variables in G with g-status +. The case for disjunction
is clear as a positive g-status results for a variable in a disjunction only if both
variables exists in the disjuncts and are labelled +. Now the last case is that of
the exists quantifier G = EXISTS xF (x+ , y − , z −− ). According to induction as-
sumption rr(F ) = x. G may result from a transformation of an exists subformula
EXISTS xhCl(x+ , . . . ) AND F 0 in hcl(u+ ). So the variable x is by definition in
the set x of variables in F with g-status +, hence rr(G) = rr(F )\{x}. But G does
not occur as free variable in G, hence the set of variables in G with g-status + is
actually x without x, which proves the induction claim. Now G may also result
from applying somewhere the rule FORALL ≡ NOT EXISTS NOT. But again, there
is a formula with variables that have g-status + and are bounded by the all quan-
tifier so that one gets again a formula of the form EXISTS xhCl(x+ , . . . ) AND F 0 .


4    Unfolding STARQL into CQL
Having shown domain independence for the the HAVING clause language is the
main step towards using STARQL for OBDA in the classical sense according to
which queries on the ontology level are rewritten and unfolded into queries over
the data source. Rewriting is done locally w.r.t. every ABox in the sequence,
resulting in a new STARQL query. Hence we only discuss unfolding.
    We illustrate how to unfold STARQL queries into CQL queries; CQL [3] is
one of the early relational stream query languages having served as a blue print
for many stream query languages even on the ontological level (e.g., [12],[6],[18]).
CQL window operators get as input a stream and produce a temporal relation,
which is a function over the time domain T giving for every t an ordinary (called
instantaneous) relation Rt . The operator RStream gets a temporal relation R
as input and produces a stream of tuples dhti such that d ∈ Rt .
    Following the classical OBDA approach we assume that the streams to which
STARQL refers are produced by mappings. In our example, let be given a
CQL stream of measurements M smt with schema Msmt(MID, MtimeStamp,
SID, Mval). A mapping takes a CQL query over this stream and produces a
stream of assertions of the form val(x, y)hti.

val(x, y)hzi ←−
             SELECT Rstream(f(SID) as x, Mval as y, MtimeStamp as t)
             FROM Msmt[NOW]

    The main challenge for unfolding STARQL is the new data structure of an
ABox sequence, which is not representable in CQL. So we therefore that the
STARQL queries use the standard sequencing only, so that from every state i
in the sequence associated with tN OW one can reconstruct the timestamps of
the tuples occurring in the ABox Ai . Moreover, we assume a default stream-
to-stream operator implemented into the CQL answering system and applied
directly after every window-to-stream operator, transforming dhti to (d, t)hti.
    The CQL query in the following listing is the unfolded pendant of the STARQL
query. The outer WHERE clause is the pendant of the monotonicity formula ex-
pressed in the HAVING clause.
CREATE VIEW windowRelation as
SELECT * FROM Msmt [ RANGE 2 s Slide 1 s ];
SELECT Rstream ( sensor , timestamp )
FROM windowRel , sensorRel
WHERE sensorRel . type = ’’ BurnerTipTempSens ’ ’ AND
NOT EXISTS (
 SELECT * FROM
 ( SELECT timestamp as i , value as x FROM windowRelation ) ,
 ( SELECT timestamp as j , value as y FROM windowRelation )
 WHERE    i < j AND x > y ) ;

Experiments with our STARQL prototype (using a CQL like back end language)
show correctness and completeness for a representative set of STARQL queries.
Performance and scalability experiments are on our TODO list.


5   Related Work

Much of the relevant work on stream processing has been done in the context of
data stream management systems (DSMSs), mainly with SQL-like stream query
languages such as CQL [3] or the ones used in TelegraphCQ [9], Aurora/Borealis
[13], or PIPES [15]. Nevertheless, the stream community is far from having a
query standard for DSMS (see [14] for some ideas).
     First steps towards streamified OBDA are C-SPARQL [12], SPARQLstream
[6], and CQELS [18]. These approaches extend SPARQL with a window operator
whose content is a multi-set of variable bindings for the open variables in the
query. This solution is not without problems. It presupposes mixed interim states
in which the constraints/consequences of the ontologies are faded out. Moreover,
it does not adhere to the requirements of an orthogonal query language. Last
but not least, if one considers KBs that allow for the formulation of persistency
assumptions, then one has to keep track of the time points in the window.
     The semantical foundation of evaluating HAVING clauses is similar to that of
[5], one of the recent approaches to temporalizing OBDA. (Another one is [4]).
The difference is that [5] uses an LTL based language with embedded CQs not
a sorted FOL language. For engineering applications with information needs as
in the monotonicity example the LTL framework is not sufficient, as it does not
provide exists quantifier on top of the embedded CQs.
     Safety conditions are considered in the classical DB literature [1] but also
specifically for temporal DBs [10]. We do not claim novelty w.r.t. safety aspects
but only w.r.t. the new adornment technique which directly operates on the FOL
formulas without transforming them to some normal form.
     Though not directly related to OBDA, other relevant work stems from the
field of complexed event processing. For example, EP-SPARQL/ETALIS [2] uses
also a sequencing constructor; and T-REX with the event specification language
TESLA [11] uses an FOL language for identifying patterns.


6   Conclusion

The paper has presented a query framework lying in the intersection of classi-
cal OBDA and stream processing. The query language (necessarily) extends the
sliding window concepts, which are known from many languages for relational
stream data management systems as well as recent systems for RDFS, with ABox
sequencing constructors. The advantage of using a sequence based methodology
over other approaches are, first, that the sequence sets up a (nearly) standard
context in which standard OBDA reasoning services can be applied, and second,
that the query language can be equipped with a neat semantics based on the
certain answer semantics for pure DL-Lite ABoxes (see [17]). Though the results
in this paper show that ABox sequencing w.r.t. the standard sequencing strat-
egy is syntactic sugar, it is not a redundant operator if non-standard sequencing
strategies are used. For example, in many cases one does not want to handle
(certain) answers over inconsistent ABoxes as these do not result in useful in-
formation. Hence, a non-standard sequencing strategy would only build ABoxes
in the sequence that are consistent, so that only these are queried.
    STARQL’s combination of sufficient expressiveness on the conceptual level
with high expressiveness w.r.t. arithmetical, and statistical computations as well
as event specifications can be implemented in a safe manner in order to reach
domain independence. This lays the ground for a complete and correct transfor-
mation to streaming query languages on the backend data sources.
References
 1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley
    (1995)
 2. Anicic, D., Rudolph, S., Fodor, P., Stojanovic, N.: Stream reasoning and complex
    event processing in etalis. Semantic Web 3(4), 397–407 (2012)
 3. Arasu, A., Babu, S., Widom, J.: The CQL continuous query language: semantic
    foundations and query execution. The VLDB Journal 15, 121–142 (2006), http:
    //dx.doi.org/10.1007/s00778-004-0147-z, 10.1007/s00778-004-0147-z
 4. Artale, A., Kontchakov, R., Wolter, F., Zakharyaschev, M.: Temporal description
    logic for ontology-based data access. In: Proceedings of the Twenty-Third Inter-
    national Joint Conference on Artificial Intelligence. pp. 711–717. IJCAI’13, AAAI
    Press (2013), http://dl.acm.org/citation.cfm?id=2540128.2540232
 5. Borgwardt, S., Lippmann, M., Thost, V.: Temporal query answering in the descrip-
    tion logic dl-lite. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) Frontiers
    of Combining Systems. LNCS, vol. 8152, pp. 165–180. Springer Berlin Heidelberg
    (2013)
 6. Calbimonte, J.P., Corcho, O., Gray, A.J.G.: Enabling ontology-based access
    to streaming data sources. In: Proceedings of the 9th international semantic
    web conference on The semantic web - Volume Part I. pp. 96–111. ISWC’10,
    Springer-Verlag, Berlin, Heidelberg (2010), http://dl.acm.org/citation.cfm?
    id=1940281.1940289
 7. Calbimonte, J.P., Jeung, H., Corcho, O., Aberer, K.: Enabling query technologies
    for the semantic sensor web. Int. J. Semant. Web Inf. Syst. 8(1), 43–63 (Jan 2012),
    http://dx.doi.org/10.4018/jswis.2012010103
 8. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Poggi, A., Rodríguez-
    Muro, M., Rosati, R.: Ontologies and databases: The DL-Lite approach. In: Tes-
    saris, S., Franconi, E. (eds.) Semantic Technologies for Informations Systems –
    5th Int. Reasoning Web Summer School (RW 2009), Lecture Notes in Computer
    Science, vol. 5689, pp. 255–356. Springer (2009)
 9. Chandrasekaran, S., Cooper, O., Deshpande, A., Franklin, M.J., Hellerstein, J.M.,
    Hong, W., Krishnamurthy, S., Madden, S., Raman, V., Reiss, F., Shah, M.A.:
    Telegraphcq: Continuous dataflow processing for an uncertain world. In: CIDR
    (2003)
10. Chomicki, J., Toman, D.: Temporal databases. In: Handbook of Temporal Reason-
    ing in Artificial Intelligence, vol. 1, pp. 429–467. Elsevier (2005)
11. Cugola, G., Margara, A.: Tesla: A formally defined event specification language. In:
    Proceedings of the Fourth ACM International Conference on Distributed Event-
    Based Systems. pp. 50–61. DEBS ’10, ACM, New York, NY, USA (2010), http:
    //doi.acm.org/10.1145/1827418.1827427
12. Della Valle, E., Ceri, S., Barbieri, D., Braga, D., Campi, A.: A first step towards
    stream reasoning. In: Domingue, J., Fensel, D., Traverso, P. (eds.) Future Internet
    – FIS 2008, Lecture Notes in Computer Science, vol. 5468, pp. 72–81. Springer
    Berlin / Heidelberg (2009), http://dx.doi.org/10.1007/978-3-642-00985-3_6
13. Hwang, J.H., Xing, Y., Çetintemel, U., Zdonik, S.B.: A cooperative, self-configuring
    high-availability solution for stream processing. In: ICDE. pp. 176–185 (2007)
14. Jain, N., Mishra, S., Srinivasan, A., Gehrke, J., Widom, J., Balakrishnan, H.,
    Çetintemel, U., Cherniack, M., Tibbetts, R., Zdonik, S.: Towards a streaming sql
    standard. Proc. VLDB Endow. 1(2), 1379–1390 (Aug 2008), http://dl.acm.org/
    citation.cfm?id=1454159.1454179
15. Krämer, J., Seeger, B.: Semantics and implementation of continuous sliding window
    queries over data streams. ACM Trans. Database Syst. 34(1), 1–49 (Apr 2009),
    http://doi.acm.org/10.1145/1508857.1508861
16. Özçep, O.L., Möller, R., Neuenstadt, C.: Obda stream access combined with safe
    first-order temporal reasoning. Technical report, Hamburg University of Technol-
    ogy (2014)
17. Özçep, Ö.L., Möller, R., Neuenstadt, C., Zheleznyakov, D., Kharlamov, E.: Deliv-
    erable D5.1 – a semantics for temporal and stream-based query answering in an
    OBDA context. Deliverable FP7-318338, EU (October 2013)
18. Phuoc, D.L., Dao-Tran, M., Parreira, J.X., Hauswirth, M.: A native and adaptive
    approach for unified processing of linked streams and linked data. In: International
    Semantic Web Conference (1). pp. 370–388 (2011)

</pre>