Information Technology Reference
In-Depth Information
definition
LBA_bpr :: "('q, 'l, _) LBA_scheme
⃒
(nat, 'l) LBA nres"
where
"LBA_bpr
A≡
do {
C
←
LBA_bpr_C
A
;
RETURN (LBA_rename
A
C)
}"
Fig. 9.
Procedure for constructing the coloured automaton
In addition to language equivalence we also show that the coloured automaton
is well-formed, i.e.
LBA
A
C
holds.
4.2
α
-Balls Reduction
Most of the Isabelle development on this topic uses in fact BA, not LBA, and the
formalisation of
ʱ
-balls reduction for LBA is based on the one for BA. However,
we focus here on LBA because the use of LBA required certain adaptations that
partly make the contribution of our work.
An
ʱ
-ball for LBA has, of course, an Isabelle definition. However, this is not
very readable and so we prefer to present the following characterisation:
lemma
ʱ
ball
L
_full_def:
"
ʱ
ball
L
A ʱ
Q
≡
GA
Q
∈
sccs
A∧
Q
=
{}
∧
(
∀
q
∈
Q. successors
A
q
ↆ
Q)
∧
(
∀
q
∈
Q.
LA
q=
ʱ
)"
The lemma says that
Q
is an
ʱ
-ball iff the following four conditions hold: (1)
the graph of
A
, restricted to
Q
,isanSCCof
A
;(2)
Q
=
∅
;(3)thereisnoedge
leading out of
Q
; (4) all states in
Q
are labelled with
ʱ
.
Fig. 10 gives an auxiliary definition for balls reduction. There is a loop for
working through the SCCs. Trivial balls or balls without accepting states are
removed. One-element balls are left untouched. Finally, non-trivial balls are col-
lapsed to a single state. Based on the computation of SCCs according to Tarjan's
algorithm [9] we obtain a function that computes the SCCs and then reduces,
as shown in Figure 11. The ball reduction on LBAs thus returns a well-formed
equivalent automaton and a set
SCCs
R
representing its SCCs.
The correctness follows from the correctness of
LBA reduce ball aux
and
tarjan
:
lemma
(
in
LBA) LBA_reduce_balls_correct:
"LBA_reduce_balls
A≤
SPEC(
ʻ
(
A
R
, SCCs
R
).
A
R
∧
(
∀
w. LBA_accept
A
R
w
←ₒ
A
w)
LBA
LBA_accept
∧QA
R
=
SCCs
R
∧
pairwise_disjoint SCCs
R
∧
(
∀
Q
∈
SCCs
R
.
GA
R
Q
∈
sccs
A
R
∧
Q
=
{})
)"
