Information Technology Reference
In-Depth Information
p ∈
R
f
x
1
,...,x
ι
(
p
)
∈
V are pairwise distinct
p
(
x
1
,...,x
ι
(
p
)
)
∈F
FLX
ϕ ∈F p ∈
R
r
ι
(
p
)
ϕ ∈F p ∈
R
r
ι
(
p
)
i
=1
fv
(
t
i
)
⊆ fv
(
ϕ
)
ϕ ∧ p
(
t
1
,...,t
ι
(
p
)
)
∈F
i
=1
fv
(
t
i
)
⊆ fv
(
ϕ
)
ϕ ∧¬p
(
t
1
,...,t
ι
(
p
)
)
∈F
RIG
∧
RIG
∧¬
ϕ ∈F p ∈
R
r
ι
(
p
)
i
=1
,i
=
j
fv
(
t
i
)
⊆ fv
(
ϕ
)
t
j
∈
V
j ∈ H
p
RIG
∧
ϕ ∧ p
(
t
1
,...,t
ι
(
p
)
)
∈F
ϕ, ψ ∈F
ϕ ∧ ψ ∈F
ϕ, ψ ∈F fv
(
ψ
)
⊆ fv
(
ϕ
)
ϕ ∧¬ψ ∈F
ϕ, ψ ∈F fv
(
ψ
)=
fv
(
ϕ
)
ϕ ∨ ψ ∈F
GEN
∧
GEN
∧¬
GEN
∨
ϕ ∈F
∃x. ϕ ∈F
ϕ ∈F
I
ϕ ∈F
ϕ ∈F
[
ω
t
z.ϕ
](
y
;
g
)
∈F
GEN
∃
GEN
GEN
ω
ϕ, ψ ∈F fv
(
ϕ
)
⊆ fv
(
ψ
)
ϕ
S
I
ψ ∈F
ϕ, ψ ∈F fv
(
ϕ
)
⊆ fv
(
ψ
)
¬ϕ
S
I
ψ ∈F
GEN
S
GEN
¬
S
Fig. 2.
The derivation rules defining the fragment
F
of monitorable formulas
information obtained from a predicate symbol
tpts
that is interpreted as
tpts
D
i
=
{
(
i,τ
i
)
}
,for
i
∈
N
.
The multiplicity issue illustrated by Example 3 also appears in databases. SQL is
basedonamulti-setsemanticsandoneusesthe
DISTINCT
keyword to switch to
a set-based semantics. However, it is problematic to define a multi-set semantics
for first-order logic, i.e., one that attaches a multiplicity to a tuple
d
∈
D
|fv
(
ϕ
)
|
for how often it satisfies the formula
ϕ
instead of a Boolean value. For instance,
there are several ways to define a multi-set semantics for disjunction: the multi-
plicity of
d
for
ψ
ψ
can be either the maximum or the sum of the multiplicities
of
d
for
ψ
and
ψ
. Depending on the choice, standard logical laws become invalid,
namely, distributivity of existential quantification or conjunction over disjunc-
tion. Defining a multi-set semantics for negation is even more problematic.
∨
3 Monitoring Algorithm
We assume that policies are of the form
x.ϕ
,where
ϕ
is an MFOTL
Ω
formula
and
x
is the sequence of free variables of
ϕ
. The policy requires that
∀
∀
x.ϕ
holds
at every time point in temporal structure (
¯
D
, τ
). In the following, we assume
that (
¯
D
, τ
)isa
temporal database
, i.e., (1) the domain
D
is countably infinite,
(2) the relation
p
D
i
is finite, for each
p
,(3)
p
D
is a recursive
∈
R
f
and
i
∈
N
R
r
,and(4)
f
D
is computable, for each
f
relation, for each
p
F
. We also
assume that the aggregation operators in
Ω
are computable functions on finite
multi-sets.
The inputs of our monitoring algorithm are a formula
ψ
, which is logically
equivalent to
∈
∈
ϕ
, and a temporal database (
¯
, τ
), which is processed iteratively.
The algorithm outputs, again iteratively, the relation
¬
D
(
¯
D
,τ,i
)
,foreach
i
ψ
≥
0.
