Information Technology Reference
In-Depth Information
Example 1.
For brevity, cf. [6] for some LTL
FO
example policies formalised in LTL
FO
.
However, to give at least an intuition, let's pick up the idea of monitoring Android
“Apps” again, and specify that “Apps” must not send SMS messages to numbers not
in a user's contact database. Assuming there exists an
U
-operator
sms
, which is true
/ appears in the trace, whenever an “App” sends an SMS message to phone number
x
,
we could formalise said policy in terms of
G
x
:
sms. contact
(
x
). Note how in this
formula the meaning of
x
is given implicitly by the arity of
sms
and must match the
definition of
contact
in each world. Also note how
sms
is interpreted indirectly via
its occurrence in the trace, whereas
contact
never appears in the trace, even if true.
contact
can be thought of as interpreted via a program that queries a user's contact
database, whose contents may change over time.
∀
4
Complexity of Monitoring in the First-Order Case
LTL
FO
as defined above is undecidable as can be shown by way of the following lemma.
It basically helps us reduce finite satisfiability of standard first-order logic to LTL
FO
.
Lemma 1.
Let
ϕ
be a sentence in first-order logic, then we can construct a correspond-
ing
ψ
∈
LTL
FO
s.t.
ϕ
has a finite model iff
ψ
is satisfiable.
Theorem 2.
LTL
FO
is undecidable.
Proof (Sketch).
Follows from Lemma 1 and Trakhtenbrot's Theorem (cf. [20,
§
9]).
Let's now define what is meant by Kripke structures in our new setting. They either
give rise to infinite-trace languages (i.e., have a left-total transition relation), or repre-
sent finite traces (i.e, are essentially linear structures). For brevity, we shall restrict to the
definition of the former. Note that we will also skip detailed redefinitions of the decision
problems discussed in
§
2, since the concepts transfer in a straightforward manner.
Definition 6.
Given some
A
,a
(
A
)-Kripke structure
, or just first-order Kripke structure,
K
=(
S,s
0
,λ,
→
)
,where
S
is a finite set of states,
s
0
∈
S
is a state-transition system
−→
A
×
Ev
,where
A
{
A
|
A
∼
A
}
a distinguished initial state,
λ
:
S
=
, a labelling
function, and
→⊆
S
×
S
a (left-total) transition relation.
Definition 7.
Fo r a
(
A
)
-Kripke structure
K
with states
s
0
,...,s
n
,the
generated lan-
guage
is given as
L
(
K
)=
{
(
A
,w
)
|
(
A
0
,w
0
)=
λ
(
s
0
)
and for all
i
∈
N
there exist
some
j,k
∈
[0
,n
]
s.t.
(
A
i
,w
i
)=
λ
(
s
j
)
,
(
A
i−
1
,w
i−
1
)=
λ
(
s
k
)
and
(
s
k
,s
j
)
∈→}
.
The inputs to the LTL
FO
word problem are therefore an LTL
FO
formula and a linear
first-order Kripke structure, representing a finite input trace. Unlike in standard LTL,
Theorem 3.
The word problem for
LTL
FO
is PSpace-complete.
The inputs to the LTL
FO
model checking problem, in turn, are a left-total first-order
Kripke structure, which gives rise to an infinite-trace language, and an LTL
FO
formula.
