Information Technology Reference
In-Depth Information
the formulae are kept in e.g. disjunctive normal form). This is no longer the
case for the abstract operators as during evaluation an unbounded number of
inequivalent formulae may occur. This is expected, as the formula describes a
pushdown-language and encodes a stack. In the following, we will use pushdown
machines to handle the stack explicitly. This simplifies implementation as well
as theoretical discussion.
The outline for the rest of this section isasfollows.Weintroducenon-deter-
ministic push-down Mealy machines (Pmm) and show how they can be deter-
minized. Next, based on the FCaRet
4
semantics defined above, we give a pro-
cedure to construct a Pmm from a CaRet
+
formula, that reads symbols and
outputs the FCaRet
4
semantics of the word read so far.
Mealy Machines.
A non-deterministic Mealy machine can, in general reach mul-
tiple configurations at a time. Each such current configuration yields an output.
To consistently define the overall output of the automaton, we need to be able
to summarize the single outputs in each step. The existential character of a
non-deterministic model is lifted to a supremum (join) operation on all possible
outputs in each step. A configuration may have multiple successors, which have
no order. We therefore need commutativity, associativity and idem-potency of
the join operation on the outputs, that is, we require the output domain to be
a semi-lattice.
Definition 1 (Push-down Mealy Machine).
A (non-deterministic)
push-
down Mealy machine
(
Pmm
)isatuple
M
=(
Q,Σ,Γ,δ,Q
0
,
L
)
where
-
Σ,Γ
are the finite
input
and
stack alphabet
, respectively, and
Γ
#
:=
Γ
∪{
#
}
the stack alphabet enriched by a new bottom symbol
#
∈
Γ
,
-
L
is the
output alphabet
with
(
L
,
)
forming a semi-lattice,
-
Q
is a finite set of control
states
,
-
Q
0
⊆
Q
is the set of
initial states
and
2
Q×Γ
≤
#
×
L
is the non-deterministic, labeled
transition
-
δ
:
Q
×
Γ
#
×
Σ
→
function
.
(
Γ
∗
{
A
configuration
of
) comprising the cur-
rent control state and a stack assignment ending with #. The
run
of
M
is a tuple (
q,s
)
∈
Q
×
#
}
M
on
a non-empty input word
w
=
w
0
w
1
...w
n
∈
Σ
+
is the alternating sequence
1
−→
C
1
...
n
(
Γ
∗
{
C
0
−→
C
n
of sets of configurations
C
i
⊆
Q
×
#
}
) and output
symbols
i
∈
L
s.t.
-
C
0
=
Q
0
×{
#
}
,
-
L
i
+1
⊆
L
and
C
i
+1
are the smallest sets such that, for
γ
∈
Γ
,(
q,γs
)
∈
C
i
and (
q
,γ
γ
,
)
δ
(
q,γ,a
i
+1
) implies (
q
,γ
γ
s
)
∈
∈
C
i
+1
and
∈
L
i
+1
,and
-
i
=
L
i
+1
.
The
output
of
M
on
w
is
M
(
w
):=
n
.
M
is called a
visibly
Pmm
(Vpmm), if it satisfies the corresponding con-
straints defined above for Vpa.
