Information Technology Reference
In-Depth Information
definition
LBA_reduce_balls_aux ::
"[('q, 'l, 'more) LBA_scheme, 'q set set]
⃒
(('q, 'l, 'more) LBA_scheme
×
'q set set) nres"
where
"LBA_reduce_balls_aux
A
SCCs
≡
FOREACHi
(LBA_reduce_balls_aux_foreach_inv
A
SCCs)
SCCs
(
ʻ
Q(
A
R
, SCCs
R
).
if
¬
ball
L
A
R
Q then RETURN (
A
R
, {Q}
∪
SCCs
R
)
else if scc_trivial
A
R
(
GA
R
Q)
then RETURN (remove_states
A
R
Q, SCCs
R
)
else if
∀
q
∈
Q.
¬FA
R
q
then RETURN (remove_states
A
R
Q, SCCs
R
)
else if (
∃
q. Q = {q}) then RETURN (
A
R
, {Q}
∪
SCCs
R
)
else
case ball
L
_get_
ʱ A
R
Qof
None
⃒
RETURN (
A
R
, {Q}
∪
SCCs
R
)
| Some
ʱ ⃒
do { (
A
R
,Q
R
)
←
LBA_remove_
ʱ
ball
A
R
Q;
ASSERT (Q
R
ↆ
Q
∧
Q
R
=
{});
RETURN (
A
R
,{Q
R
}
∪
SCCs
R
)}
)
(
A
, {})"
Fig. 10.
Auxiliary definition for
ʱ
-balls reduction
definition
LBA_reduce_balls ::
"('q, 'l, 'more) LBA_scheme
⃒
(('q, 'l, 'more) LBA_scheme
×
'q set set) nres"
where
"LBA_reduce_balls
A≡
do {
←
tarjan
A
(
IA
);
SCCs
(
A
R
, SCCs
R
)
←
LBA_reduce_balls_aux
A
SCCs;
RETURN (
A
R
, SCCs
R
)
}"
Fig. 11.
Ball reduction on LBAs
5Con lu on
We have presented an Isabelle/HOL formalisation of two Buchi automata opti-
misations proposed by [3]. The context of this work is explained in detail in [2]:
implementing full-fledged model checkers verified in Isabelle/HOL. Within this
endeavour, it is worthwhile to invest effort in the optimisation of the property
automaton. While the optimisations are particularly relevant for model checking,
they are abstract enough to be applicable to Buchi automata in general.
