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 ϕ .
 
Search WWH ::




Custom Search