Information Technology Reference
In-Depth Information
Buchi Automata Optimisations Formalised
in Isabelle/HOL
Alexander Schimpf
1
,
and Jan-Georg Smaus
2
1
Institut fur Informatik, Universitat Freiburg, Germany
2
IRIT, Universite de Toulouse, France
smaus@irit.fr
Abstract.
In applications of automata theory, one is interested in re-
ductions in the size of automata that preserve the recognised language.
For Buchi automata, two optimisations have been proposed: bisimulation
reduction, which computes equivalence classes of states and collapses
them, and
ʱ
-balls reduction, which collapses strongly connected com-
ponents (SCCs) of an automaton that only contain one single letter as
edge label. In this paper, we present a formalisation of these algorithms
in Isabelle/HOL, providing a formally verified implementation.
1
Introduction
Model-checking is an important method for proving systems correct, and is ap-
plied in industrial practice [1]. In previous work [2], we present a reference im-
plementation for an LTL (linear temporal logic) model checker for finite-state
systems a la SPIN [5]. The model checker follows the well-known automata-
theoretic approach. Given a finite-state program
P
andanLTLformula
ˆ
,two
Buchi automata are constructed: the
system automaton
that recognises the ex-
ecutions of
P
,andthe
property
or
formula automaton
expressing all potential
executions that violate
ˆ
, respectively. Then the product of the two automata is
computed and tested on-the-fly for emptiness. This implementation is realised
and verified using Isabelle/HOL [7].
One important part of automata-based model checking is the translation of an
LTL formula into a Buchi automaton. The standard algorithm for this problem
has been proposed by Gerth
et al.
[4]. Previously to [2], we have implemented
and verified this algorithm in Isabelle/HOL [8]. In this paper, we consider two
of the optimisations proposed by Etessami and Holzmann [3] to reduce the size
of the formula automaton.
In model checking, the system automaton is usually much larger than the
property automaton, but since the size of the property automaton is a mul-
tiplicative factor of the overall complexity, it is worthwhile to put substantial
effort into its optimisation [3].
The first optimisation is
bisimulation
reduction, which computes equivalence
classes of states and collapses them. The algorithm of [3] uses a so-calledcolouring.
