Information Technology Reference
In-Depth Information
at least one word in a configuration (
q,w
#) iff
w
∈
Γ
∗
accepted by
A
when
starting in the state
q
Q
.
We construct a Vpa
F
∈
=(
Q,Σ,Γ
×
S
Q
,δ
F
,Q
0
,F
F
)thatbehaveslike
P
but
simultaneously simulates
A
. The initial configuration of
F
represents the initial
configurations of
P
and
A
. Reading inputs form
Σ
,
F
simulates the behavior of
P
and when
P
pushes a symbol
γ
onto the stack,
F
additionally simulates
A
reading
γ
and stores the new configuration of
A
on the stack. When
P
removes
the top-most symbol
γ
from the stack,
F
also removes the top-most symbol
including the current configuration of
A
and thereby restoring the configuration
of
A
before having read
γ
.
A configuration of
A
is a state
s
∈
S
∪
Q
for each initial state
q
∈
Q
, meaning
if
started in
q
it would currently be in state
s
. A configuration is therefore a
mapping from
Q
to
S
A
Q
.Let
δ
A
:
S
Q
S
Q
be the transition function of
∪
×
Γ
→
δ
A
(
f
(
q
)
,γ
). That is
δ
A
applies
a
γ
transition “state-wise” to
f
. Following this idea, we define the transition
function of
S
Q
s.t.
δ
A
(
f,γ
):
q
A
lifted to mappings
f
∈
→
as follows. Note,
ω
-Vpa can, in general, not be determinized and
thus we construct a non-deterministic automaton
F
F
. However since
F
is a Vpa,
it can be determinized afterwards [13].
(
q
,
(
γ,f
))
(
q
,γ
)
∈
δ
F
(
q,
(
γ,f
)
,a
)
⇔
∈
δ
P
(
q,γ,a
)
(for
a
∈
Σ
int
)
(
q
,
#
F
)
(
q
,
#
P
)
∈
δ
F
(
q,
#
F
,a
)
⇔
∈
δ
P
(
q,
#
P
,a
)
(for
a
∈
Σ
r
)
for
a
∈
Σ
r
(
q
,
)
(
q
,
)
∈
δ
F
(
q,
(
γ,f
)
,a
)
⇔
∈
δ
P
(
q,γ,a
)
and
γ
=#
P
(
q
,γ
γ
)
δ
P
(
q,γ,a
)
and
f
=
δ
A
(
f,γ
)
∈
(
q
,
(
γ
,f
)(
γ,f
))
∈
δ
F
(
q,
(
γ,f
)
,a
)
⇔
(for
a
∈
Σ
c
)
, respectively.
To correctly treat the empty stack, we interpret the bottom symbol #
F
of
Here, #
F
and #
P
denote the bottom stack symbols of
F
and
P
F
as (#
P
,
id
) since for each state
q
of
P
,
A
is initially in the corresponding initial
state, which is
q
itself.
In every state
q
∈
Q
,
P
is in a non-empty configuration, iff the multi-
automaton
A
accepts the current stack for
q
. The current configuration
f
of
A
is stored in the top-most stack symbol of
F
.So,when
f
(
q
) is an accepting
state of
A
and the current control state is
q
,
P
had a non-empty configuration
and we hence let
F
A
.
This condition can be realized technically by storing the top-most stack symbol
in the finite control and define the set of accepting states of
F
accept exactly in the configurations (
q,
(
γ,f
)
s
) s.t.
f
(
q
)
∈
F
accordingly.
From that construction we conclude that
F
accepts exactly the non-bad pre-
fixes for the language accepted by
.
Theorem 2.
For all
w ∈ Σ
∗
,
w ∈L
(
F
)
if and only if
M
3
(
L
(
P
))(
w
)
=
⊥.
P
4.2 Anticipatory Monitors for Visibly Context-Free Properties
Using the construction above we can now construct a Moore machine that com-
putes the three-valued monitoring semantics
M
3
(
P
) for any visibly context-free
Σ
ω
, assuming that
P
is presented as
ω
-Vpa.
property
P
⊆
