Information Technology Reference
In-Depth Information
lemma
LBA_rename_simps:
"
ʴ
(LBA_rename
A
C)qa=C'
ʴ A
(inv_into (
QA
) C q) a"
"
I
(LBA_rename
A
C) = C '
IA
"
"
F
(LBA_rename
A
C) q
←ₒ F A
(inv_into (
QA
) C q)"
"
L
(LBA_rename
A
C) q =
LA
(inv_into (
QA
) C q)"
Fig. 7.
Renaming function for LBAs
q
a
q
a
1
a
Fig. 8.
An LBA and its colouring
fun
bpr_run
where
"bpr_run
A
C r q0 0 = q0"
| "bpr_run
A
C r q0 (Suc k)
= (SOME q'. C q' = C (inv_into (
QA
) C (r (Suc k)))
∧
q'
∈ʴ
L
A
(bpr_run
A
C r q0 k))"
This function is needed for the following reason: if we start from a run
r
for
w
in the coloured automaton and use
inv into Qfq
to compute a corresponding
state in the input automaton for each state
q
in
r
, then these states do not
necessarily “fit together”, i.e., they may not form a run in the input automaton.
Example 1.
Figure 8 shows an LBA accepting the word
aaa . . .
on the left, and
the simplified automaton obtained by colouring on the right. Obviously, the
state sequence in the coloured automaton is always simply a sequence of 1's.
The inverse of “1” is either
q
1
or
q
2
, so simply translating 11
...
back into the
original LBA would give either
q
1
q
1
...
or
q
2
q
2
...
. In neither case this would
correspond to a run of the original LBA.
As the example shows, constructing a run in the original LBA, given a run
in the coloured LBA, is not so simple and has to be done step by step starting
from the initial state. This is what the function
bpr run
is good for. It starts by
taking an inverse of the initial state of the run
r
of the coloured automaton, and
then always picks an appropriate inverse for each next state in
r
. The existence
of such an inverse is guaranteed by the assumption that the colouring
C
fulfils
the characterisation according to Figure 5.
The entire procedure for constructing the coloured automaton is then given
in Figure 9. By the considerations given above, this construction is correct:
lemma
in
LBA) LBA_bpr_correct:
"LBA_bpr
A
≤
SPEC (
ʻA
C
. LBA
A
C
(
∧
(
∀
w. LBA_accept
A
C
w
←ₒ
LBA_accept
A
w))"
