Information Technology Reference
In-Depth Information
1
:
proc
BasicBisimReduction
(
A
)
≡
2
:
/* Init:
∀q ∈ Q. C
−
1
(
q
):=1,and
∀q ∈ F. C
0
(
q
):=1
, ∀q ∈ Q \ F. C
0
(
q
):=2.*/
3
:
i
:= 0;
4
:
while
|C
i
(
Q
)
|
=
|C
i−
1
(
Q
)
|
do
5
:
i
:=
i
+1
6
:
foreach
q ∈ Q
do
7
:
C
i
(
q
):=
C
i−
1
(
q
)
, ∪
(
q,a,q
)
∈ʴ
{
(
C
i−
1
(
q
)
,a
)
}
8
:
od
9
:
Rename colour set
C
n
(
Q
), with
{
1
,...,|C
i
(
Q
)
|}
, using lexicogr. ordering.
10
:
od
11
:
C
:=
C
i
;
return
A
:=
Q
:=
C
(
Q
)
,ʴ
,q
I
:=
C
(
q
I
)
,F
:=
C
(
F
)
;
12
:
/*
ʴ
defined so that (
C
(
q
1
)
,a,C
(
q
2
))
∈ ʴ
iff (
q
1
,a,q
2
)
∈ ʴ
for
q
1
,q
2
∈ Q
*/
Fig. 1.
Basic Bisimulation Reduction Algorithm [3]
Our formalisation has revealed that there is a mistake in the initialisation of the
algorithm, which we have corrected in our implementation.
The second optimisation is
ʱ-balls reduction
, which collapses strongly con-
nected components (SCCs) that only containonesingleletterasedgelabel.
The rest of the paper is organised as follows: Section 2 gives some preliminar-
ies. Section 3 recalls the two optimisations of [3] in turn. Section 4 presents our
Isabelle formalisations of those algorithms, and Sec. 5 concludes.
2 Preliminaries
We recall the basic notions of automata as used by [3]; for more details see [10].
Usually, Buchi (or finite) automata have transitions labelled with characters
from an alphabet
ʣ
. In [3], a generalisation of such labellings is considered, but
for our purposes, this is not necessary and so we assume simple characters. We
assume that a Buchi automaton
A
is given by
Q,ʴ,q
I
,F
.Here
Q
is a set of
states,
ʴ
ↆ
(
Q
×
ʣ
×
Q
) is the transition relation,
q
I
∈
Q
is the initial state, and
F
Q
is the set of final states. The language
L
(
A
) is defined as the set of those
ˉ
-words which have an accepting run in
A
,wherea
run
on word
w
=
a
1
a
2
...
is
a sequence
q
0
q
1
q
2
...
such that
q
0
=
q
I
and (
q
i
,a
i
+1
,q
i
+1
)
ↆ
∈
ʴ
for all
i
≥
0, and
it is
accepting
if
q
i
∈
F
for infinitely many
i
.
Isabelle/HOL [7] is an interactive theorem prover based on Higher-Order Logic
(HOL). You can think of HOL as a combination of a functional programming
language with logic. Isabelle/HOL aims at being readable by humans and thus
follows the usual mathematical notation, but still the syntax needs some expla-
nations which we provide when we come to the examples. In our presentation of
Isabelle code we have stayed faithful to the sources.
3 The Original Algorithms
3.1 The Bisimulation Reduction Algorithm
Fig. 1 shows the basic bisimulation reduction algorithm in pseudo-code. The let-
ter
C
with a superscript refers to the iterations of the computation of a colouring.
