Information Technology Reference
In-Depth Information
5.1
Spawning Automata Construction
Given some
ϕ
∈
LTL
FO
, let us now examine how to build the corresponding SA,
A
ϕ
=
(
Σ,l,Q,Q
0
,δ
→
,δ
↓
,
F
) s.t.
L
(
A
ϕ
)=
L
(
ϕ
) holds. To this end, we set
Σ
=
{
(
A
,σ
)
|
σ
A
ϕ,v
to denote the spawning automaton
for
ϕ
in which free variables are mapped according to a finite set of valuations
v
.
2
To
define the set of states for an SA, we make use of a restricted subformula function,
sf
∈
(
A
)-Ev
}
.If
ϕ
is not a sentence, we write
|
∀
(
ϕ
), which is defined like a generic subformula function, except if
ϕ
is of the form
∀
x
:
p. ψ
,wehavesf
|
∀
(
ϕ
)=
{ϕ}
. This essentially means that an SA for a formula
ϕ
on the topmost level looks like the generalised Buchi automaton (GBA, cf. [3]) for
ϕ
,
where quantified subformulae have been interpreted as atomic propositions.
For example, if
ϕ
=
ψ
∧∀
x
:
p. ψ
,where
ψ
is a quantifier-free formula, then
A
ϕ
,
at the topmost level
n
, is like the GBA for the LTL formula
ψ
∧
a
,where
a
is an atomic
∀
x
:
p. ψ
separately in
proposition; or in other words,
A
ϕ
handles the subformula
terms of a subautomaton of level
n
1 (see also definition of
δ
↓
below).
Finally, we define the closure of
ϕ
wrt. sf
−
|
∀
(
ϕ
) as cl(
ϕ
)=
{¬
ψ
|
ψ
∈
sf
|
∀
(
ϕ
)
}∪
sf
|
∀
(
ϕ
), i.e., the smallest set containing sf
|
∀
(
ϕ
), which is closed under negation. The
set of states
of
A
ϕ
,
Q
, consists of all complete subsets of cl(
ϕ
);thatis,aset
q
⊆
cl(
ϕ
)
is complete iff
•
for any
ψ
∈
cl(
ϕ
) either
ψ
∈
q
or
¬
ψ
∈
q
, but not both; and
ψ
∈
ψ
∈
q
and
ψ
∈
•
for any
ψ
∧
cl(
ϕ
),wehavethat
ψ
∧
q
iff
ψ
∈
q
;and
for any
ψ
U
ψ
∈
cl(
ϕ
),wehavethatif
ψ
U
ψ
∈
q
then
ψ
∈
•
q
or
ψ
∈
q
,andif
ψ
U
ψ
∈
q
,then
ψ
∈
q
.
Let
q
∈
Q
and
A
=(
|
A
|
,I
).The
transition function
δ
→
(
q,
(
A
,σ
)) is defined iff
q
,wehave
t
I
p
I
and for all
q
,wehave
t
I
p
I
,
•
for all
p
(
t
)
∈
∈
¬
p
(
t
)
∈
∈
q
,wehave
t
I
r
I
and for all
q
,wehave
t
I
r
I
.
•
for all
r
(
t
)
∈
∈
¬
r
(
t
)
∈
∈
In which case, for any
q
∈
Q
,wehavethat
q
∈
δ
→
(
q,
(
A
,σ
)) iff
q
,and
•
for all
X
ψ
∈
cl(
ϕ
),wehave
X
ψ
∈
q
iff
ψ
∈
for all
ψ
U
ψ
∈
cl(
ϕ
),wehave
ψ
U
ψ
∈
q
iff
ψ
∈
q
and
ψ
U
ψ
∈
q
.
•
q
or
ψ
∈
This is similar to the well known syntax directed construction of GBAs (cf. [3]), except
that we also need to cater for quantified subformulae. For this purpose, an inductive
spawning function
is defined as follows. If
l>
0,then
δ
↓
(
q,
(
A
,σ
)) yields
⎛
⎛
⎝
(
p,
d
)
⎞
⎞
⎛
⎛
⎝
(
p,
d
)
⎞
⎞
⎝
⎠
⎠
∧
⎝
⎠
⎠
,
σ
A
ψ,v
σ
A
¬ψ,v
∀
x
:
p.ψ∈q
∈
¬∀
x
:
p.ψ∈q
∈
where
v
=
v
and
v
=
v
∪{
x
→
d
}
∪{
x
→
d
}
are sets of valuations, otherwise
δ
↓
(
q,
(
A
,σ
)) yields
. Moreover, we set
Q
0
=
{
q
∈
Q
|
ϕ
∈
q
}
,
F
=
{
F
ψ
U
ψ
|
2
Considering free variables, even though our runtime policies can only ever be sentences, is
necessary, because an SA for a policy
ϕ
is inductively defined in terms of SAs for its subfor-
mulae (i.e.,
A
ϕ
's subautomata), some of which may contain free variables.
