Information Technology Reference
In-Depth Information
,I
1
)
...
is a (possibly infinite) sequence of first-order structures and
w
=
w
0
w
1
...
acor-
responding trace. We demand that for all
A
,w
),where
A
|
A
0
|
,I
0
)(
|
A
1
|
A
first-order temporal structure
is a tuple (
=(
A
i
and
A
i
+1
from
A
, it is the case that
|
A
i
|
=
|
A
i
+1
|
for all
f
∈
F
,
f
I
i
+1
=
f
I
i
,andforall
τ
∈
S
,
τ
I
i
=
τ
I
i
+1
.Forany
two structures,
A
and
A
, which satisfy these conditions, we write
A
∼
A
. Moreover
given some
A
and
A
,ifforall
A
i
from
A
,wehavethat
A
i
∼
A
, we also write
A
∼
A
.
Finally, the interpretation of an
U
-operator
p
with arity
τ
1
×
...
×
τ
m
is then defined
wrt. a position
i
in
w
as
p
I
i
=
. Essentially this means that, unlike
function symbols,
U
-and
I
-operators don't have to be rigid.
Note also that from this point forward, we consider only the case where the policy to
be monitored is given as a closed formula, i.e., a sentence. This is closely related to our
means of quantification: a quantifier in LTL
FO
is restricted to those elements that appear
in the trace, and not arbitrary elements from a (possibly infinite) domain. While certain
policies cannot be expressed with this restriction (e.g., “for all phone numbers
x
that
are not in the contact list,
r
(
x
) is true”), this restriction bears the advantage that, when
examining a given trace, functions and relations are only ever evaluated over known
objects. The advantages of this type of quantification in monitoring first-order languages
have also been pointed out in [16,5]. In other words, had we allowed free variables, a
monitor might end up having to “try out” all the different domain elements in order to
evaluate such policies, which runs counter to our design rationale of quantification.
In what follows, let us fix a particular
Γ
. The semantics of LTL
FO
can now be defined
wrt. a quadruple (
{
d
|
(
p,
d
)
∈
w
i
}
∈
N
0
,and
v
is an (initially empty) set
of valuations assigning domain values to variables:
A
,w,v,i
) as follows, where
i
=
p
(
t
1
,...,t
n
) iff (
t
I
1
,...,t
I
n
)
p
I
i
,
(
A
,w,v,i
)
|
∈
r
I
i
,
(
A
,w,v,i
)
|
=
¬ϕ
iff (
A
,w,v,i
)
|
=
ϕ
is not true
,
=
r
(
t
1
,...,t
n
) iff (
t
I
1
,...,t
I
n
)
(
A
,w,v,i
)
|
∈
(
A
,w,v,i
)
|
=
ϕ
∧
ψ
iff (
A
,w,v,i
)
|
=
ϕ
and (
A
,w,v,i
)
|
=
ψ,
(
A
,w,v,i
)
|
=
X
ϕ
iff
|
w
|
>i
and (
A
,w,v,i
+1)
|
=
ϕ,
(
A
,w,v,i
)
|
=
ϕ
U
ψ
iff for some
k
≥
i,
(
A
,w,v,k
)
|
=
ψ,
and (
A
,w,v,j
)
|
=
ϕ
for all
i
≤
j<k,
(
A
,w,v,i
)
|
=
∀
(
x
1
,...,x
n
):
p. ϕ
iff for all (
p,d
1
,...,d
n
)
∈
w
i
,
(
A
,w,v
∪{
x
1
→
d
1
,...,x
n
→
d
n
}
,i
)
|
=
ϕ,
where terms are evaluated inductively and
x
I
treated as
v
(
x
).If(
A
,w,v,
0)
|
=
ϕ
,we
write (
=
ϕ
.
Later we will also make use of the (possibly infinite) set of all events wrt.
A
,w,v
)
|
=
ϕ
,andif
v
is irrelevant or clear from the context, (
A
,w
)
|
A
,given
)-Ev =
p∈
U
{
as (
A
(
p,
d
)
|
d
∈
D
p
}
, and take the liberty to omit the trailing (
A
)
whenever a particular
is either irrelevant or clear from the context. We can then de-
scribe the
generated language
of
ϕ
,
A
L
(
ϕ
) (or simply the language of
ϕ
, i.e., the set of
2
Ev
and (
all logical models of
ϕ
) compactly as
,
although, as before, we shall only ever concern ourselves with either infinite- or finite-
trace languages, but not mixed ones. Finally, we will use common syntactic “sugar”,
including
L
(
ϕ
)=
{
(
A
,w
)
|
w
i
∈
A
,w
)
|
=
ϕ
}
∃
(
x
1
,...,x
n
):
p. ϕ
=
¬
(
∀
(
x
1
,...,x
n
):
p.
¬
ϕ
),etc.
