In this paper we analyze the theoretical aspects of our semantic rule language, SDRL. Inspired with an industrial collaboration, SDRL is designed to process signals from sensors installed in industrial equipment by filtering, aggregating, and combining sequences of time-stamped measurements recorded by the sensors. In our previous work, we conducted extensive experiments showing scalability of the language on real data. Here instead, we analyze theoretical properties of SDRL. In particular, we show that query answering in SDRL can be reduced to relational algebra with aggregations. To this end, we rely on recently introduced Datalognr MTL that is first order rewritable. First we introduce an extension of Datalognr MTL with aggregate functions. Then we show how to translate query answering in SDRL into the query answering in the extended language.
Large engineering and maintenance companies like Siemens typically rely on rule-based
intelligent diagnostics: diagnostic engineers create and use complex diagnostic rule-sets
to detect abnormalities during equipment run time and sophisticated analytical models
to combine these abnormalities with models of physical aspects of equipment such as
thermodynamics and energy efficacy [
An important class of rules that are commonly used in Siemens for rule-based equipment diagnostics are signal processing rules (SPRs). SPRs allow to filter, aggregate, combine, and compare signals, that are time stamped measurement values, coming from sensors installed in equipment and trigger error or notification messages when a certain criterion has been met. Thus, sensors report temperature, pressure, vibration and other relevant parameters of equipment and SPRs process this data and alert whenever a certain pattern is detected. Moreover, SPRs can combine data of two types: master data that contains train engineering specifications, results of previous diagnostic tasks, and diagnostic event data, and operational data that contains recorded signals from sensors installed in equipment. Data processed by SPRs is then used by analytical models in order to ensure safety, efficiency, and to lower the maintenance costs.
SPRs that are currently offered in most of existing diagnostic systems and used in Siemens are highly data dependent in the sense that (i) data about specific characteristics like speed, capacity, and identifiers of individual sensors and pieces of equipment are explicitly encoded in SPRs and (ii) schema of such data is reflected in the SPRs. As a result, for a typical simple train diagnostic task an engineer has to write from dozens to hundreds of SPRs with hundreds of sensor tags, component codes, sensor and threshold values and equipment configurations and design data.
Example 1. Consider the diagnostic task: all door sensors indicate that the car doors are OK, and the main train line pressure is trending upwards for more than 33 seconds.
The above task can be checked by analyzing the train sensors. For instance, let us assume that the locomotive L1 has door sensors SKNF X01, SKNF X02, SKNF X03 and SKNF X04, and let MNPRSS be the sensor that measures the main train pressure. Further, let us assume that the task is verified as OK if the sum of the above sensors values is equal to 16. Then, the following data dependent SPR written in a syntax similar to the one of Siemens SPRs can be used to accomplish the task: $CarDoorsOK = truth (sum (SKNF X01; SKNF X02; SKNF X03; SKNF X04) (1) : value(=; 16) &&trend(MNPRSS; ’up’) : duration(>; 0:33s)) Here $CarDoorsOK is a Boolean variable. Many of these SPRs differ only on specific sensor identifiers and the number of speed signals to aggregate. Adapting these SPRs to another cars will also require to change a lot of identifiers.
Data dependence of SPRs poses significant challenges for diagnostic engineers in (i) authoring, and then (ii) reuse, and (iii) maintenance of SPRs. These challenges are common for large enterprises and Siemens is not an exception.
In our previous work [
We prove that the reasoning tasks in SDRL programs can be rewritten into query answering using linear algebra with aggregates (that is SQL). Further, we analyzed the upper bound of the complexity of our problem. In particular, we measure the complexity of the problem in the size of two main components: the program and the data. We expect, the size of the data largely dominates the size of programs, and while the data can be huge (typically several GBs) that the size of program can be significantly big (e.g., several thousands of rules) thus both measures are relevant. 4
To study the two properties from above, we encode the problem of firing a message
in SDRL into the fact-entailment problem [
Still, DatalognrMTL cannot be immediately related to our language since it does not
support aggregates and some other logic constructs that we need for our encoding (in
particular, functional symbols, negation and aggregates). So first, we extend DatalogMTL
with functional symbols, aggregation, etc. under reasonable restrictions, without increasing
the complexity. Then to show that our problem is rewritable into linear algebra with
aggregates we do the following encoding. Given a program and a message rule r we
create an extended non-recursive DatalognrMTL program ;r and a proposition mr
only such that: fires r iff “entails” mr. A corollary of this gives us (i) that our
language is suitable for OBDA [
In this section, we introduce formally the syntax and semantics of our signal diagnostic processing language, SDRL. To do so, we first introduce signal processing expressions that allow one to manipulate basic signals using mathematical functions. Then we introduce a notion of programs that allow one to compose and combine expressions, and form message rules. Finally, we provide semantics of our language that formally defines how SDRL should be executed. 2.1
We introduce signal expressions that filter and manipulate basic signals and create new more complex signals. Intuitively, in our language we group signals in ontological concepts and signal expression are defined on the level of concepts. Then, a signal processing expression is recursively defined as follows:
C = Q
C agg C1 where C is a concept, Q is a CQ with one output variable, 2 f+; ; ; =g, agg 2 fmin; max; avg; sumg, 2 R, 2 f<; >; ; g, align 2 fwithin; after[t]; before[t]g, t is a period, and direction 2 fup; downg. In the following we will consider well formed sets of signal expressions, that is, sets where (i) each concept is defined at most once and (ii) where definitions of new concepts are assumed to be acyclic: if C1 is used to define C2 (directly or indirectly) then C1 cannot be defined (directly or indirectly) using C2.
Expressions C = Q and C = fs1; : : : ; smg we call basic signal expressions and other we call complex signal expressions.
The formal meaning of signal processing expressions is defined in Table 1. Example 2. The data-driven rules that can be used to determine that car doors function well, as in Equation (1), can be expressed with two concepts in SDRL as follows: DoorsLocked = sum MainCarDoors : value(=; LockedValue)
PressureUp = CabinPressure : trend(’up’) : duration(>; 33sec) (2) (3) Here, MainCarDoors is a CQ defined over a database. For brevity we do not introduce a new concept for each expression but we just join them with symbol “ :”. The constant LockedValue is a parameter for analyzing door of a train, and they are instantiated from the train configuration when the expressions are evaluated. 2.2
We now show how to use signal expressions to compose diagnostic programs and to alert messages.
A diagnostic program (or simply program) is a tuple (S; K; M) where S is a set of basic signals, K a KB, M a set of well formed signal processing expressions such that each concept that is defined in M does not appear in K.
In order to enjoy favorable semantic and computational characteristics of OBDA, we
consider well-studied ontology language OWL 2 QL that formal basis is DL-LiteR [
On top of diagnostic programs SDRL allows to define message rules that report the current status of a system. Formally, they are defined as Boolean combinations of signal processing expressions:
D :=
C j not D1 j D1 and D2: A message rule is a rule of the form, where D is a concept and m is a (text) message: message(m) = D: Example 3. Using Equations (2)–(3) we define the following message: message(“All car doors OK”) = DoorsLocked and PressureUp: The message intuitively indicates that the doors are functioning and locked.
Now we are ready to define the semantics of the rules, expression and programs. 2.3
We now define how to determine whether a program fires a rule r. To this end, we extend first-order interpretations that are used to define semantics of OWL 2 KBs.
Formally, our interpretation I is a pair (IFOL; IS ) where IFOL interprets objects and their relationships (like in OWL 2) and IS —signals. First, we define how both components of I interprets basic signals in S. Formally, SI = fs1I ; : : : ; sIng where IFOL ‘returns’ the signal id, i.e. sIFOL = os and IS ‘returns’ the signal itself, i.e. sIS = s.
Now we can define how I interprets KBs. Interpretation of a KB KI extends the notion of first-order logics interpretation as follows: KIFOL is a first-order logics interpretation K and KIS is defined for objects, concepts, roles and attributes extending SI . That is, for each object o we define oIS as s if o is the id of s from S; otherwise C = Q
C1 C1 : value( ; ) C1 : duration( ; t0) fs1; : : : ; smg agg C1 all signal ids return by Q evaluated over the KB. new signal s0 for each signal s in C1 with fs0 = fs. new signal s0 for each signal s in C1 with fs0 (t) = fs(t) if fs(t) at time point t; otherwise fs0 (t) = ?. new signal s0 for each s 2 C1 with fs0 (t) = fs(t) if exists an interval I s.t.: fs is defined I, t 2 I and size(I) t0; otherwise fs0 (t) = ?. all enumerated signal fs1; : : : ; smg. new signal s0 with fs0 (t) = aggs2C1 fs(t), that is, s0 is obtained from all signals in C1 by applying the aggregate agg at each time point t. new signal s1 from C1 if: exists a signal s2 from C2 that is aligned with s1, i.e., for each interval I1 where fs1 is defined there is an interval I2 where fs2 is defined s.t. I1 aligns with I2. one signal s0 for each signal s in C1 with fs0 (t) = fs(t) if exists an interval I around t s.t.: fs is defined I, and fs is an increasing (decreasing) function on I for direction=up (=down resp.) (o; f?). Then, for a concept A we define AIS = fsIS j osIFOL 2 AIFOL g. Similarly, we define IS for roles and attributes.
Finally, we are ready to define I for signal expressions and we do it recursively following the definitions in Table 1.
We now illustrate some of them. For example, if C = fs1; : : : ; smg, then CI =
fs1I ; : : : ; sImg; if C = Q then CIFOL = QIFOL where QIFOL is the evaluation of Q over
IFOL and CIS = fs j osIFOL 2 QIFOL g, provided that IFOL is a model of K. Otherwise we
define CI = ;. Similarly, we define interpretation of the other expressions.
Firing a Message Let be a program and ‘r : message(m) = C’ a message rule.
We say that fires message r if for each interpretation I = (IFOL; IS ) of it holds
CIFOL 6= ;, that is, the concept that fires r is not empty. Our programs and rules enjoy the
canonical model property, that is, each program has a unique (Hilbert) interpretation
[
In this part we introduce our extension of DatalogMTL . An atom A in extended DatalogMTL is either a comparison (e.g., 0) or defined by the following grammar: A ::= P ( 1; : : : ; m) j > j
A U% A0 j
A S% A0 :A %A j %A
%A j
j j = aggJ i j P ( 1; : : : ; m)K %A Here, P is a predicate, % is an interval in reals, is a term (possibly with functional symbols), agg 2 fmin; max; avg; sumg and brackets J K denote multiset (values can repeat). A DatalogMTL program
is a finite set of rules of the following form: A+
A1 ^ ^ Ak or ?
A1 ^ ^ Ak; where A+ is an atom that does not contain any ‘non-deterministic’ operators %, %, U%, S%, negated atoms, or aggregate operators.
For our purposes it is sufficient to consider non-recursive programs. Informally, that are programs where dependency (direct or indirect) between predicates is acyclic. In fact, it is not trivial to understand how one would even define the semantics of programs with recursion in case of aggregates and negation. So, from now, we only consider extended DatalogMTL programs that are non-recursive.
In DatalogMTL , temporal operators are defined over intervals and they take the form
%, % and U%, which refer to the future, and %, % and S%, which refer to the past
where % is an interval. For example, %A is true at t iff an atom A is true in all points of
an interval % in the future from t, while %A is true at t iff there exists a point in the past
not longer than % from t where A is true. For the complete semantics of the temporal
operators and rules, please see [
A (temporal) data instance is a finite set of facts of the form P (c)@ , where P (c) is a ground atom and an interval. The fact P (c)@ states that P (c) holds throughout the interval . Moreover, we simply write P (c)@t for P (c)@[t; t].
Finally, every satisfiable extended Datalognr MTL program with database D has the canonical (or minimal) model of and D, M ;D. As usual, the most important property of canonical model is that if a fact holds in canonical model then it holds in any other model. 4
We start with an example of the encoding then we show the complete encoding. Example 4 (Example of Encoding). The query in signal processing expression in Examples 2 and 3 can be encoded in a modular way, starting from simpler to more complex expressions. We start with the encoding rules for Example 2. First, we show how to capture the expression “sum MainCarDoors” in (2). For that we use the following rule:
sumJv j MainCarDoors(x); value(x; v)K = v1: Intuitively, the rule introduces a new constant car representing the “aggregated main car door sensor” and assign the average value of all main car door sensors to it. Then, we encode the second part of (2), value(=; LockedValue), using SumMainCarDoors with:
To encode expression (3) in Example 2 we need to use temporal operators. In particular, to encode CabinPressure : trend(‘up’) we need to copy all intervals of a signal in CabinPressure on which the signal is trending up. For that we need universal quantification (“ 8”). This is expressible in Datalog by two rules connected with a negation. First we compute intervals on which a signal is not trending up with the rule: notTrendUpCP(x)
CabinPressure(x); value(x; v1); (0; ](value(x; v2); v1 > v2) Intuitively, formula (value(x; v1); (0; ](value(x; v2); v1 > v2)) evaluates to true for some value v1 at a time point t if there exists an interval of a size at most containing t in which signal x has another value v2 that is smaller than v1. Here, a parameter is a “small” real number and it is typically selected based on the size of signal sampling.
We compute the trending-up intervals by eliminating non-trending-up time points:
CabinPressure(x); :notTrendUpCP(x)
Here, the functional symbol fcp is used to create a new signal identifier for each x. The values of the new signals are the same as originals and they are just copied for each time-point that is “trending up”: value(fcp(x); v)
To encode the construct duration we also need temporal operators. In particular, we encode the construct : duration(>; 33sec) with the rule:
[0;33s] [0;33s] CabinPressureAux(x) Intuitively, the temporal operator [0;33s] selects “an event that lasts for the last 33s”, and the temporal operator [0;33s] selects “an event happens within the last 33s”. The nesting [0;33s] [0;33s] of these two operators selects the whole duration of all the events lasting at least 33s. Similarly as above, the value is transferred with the rule: value(fpu(x); v)
Finally, to encode message firingfrom Example 3 we introduce two propositionals pdl and ppu for concepts DoorsLocked and PressureUp, respectively. In particular, pdl is true if there exists a signal in DoorsLocked that has at least one value. And similarly for ppu. This is encoded with the rules: pdl pup [0;1)DoorsLocked; [0;1)PressureUp; pdl pup [0;1)DoorsLocked; [0;1)PressureUp Here, [0;1) and [0;1) are used to check if DoorsLocked has at least one signal with value in the past or in the future, respectively. Then we encode with the firing a message: message(“All car doors OK”) pdl; pup Let (S; K; M) be an SDRL program. We define a corresponding extended Datalognr MTL program (DS;K; M) where the temporal facts DS;K encodes S and K, and the program M encodes expressions M. In particular, for each basic signal s = (os; fs) in S: – if fs(t) = v we add value(s; v)@t to DS;K, and – if os is an answer of Q over KB K then we add Q(os)@( 1; +1) to DS;K.
We observe that the signals can be encoded as a finite database instance is due to the assumption that signals are step functions.
The program M is constructed from M following the encodings in Table 2. The
encoding is obtained by using a unary predicate C for each signal processing expression
C and a binary predicate value which we describe in the next paragraphs. It is important
to note that these predicates are interpreted not like FO-predicates but using point based
semantics (e.g., C (o) is true or false for a constant o at a given time point t). For detailed
semantics of such rules see [
More formally, for a signal s = (os; fs), the fact C (os) is true at a time point t iff (i) o 2 CI and (ii) fs(t) is a real number. Condition (ii) simplifies the encoding since we do not need to define when a signal does not have a real value at a point; otherwise we have to have the rules that encode the absence of a real value. Further, we use functional symbols, e.g., fC , to generate fresh signal identifier. E.g., for a signal s, fC (os) represents a new signal id obtained from s for the expression C.
To store the value of a signal at a time point we use the predicate value. That is, value(os; v) is true at point t iff fs(t) = v.
The encoding rules for trend(up) and trend(down) are based on intervals. For them we introduce a parameter , a “small” real number, that we use to select an interval around a time point. In theory, such parameter should converge to 0 to indeed check the trend of a real function (in fact, one needs the first derivative), however, in practice we expect that one can select such a priori (e.g., the length of signal sampling since signals are step functions) that is sufficiently small to check the trend of a function for a particular time point.
It is easy to observe that the extended DatalogMTL program is non-recursive. 5
In this part we state the formal properties of the encoding. First we introduce two lemmas that characterize the encodings of auxiliary predicates value, C ’s and propositional pD’s. Then we use them to show the main encoding theorem.
The following lemma establishes the correspondence between a program and auxiliary predicates value and C ’s.
Lemma 1. Let = (S; K; M) be an SDRL program and = (DS;K; M) be the extended DatalogMTL program as defined above. Further, let I be the canonical interpretation for and let M be the canonical interpretation for . Then, for a signal processing expression C and a time point t the following are equivalent: – sI 2 CI and fs(t) = v; – M; t j= C (os) and M; t j= value(os; v).
Proof. The proof (in the both directions of “iff”) is based on induction on the number of rules that are required to generate expression C starting from basis expressions. We show direction “(”. The opposite one can be shown analogously.
Induction Base: In this case, C is defined either with C = Q or C = fs1; : : : ; smg.
Let us assume C = Q, and sI 2 CI and fs(t) = v. Since s is a basic signal, DS;K must contain the fact value(os; v)@t. Moreover K j= Q(os) hence according to the rule Expression C Q fs1; : : : ; smg
C1; C1 : value( ; ) C1 : duration( ; t) C1 : duration(<; t) .
C (fC (x)) C1 (x); : ( [0;t]( [0;t] C1 (x)). value(fC (x); v) C (fC (x)); value(x; v): C (c); value(c; v) v = aggJv1 j value(x; v1); C1 (x)K, where c is a fresh constant, aggJ K is an aggregation operator over bags C (fC (x1)) value(fC (x1); v)
C1 (x1) U[0;1) (: C1 (x1) ^ : C2 (x2)) U[0;t] C2 (x2) :
C (fC (x1)); value(x1; v) C (fC (x1)) value(fC (x1); v)
C1 (x1) S[0;1) (: C1 (x1) ^ : C2 (x2)) S[0;t] C2 (x2) :
C (fC (x1)); value(x1; v) C (fC (x1))
C1 (x1) ^ C2 (x2) S[0;1) (: C1 (x1))
U[0;1) : C1 (x1) : value(fC (x1); v)
C (fC (x1)); value(x1; v): C (fC (x)) C1 (x); : notTrendUpC1 (x) notTrendUpC1 (x) C1 (x); value(x; v1); (0; ](value(x; v2); v1 > v2)
where is a “small enough” positive real number value(fC (x); v) C (fC (x)); value(x; v): C (fC (x)) C1 (x); : notTrendDownC1 (x) notTrendDownC1 (x) value(x; v1); (0; ](value(x; v2); v1 < v2)
where is a “small enough” positive real number value(fC (x); v) C (fC (x)); value(x; v): Encoding of D pD pD pD pD1 ; pD2 : :pD1 : [0;1) C (x): pD [0;1) C (x): message(m) = D message(m)
pD: C (x) Q(x); value(x; v) we have that M; t j= C (os). Since, value(x; v)@t 2 DS;K we also have that M; t j= value(os; v).
Assume now that C = fsi; : : : ; smg and s = si for some i. Then it must be sI 2 CI . Next, let us assume that fs(t) = v. Since s is a basic concept, we have that value(os; v)@t is in DS;K, and thus M; t j= value(os; v). Further, following the encoding rule for C, C (x) value(x; v), we have that M; t j= C (os).
Induction Step: Consider now that C is an expression that is created by other expressions in at most n + 1. For example, let us assume that C C1 : duration( ; t0). Induction step for the other rules can be shown analogously.
We assume that sI 2 CI and fs(t) = v for some t and v. Since C is created from C1 then it must exists s1 such that os = fC (os1 ) and fs1 (t) = v for some interval I that contains t and is longer t0. Since, C1 is created in at most n steps by induction hypothesis we have that M; t j= C1 (os1 ) and M; t j= value(os1 ; v). Now we analyze the encoding rule C (fC (x)) [0;t0] [0;t0] C1 (x). Intuitively, the body of the rule evaluates to true for some x if there exists a time point in the “past” of t (expressed with condition [0;t0]) contained in an interval of size t0 (expressed with condition [0;t0]) such that on that interval C1 (x) is true, i.e, M; t00 j= C1 (x) for all t00 2 I. Since I is such interval for which C1 (os1 ) is true, we have that encoding rule fires and makes C (fS (os)) true at point t, i.e., M; t j= C (fS (os1 )). Furthermore, from the rule value(fC (x); v) C (fC (x)); value(x; v) and the fact that M; t j= C (fS (os1 )); value(s1; v) it holds that M; t j= value(fC (os1 ); v). This concludes the proof.
The following lemma defines a correspondence between a Boolean combinations of signal processing expressions and their encoding rules.
Lemma 2. Let = (S; K; M) be an SDRL program and = (DS;K; M) be the extended Datalognr MTL program as defined above. Further, let I be the canonical interpretation for and M be the canonical interpretation for . Then, for a Boolean combination of signal processing expression D we have that the following is equivalent: DI is true iff
M; t j= pD for any time point t Proof. The proof is based on induction on the size of D.
Induction Base: We assume D = C for complex expression C and assume DI is true. Then there must exists a signal s such os 2 CI which has at least one value v at some time point t. From Lemma 1 we have that M; t j= C (os). Thus, from the encoding rule pD C (x) we have that M; t j= pD.
Induction Step: We prove induction step for the case D = D1 and D2. Similarly, it can be shown in case D = :D1. Assume that D is true in I, then also D1 and D2 are true. Since D1 and D2 are constructed in less steps then D by induction hypothesis we have that M; t j= pD1 and M; t j= pD2 . Hence, M; t j= pD.
For an extended DatalogMTL program , ground atom A and a time point t we define that j= A@t for the canonical model M of it holds M; t j= A Then, directly from Lemmas 1 and 2 we have the following theorem.
Theorem 1 (Encoding Theorem). Let be a program and r a message rule. Let the extended DatalogMTL that encodes as described above and let the grounded propositional mr be the head of DatalogMTL rule encoding r. Then: fires r iff
It is not hard to show the ideas of Theorem 5 in [
The second observation is that we can extend rewriting techniques developed for
Datalognr MTL in [
Let be an extended Datalognr MTL program, D a set of facts and A an grounded atom. As usual, ; D j= A@t for some time point t holds if for the canonical model M of [ D it holds M; t j= A. The decision problem success is the problem of checking whether ; D j= A@t. We refer to program (resp. data) complexity if all parameters are fixed except the program (resp. set of facts).
Lemma 3. Success problem for extended Datalognr MTL programs is PSPACE-complete in combined and program complexity and in AC0 in data complexity.
Proof (Proof Idea). Hardness follows from Theorem 5 in [
From Lemma 3 and Theorem 1 we have the following.
Theorem 2. The problem of checking whether a message rule is fired is PSPACEcomplete (it is complete already in size of rule signal expressions), and it is in AC0 in the size of signal data and ontological data. 6
In the Semantic Web community it is common to use rule-based ontological languages
such as SWRL [
Works in [
As discussed above, our work is strongly related to the work on well-studied Metric
Temporal Logic [
Another related direction is real-time processing of signal data streams. In this
direction, most of the work done so far mainly focused on querying RDF stream data. Many
different approaches such as C-SPARQL [
Acknowledgments This research is supported by the EPSRC projects MaSI3, DBOnto, ED3; and by the Free University of Bolzano projects QUEST, OBATS and ROBAST. 22. D. Anicic, P. Fodor, S. Rudolph, N. Stojanovic, EP-SPARQL: a unified language for event processing and stream reasoning, in: WWW, 2011, pp. 635–644. 23. H. Beck, M. Dao-Tran, T. Eiter, M. Fink, LARS: A logic-based framework for analyzing reasoning over streams, in: AAAI, 2015, pp. 1431–1438.