Hardware Reference
In-Depth Information
2. The next state relation
0
of F
0
is given by
0
D
[f
.
v
;s;.s;1//
j
v
2
V; s
2
S
g
[f
.
v
;.s;j/;.s;j
C
1//
j
v
2
V; s
2
S; 1
j<l
g
[f
.x;.s;j/;s
0
/
j
.x;s;s
0
/
2
; 1
j
l
g
:
3. r
0
D
r and Q
0
D
Q.
The procedures for projection, lifting and restriction guarantee the substitution
property f./
D
.
Given that all the operators used to express the solution of regular language
equations have constructive counterparts on automata, we conclude that there is an
effective (constructive) way to solve equations over regular languages.
As an example, given a regular language equation A
X
C ,whereA is a
regular language over alphabet I
U , C is over I
O, and the unknown regular
language X is over U
O, an algorithm to build X follows.
Procedure 2.3.1.
Input: Regular language equation
A
X
C
; Output: Largest
regular language solution
X
1. Consider the finite automata F.A/ and F.C/ corresponding, respectively, to
regular languages A and C .
2. De
te
rminize F.C/ by subset construction, if it is a NDFA. The automaton F.C/
of C is obtained by interchanging the sets of accepting and non-accepting states
of the determinization of F.C/.
3. Lift the language A to O by replacing each labe
l .
i;
u
/ of a transition of F.A/
with all triples .i;
u
;o/, o
2
O. Lift the language C to U by replacing each label
.i; o/ of a transition of F.C
/ w
ith all triples .i;
u
;o/,
u
2
U .
4. Build the automaton F.A
\
C/of the int
ers
ection A
\
C . The states are pairs of
states of the lifted automata F.A/ and F.C/, the initial state is the pair of initial
states, and a state of the intersection is accepting if both states of the pair are
accepting. There is a transition
fr
om the state .s
1
;s
2
/ to the state .s
1
;s
2
/ labeled
with action .i;
u
;o/ in F.A
\
C/, if there are corresponding transiti
on
s labeled
with .i;
u
;o/fr
om
state s
1
to state s
1
in F.A/ a
nd
from s
2
to s
2
in F.C/.
5. Project F.A
\
C/ to U
O to obtain F.A
C/ by deleting i from the labels
.i;
u
;o/. Projection i
n g
eneral makes the finite automaton non-deterministic.
6. De
termin
ize F.A
C/ by subset construction, if it is a NDF
A. The
automaton
F.A
C/corresponding to the regular language solution X
D
A
C is obtained
by interchanging the
s
ets of accepting and non-accepting states of the deter-
minization of F.A
C/.
Notice that Procedure
2.3.1
holds for any regular language, not only for prefix-
closed languages as in restricted versions reported in the literature.
A companion procedure to solve the regular language equation under parallel
composition A
˘
X
C is obtained from Procedure
2.3.1
, after replacing the
Search WWH ::
Custom Search