Information Technology Reference
In-Depth Information
Kind
(
GEN
ω
)
.
Let [
ω
t
z
.ψ
](
y
;
g
)beaformulaofkind(
GEN
ω
). It holds that
,τ,i
)
=
ω
θ
(
t
)
,τ,i
)
,
(
¯
(
¯
[
ω
t
z
.ψ
](
y
;
g
)
D
D
ψ
where
fv
(
ψ
)=(
y
1
,...,y
n
), for some
n
≥
0,
G
=
{
i
|
y
i
∈
g
}
,and
θ
:
fv
(
ψ
)
→
fv
(
ψ
). For
{
z
1
,...,z
n
}
is given by
θ
(
x
)=
z
j
with
j
being the index of
x
in
instance, for [
SUM
x
+
y
x,y.p
(
x,y,z
)](
s
;
z
), we have
G
=
{
3
}
and
θ
(
t
)=
z
1
+
z
2
.
Other kinds.
The case for (
RIG
∧¬
) is similar to the one for (
RIG
∧
). The cases for
(
GEN
∧
), (
GEN
∧¬
), and (
GEN
¬
S
) are similar to the one for (
GEN
S
). The cases for
(
GEN
∧¬
)and(
GEN
¬
S
) use the antijoin instead of the join. The cases for (
GEN
∨
),
(
GEN
∃
), (
GEN
) are obvious. Additional details are in the appendix of the full
version of the paper available at the authors' web pages.
3.4 Algorithmic Realization
Our monitoring algorithm for MFOTL
Ω
is inspired by those in [7,8,11]. We only
sketch it here. Further details are given in the appendix.
For a formula
ψ
∈F
, the algorithm iteratively processes the temporal
database (
¯
D
, τ
). At each time point
i
, it calls the procedure
eval
to com-
(
¯
,τ,i
)
. The input of
eval
at time point
i
is the formula
ψ
, the time point
i
with its timestamp
τ
i
, and the interpretations of the flexible predicate symbols,
i.e.,
r
D
i
,foreach
r
D
pute
ψ
R
f
.Notethat
¯
's domain and the interpretations of the
rigid predicate symbols and the function symbols, including the constants, do
not change over time. We assume that they are fixed in advance.
The computation of
∈
D
(
¯
D
,τ,i
)
is by recursion over
ψ
's formula structure and
is based on the equalities in Section 3.3. Note that extended relational algebra
operators have standard, ecient implementations [17], which can be used to
evaluate the expressions on the right-hand side of the equalities from Section 3.3.
To accelerate the computation of
ψ
(
¯
D
,τ,i
)
, the monitoring algorithm main-
tains state for each temporal subformula, storing previously computed interme-
diate results. The monitor's state is initialized by the procedure
init
and updated
in each iteration by the procedure
eval
. For subformulas of the form
ψ
I
ψ
,we
store at time point
i>
0, the tuples that satisfy
ψ
at time-point
i
−
1, i.e.,
(
¯
D
,τ,i−
1)
. For formulas of the form
ψ
1
S
[
a,b
)
ψ
2
, we store at time
point
i
, the list of relations
ψ
the relation
D
,τ,j
)
s,C
j<k≤i
D
,τ,k
)
with
j
(
¯
(
¯
ψ
2
ψ
1
≤
i
such that
τ
i
−
τ
j
<b
,where
s
and
C
are defined as in Section 3.3. By storing
these relations, the subformulas
ψ
,
ψ
1
,and
ψ
2
need not be evaluated again
at time points
j<i
during the evaluation of
ψ
at time point
i
. Further opti-
mizations are possible. For instance, one can store and reuse some of the inter-
mediate relations used for computing the relation
ψ
1
S
[
a,b
)
ψ
2
(
¯
D
,τ,i
)
from the
relations stored in the previously mentioned list. Also, when
a
=0and
b
=
∞
,
it is sucient to store the resulting relation from the previous time point, as
∪
,τ,i
)
.
(
¯
(
¯
(
¯
(
¯
D
,τ,i
)
=
D
,τ,i
)
D
,τ,i
−
1)
D
ψ
1
S
ψ
2
ψ
2
ψ
1
S
ψ
2
ψ
1
Theorem 6.
Let
(
¯
D
, τ
)
be a temporal database,
i
∈
N
,and
ψ
∈F
. The proce-
(
¯
D
,τ,i
)
, whenever
init
(
ψ
)
,
eval
(
ψ
,0,
dure
eval
(
ψ
,
i
,
τ
i
,
Γ
i
)
returns the relation
ψ
