Information Technology Reference
In-Depth Information
Definition 2 (Push-down Moore Machine).
A (deterministic)
push-down
Moore machine
is a tuple
=(
Q,Σ,Γ,δ,q
0
,Λ,λ
)
where
-
Q
is a finite set of
states
and
q
0
∈
M
Q
the
initial state
,
-
Σ
,
Γ
,
Λ
are the finite
input-
,
stack-
and
output alphabets
, respectively, and
Γ
#
:=
Γ
∪
#
the stack alphabet enriched by a new
bottom symbol #
∈
Γ
,
Γ
≤
2
#
-
δ
:
Q
×
Γ
#
×
Σ
→
Q
×
the deterministic
transition function
and
-
λ
:
Q
→
Λ
the
output function
.
(
Γ
∗
{
) comprising the current
control state and a stack assignment ending with #. The
run
of
A
configuration
of
M
is a tuple (
q,s
)
∈
Q
×
#
}
M
on a word
w
=
Σ
∗
is the sequence of configurations
c
0
c
1
...c
n
+1
s.t.
c
0
=(
q
0
,
#) and
a
1
...a
n
∈
Γ
,
c
i
=(
q,γs
)and
δ
(
q,γ,a
i
+1
)=(
q
,γ
γ
)wehave
c
i
+1
=(
q
,γ
γ
s
).
The
output
of
for
γ
∈
M
on
w
is
M
(
w
):=
λ
(
q
last
)where(
q
last
,s
last
)=
c
n
+1
.
TheMooreMachinefor
M
3
.
In the fashion of [10] we construct
F
P
and
also
F
¬P
accepting all non-bad prefixes for the complement of
P
and combine
them to a Moore machine. We know that if some
w
Σ
∗
is rejected by
∈
F
P
,then
M
3
(
P
)(
w
)=
⊥
and consequently if
w
is rejected by
F
¬P
then
M
3
(
P
)(
w
)=
.
These cases exclude each other and if both accept then
M
3
(
P
)(
w
)=?.
Note, while it is always possible to complement an
ω
-Vpa for some property
P
and construct
F
¬P
from it, it might be preferable to negate the property earlier.
In particular, when using a logic that allows direct negation, it is advised to
negate before constructing an automaton. Recall, we can assume
F
¬P
determinized. We combine both and obtain a deterministic visibly push-down
Moore machine
F
P
and
M
⊥
, that outputs
for every good,
for every bad and ? for
every inconclusive prefix for
P
.
For
F
P
=(
Q
P
,Σ,Γ
P
,δ
P
,I
P
,F
P
)and
F
¬P
=(
Q
¬P
,Σ,Γ
¬P
,δ
¬P
,I
¬P
,F
¬P
)
we let
M
=(
Q
P
×Q
¬P
,Σ,Γ
P
×Γ
¬P
,δ,I
P
×I
¬P
,
B
3
,λ
)
with
δ
((
q
1
,q
2
)
,
(
γ
1
,γ
2
)
,a
):=((
q
1
,q
2
)
,
(
γ
1
,γ
2
)(
γ
1
,γ
2
))
where (
q
1
,γ
1
γ
1
)=
δ
ϕ
(
q
1
,γ
1
,a
)and(
q
2
,γ
2
γ
2
)=
δ
¬ϕ
(
q
2
,γ
2
,a
).
The output of
M
is defined as
⎧
⎨
if
q
2
∈
F
¬ϕ
λ
(
q
1
,q
2
)=
⊥
F
ϕ
? rwi
.
if
q
1
∈
⎩
Note, that
λ
is well defined since
P
and
¬
P
exclude each other.
Theorem 3.
Given an
ω
-
Vpa
P
, we can construct a deterministic push-down
Moore Machine
M
implementing the three-valued monitoring function for
L
(
P
)
,
i.e. for all
w
∈
Σ
∗
,
M
(
w
)=
M
3
(
L
(
P
))(
w
)
.
Corollary 2.
Given a CaRet formula
ϕ
,wecanconstructin3-
ExpTime
a
push-down Moore machine
M
implementing the three-valued semantics function
for
ϕ
.