Hardware Reference
In-Depth Information
the partitioned representation of the product automaton, is simply the union of the
two partitions, i.e.,
fT
j
T
F
.i;
v
;cs
F
;ns
j
T
F
/; T
j
T
S
.i; cs
S
;ns
j
T
S
/g:
The fact that some variables, for example,
u
and
o
, are missing, means that the
relations are independent of these variables.
7.2.1.4
Hiding Variables
Hiding variables
i
and
o
in the automaton representing the product of
F
and
S
is
an operation which changes the support automaton. In the monolithic form, it is
performed by existentially quantifying the variables, not in the support, from the
transition-output relation
TO
of the product automaton:
TO
0
.
v
;
u
;cs;ns/ D9
i;o
ŒTO.i;
v
;
u
;o;cs;ns/:
This operation usually leads to a non-deterministic automaton, even if the original
automaton is deterministic. Hiding variables cannot be performed on the partitioned
representation because the operations of existential quantification and product do
not commute. For example, it is not possible to quantify the input variables
i
from
the transition relation by quantifying them independently from each partition:
9
i
T.i;cs;ns/ D9
i
˘
j
Œns
j
T
j
.i; cs/ ¤ ˘
j
9
i
Œns
j
T
j
.i; cs/:
Thus hiding cannot be done by acting on the partitions independently. However,
a key observation is that the hiding operation can be built into the next step,
the determinization procedure, in such a way that there is no need to derive the
monolithic transition relation and then apply hiding to it.
7.2.1.5
Determinization (Subset Construction)
Determinization is performed by enumerating explicitly the subsets of states of
a non-deterministic automaton, which are reachable from the initial subset state
(which contains only the initial state). The basic step is the computation of the subset
of states, reachable under various assignments of
.
u
;
v
/
from a given subset of states,
.cs/
. Denote by
P
.
u
;
v
;ns/
the sets of states (the subset states) reachable from
.cs/
under various combinations of
.
u
;
v
/
. Using the monolithic representation,
with variable
i
hidden, the computation would be:
P
.
u
;
v
;ns/ D9
i;cs
ŒU.i;
v
;cs;
u
/:T .i;
v
; cs; ns/:.cs/:
Search WWH ::
Custom Search