Information Technology Reference
In-Depth Information
must solve equations to determine the value of the variable that does not occur
in
ϕ
. Consider, e.g., the formula
q
(
x
)
y
.
Therule(
FLX
) may seem very restrictive. However, one can often rewrite a
formula of the form
p
(
t
1
,...,t
n
) with
p
∧
x
≈
y
·
∈
R
f
into an equivalent formula in
F
.
For instance,
p
(
x
+1
,x
) can be rewritten to
∃
y.p
(
y,x
)
∧
x
+1
≈
y
. Alternatively,
one can add additional rules that handle such cases directly.
We now show that
ϕ
's membership in
F
guarantees the finiteness of
ϕ
.
Lemma 5.
Let
(
¯
D
, τ
)
be a temporal database,
i
∈
N
atimepoint,
ϕ
aformula,
and
H
p
the set of effective indexes for
p
,foreach
p
∈
R
r
.If
ϕ
is a monitorable
(
¯
formula with respect to
(
H
p
)
p∈
R
r
,then
ϕ
D
,τ,i
)
is finite.
There are formulas like (
x
≈
y
)
S
p
(
x,y
) that describe finite relations but are
not in
. However, the policies considered in this paper all fall into the moni-
torable fragment. They follow the common pattern
F
∀
x, y.ϕ
(
x, y
)
∧
c
(
x, y
)
→
c
(
y
), where
c
and
c
represent restrictions, i.e., formulas of the form
r
(
t
)
ψ
(
y
)
∧
r
(
t
) with
r
and
¬
∈
R
r
. The formula to be monitored, i.e.,
ϕ
(
x, y
)
∧
c
(
x, y
)
∧
c
(
y
)) is in
,and
c,c
satisfy the conditions of the
¬
(
ψ
(
y
)
∧
F
if
ϕ
and
ψ
are in
F
(
RIG
)rules.
Finiteness can also be guaranteed by semantic notions like domain indepen-
dence or syntactic notions like range restriction, see, e.g., [1] and also [7, 12]
for a generalization of these notions to a temporal setting. If we restrict our-
selves to MFOTL without future operators, the range restricted fragment in [7]
is more general than the fragment
. This is because, in contrast to the rules
in Figure 2, range restrictions are not local conditions, that is, conditions that
only relate formulas with their direct subformulas. However, the evaluation pro-
cedures in [1,7,12] also work in a bottom-up recursive manner. So one still must
rewrite the formulas to evaluate them bottom-up. No rewriting is needed for
formulas in
F
F
. Furthermore, the fragment ensures that aggregation operators
are always applied to
finite
multi-sets. Thus, for any
ϕ
∈F
⊥∈
D
, the element
, provided that
p
D
i
⊆
D
ι
(
p
)
and
f
D
(
a
)
ϕ
∈
D
,for
never appears in a tuple of
every
p ∈
R
,
f ∈
F
,
i ∈
N
,and
a ∈ D
ι
(
f
)
,where
D
=
D
\{⊥}
.
3.2 Extended Relational Algebra Operators
Our monitoring algorithm is based on a translation of MFOTL
Ω
formulas in
F
to extended relational algebra expressions. The translation uses equalities,
which we present in Section 3.3, that extend the standard ones [1] expressing the
relationship between first-order logic (without function symbols) and relational
algebra to function symbols, temporal operators, and group-by operators. In this
section, we introduce the extended relational algebra operators.
We start by defining constraints. We assume a given infinite set of variables
Z
=
V
, ordered by their indices. A
constraint
is a formula
r
(
t
1
,...,t
n
) or its negation, where
r
is a rigid predicate symbol of arity
n
and the
t
i
s are constraint terms, i.e., terms with variables in
Z
. We assume that for each
domain element
d
{
z
1
,z
2
,...
}⊆
∈
D
, there is a corresponding constant, denoted also by
d
.Atu-
ple (
a
1
,...,a
k
) satisfies the constraint
r
(
t
1
,...,t
n
)iff
i
=1
fv
(
t
i
)
⊆{
z
1
,...,z
k
}
