Information Technology Reference
In-Depth Information
definition
(
in
LBA)
"LBA_bpr_C_char
≡ ʻ
C.
∀
q
∈Q A
.
∀
q'
∈Q A
.
Cq=Cq'
−ₒ
(
FA
q
←ₒ F A
q')
∧LA
q=
LA
q'
∧
C ' successors q = C ' successors q'"
Fig. 5.
Characterisation of the colouring
lemma
(
in
LBA) LBA_bpr_C_correct:
"LBA_bpr_C
A≤
SPEC LBA_bpr_C_char"
Fig. 6.
Correctness property of the colouring
finite. Otherwise we could not apply the above shown properties about
set enum
.
Finiteness is given here by an implicit assumption denoted by “(
in
LBA
)”.
This characterisation turns out to be a sucient condition for proving the
correctness of the resulting coloured automaton. To obtain the automaton, we
apply a renaming function
LBA rename
which takes an LBA and a colouring
function
C
and returns the LBA where each state has been renamed using the
colouring function. The renaming function has properties shown in Figure 7.
For example the second line of the lemma states that the initial states of the
renamed automaton are exactly the renamings of the initial states of the original
automaton. The other lines state similarly that the transition function, the final
states, and the labels are preserved by the renaming.
The term
inv into Qfq
gives “the”
2
inverse element of
q
under
f
in
Q
.In
the case that this inverse is unique, i.e.,
f
is injective on
Q
, it is straightforward
to show that the renaming preserves language equivalence. However, the very
purpose of the colouring is to
reduce
the number of states, hence not to be injec-
tive! But even in this general case, language equivalence holds, as is expressed
by the following lemma:
lemma
(
in
LBA) LBA_bpr_C_rename_accept_iff:
assumes
"LBA_bpr_C_char C"
shows
"
∀
w. LBA_accept (LBA_rename
A
C) w
←ₒ
A
w"
LBA_accept
” direction consists
of taking a run (sequence of states)
r
for word
w
of the input automaton and
colouring
r
componentwise using
C
, i.e.,
r
is mapped to a run
C
The proof of the lemma works constructively. The “
←−
ⓦ
r
in the
coloured automaton.
The “
−→
” direction requires an auxiliary function:
2
This is the famous
operator of HOL: It represents an arbitrary but fixed term
fulfilling a given property.
