Information Technology Reference
In-Depth Information
Fig. 1.
Spawning on
{
login
(1
,
2
.
3
.
4
.
1)
,login
(2
,
2
.
3
.
4
.
2)
,send
(3
,
2
.
3
.
4
.
3)
,send
(1
,
2
.
3
.
4
.
1)
}
ψ
U
ψ
∈
ψ
∈
(
ψ
U
ψ
)
cl(
ϕ
)
}
with
F
ψ
U
ψ
=
{
q
∈
Q
|
q
∨¬
∈
q
}
,and
l
=depth(
ϕ
),
where depth(
ϕ
) is called the
quantifier depth
of
ϕ
.Forsome
ϕ
LTL
FO
, depth(
ϕ
)=
0 iff
ϕ
is a quantifier free formula. The remaining cases are inductively defined as
follows: depth(
∈
∀
x
:
p. ψ
) = 1+depth(
ψ
), depth(
ψ
∧
ψ
) = depth(
ψ
U
ψ
)=
max(depth(
ψ
)
,
depth(
ψ
)) and depth(
¬
ϕ
) = depth(
X
ϕ
) = depth(
ϕ
).
Lemma 3.
Let
ϕ
∈
LTL
FO
(not necessarily a sentence) and
v
be a valuation. For each
accepting run
ρ
in
A
ϕ,v
over input
(
A
,w
)
,
ψ
∈
cl(
ϕ
)
, and
i
≥
0
, we have that
ψ
∈
ρ
(
i
)
iff
(
A
,w,v,i
)
|
=
ψ
.
Theorem 6.
The constructed SA is correct in the sense that for any sentence
ϕ
∈
L
A
ϕ
)=
L
(
ϕ
)
.
LTL
FO
, we have that
(
Example 2.
Consider the graphical representation of an SA for
ϕ
=
G
(
∀
(
u,ip
):
eq
(
ip,ip
))
U
logout
(
u,ip
))) in Fig. 1. In a
nutshell,
ϕ
states that once user
u
has logged in to the system from IP-address
ip
,she
must not send anything from an IP-address other than
ip
until logged out. While
ϕ
is
not meant to represent a realistic security policy as is, it does help highlight the features
of an SA: We first note that level
l
of
(
u
,ip
):
send. eq
(
u,u
)
login.
((
∀
⇒
A
ϕ
is given by depth(
ϕ
)=2.As
ϕ
is of the form
G
A
ϕ
's individual state space is de facto that of an ordinary GBA
for an LTL formula of the form
G
p
. Let's now assume that
σ
=
∀
(
u,ip
):
login. ψ
,
{
login
(1
,
2
.
3
.
4
.
1)
,
login
(2
,
2
.
3
.
4
.
2)
,send
(3
,
2
.
3
.
4
.
3)
,send
(1
,
2
.
3
.
4
.
1)
A
ϕ
to
process. Due to
ϕ
's outmost quantifier, the two
login
-actions will lead to the spawning
of a conjunction of two subautomata of respective levels
l
}
is an event, which we want
1 (downward dotted lines).
The individual state space of these subautomata is de facto that of an ordinary GBA for
an LTL formula of the form
a
U
b
as one can see in Fig. 1, level 1. These SAs also keep
−
