Information Technology Reference
In-Depth Information
(
¯
As
ψ
and
D
,τ,i
)
are the policy violations at
time point
i
. Note that we drop the outermost quantifier as we are interested
not only in whether the policy is violated. An instantiation of the free variables
x
that satisfies
ψ
provides additional information about the violations.
¬
ϕ
are equivalent, the tuples in
ψ
3.1 Monitorable Fragment
Not all formulas are effectively monitorable. Consider, for example, the policy
∀
q
(
x,y
)thatweusefor
monitoring. There are infinitely many violations for time points
i
with
p
D
i
x.
∀
y.p
(
x
)
→
q
(
x,y
) with the formula
ψ
=
p
(
x
)
∧¬
∅
=
,
(
¯
namely, any tuple (
a,b
)
D
,τ,i
)
is infinite and its elements cannot be enumerated in finite time. We define a
fragment of MFOTL
Ω
that guarantees finiteness. Furthermore, the set of viola-
tions at each time point can be effectively computed bottom-up over the formula
structure. In the following, we treat the Boolean connective
∈
D
2
\
q
D
i
with
a
∈
p
D
i
.Insuchacase,
ψ
∧
as a primitive.
Definition 4.
The set
of
monitorable formulas
with respect to
(
H
p
)
p∈
R
r
is
defined by the rules given in Figure 2, where
H
p
⊆{
F
1
,...,ι
(
p
)
}
,foreach
p
∈
R
r
.
Let
be a label of a rule from Figure 2. We say that a formula
ϕ
∈F
is of
kind
if there is a derivation tree for
ϕ
having as root a rule labeled by
.
Before describing some of the rules, we first explain the meaning of the set
H
p
,
for
p
R
r
with arity
k
.Theset
H
p
contains the indexes
j
for which we can
determine the values of the variable
x
j
that satisfy
p
(
x
1
,...,x
k
), given that
the values of the variables
x
i
with
i
∈
=
j
are fixed. Formally, given a temporal
database (
¯
, τ
) and a rigid predicate symbol
p
of arity
k>
0, we say that
an index
j
,with1
D
k−
1
,theset
≤
j
≤
k
,is
effective
for
p
if for any
a
∈
D
p
D
}
{
d
∈
D
|
(
a
1
,...,a
j−
1
,d,a
j
,...,a
k−
1
)
∈
is finite. For instance, for the rigid
predicate
≈
, the set of effective indexes is
H
≈
=
{
1
,
2
}
. Similarly, for the rigid
predicate
.
We describe the intuition behind the first four rules in Figure 2. The meaning
of the other rules should then be obvious. The first rule (
FLX
) requires that in
an atomic formula
p
(
t
) with
p
≺
N
, defined as
a
≺
N
b
iff
a,b
∈
N
and
a<b
,wehave
H
≺
N
:=
{
1
}
R
f
,theterms
t
i
are pairwise distinct variables.
This formula is monitorable since we assume that
p
's interpretation is always a
finite relation. For the rules (
RIG
∧
)and(
RIG
∧¬
), consider formulas of the form
ϕ
∈
R
r
and
ι
(
p
)
p
(
t
)and
ϕ
p
(
t
) with
p
fv
(
ϕ
). In both cases,
the second conjunct restricts on the tuples satisfying
ϕ
. A simple example is
the formula
p
(
x,y
)
∧
∧¬
∈
i
=1
fv
(
t
i
)
⊆
y
.If
ϕ
is monitorable, such a formula is also
monitorable as its evaluation can be performed by filtering out the tuples in
∧
x
+1
≈
ϕ
that do not satisfy the second conjunct. The rule (
RIG
∧
) treats the case where
one of the terms
t
i
is a variable that does not appear in
ϕ
. We require here that
the index
j
is effective, so that the values of this variable are determined by the
values of the other variables, which themselves are given by the tuples in
ϕ
.
An example is the formula
p
(
x,y
)
x
+
y
. The required conditions on
t
j
are necessary. If
j
is not effective, then we cannot guarantee finiteness. Consider,
e.g., the formula
q
(
x
)
∧
z
≈
∧
x
≈
y
.If
t
j
is neither a variable nor a constant, then we
