Information Technology Reference
In-Depth Information
so that the loop body will definitely be entered for
i
= 0 at least once. This is
shown in Fig. 3 and will be discussed in Sec. 4.1.
3.2
α
-Balls Reduction
This optimisation may appear simple and rather specialised, but in fact, it is
quite effective in our context of model checking, more precisely, on Buchi au-
tomata that are the result of a translation from
generalised
Buchi automata
which in turn are the output of the formula translation [4]. Note also that the
reduction does not work for finite automata; it only works for Buchi automata.
The idea of the reduction is that, if in a Buchi automaton we are ever stuck
in a component, and the only transition labels in this component are
ʱ
,and
there is some accepting state in the component, then we can treat the entire
component as a single accepting state with a self-transition labelled by
ʱ
.
ʣ,a
fixed-letter
ʱ
-ball
1
inside a Buchi automaton A is
Definition 1.
For ʱ
∈
asetQ
ↆ
Q of states such that:
1. ʱ
ʣ is the unique letter which labels the transitions inside Q
;
2. the nodes of Q
form an SCC of A;
3. there is no transition leaving Q
, i.e., no
(
q
,b,q
)
∈
ʴ where q
∈
Q
and
∈
Q
.
4. Q
∩
q/
∈
F
=
∅
.
,supposeQ
ↆ
Proposition 1.
Given a Buchi automaton A
=
Q,ʴ,q
I
,f
Q is
a fixed-letter ʱ-ball of A.LetA
=
Q
)
,ʴ
,q
I
Q
)
(
Q
\
∪{
q
new
}
,
(
F
\
∪{
q
new
}
where
Q
}∪{
Q
}
ʴ
=
{
(
q
1
,b,q
2
)
|
q
1
,q
2
∈
Q
\
(
q
1
,b,q
new
)
|
(
q
1
,b,q
2
)
∈
ʴ, q
1
∈
Q,q
2
∈
∪{
(
q
new
,ʱ,q
new
)
}
,
and q
I
Q
,elseq
I
=
q
I
.ThenL
(
A
)=
L
(
A
)
.
=
q
new
if q
I
∈
4
Isabelle Formalisation
The work presented in this paper is a fragment of a bigger library being developed
on automata in the context of model checking, in particular the construction of
the
property automaton
(see Sec. 1). Modularity, generality and reuse are impor-
tant concerns in this project, which is why the Isabelle code chunks presented
here exhibit some aspects that we do not discuss in all detail.
Generally, automata are represented as
record types
that are parametrised by
the type of the states and the type of the alphabet, among others. E.g., in line 2
in Fig. 3,
q
is the type of the states. The fields of these records, mostly denoted
by calligraphic letters, refer to the states, the final states, etc. E.g., in line 5 in
Fig. 3,
Q
gives the state set, and in line 7,
F
refers to being accepting.
1
[3] defines more generally: a
fixed-formula ʱ-ball
, i.e.,
ʱ
is a formula.
