Linear weak alternating automata and the model checking problem
Diploma Thesis
Moritz Hammer
Abstract
Automata-based model checking is a widely used approach towards
software model checking. Traditionally, nondeterministic Buechi automata
are used to represent the temporal logic property to be checked. We take a
look at a special kind of alternating automata, the linear weak alternating
automata. They can be constructed from LTL formula in an elegant way in
linear time. The emptiness check on linear weak alternating automata, on the
other hand, requires exponential time, whereas the emptiness of
nondeterministic Büuchi automata, being of exponential size with respect to
the size of the LTL formula they represent, can be checked in linear
time. We try take advantage of the better constructibility of linear
weak alternating automata in model checking by implementing a model checker
using "on-the-fly generalized Buechi automata generation". The emptiness
check is conducted using an extended version of Tarjan's algorithm. After
obtaining promising results, we adapt the SPIN model checker to the new
algorithm.
[PDF], [PS]
Moritz Hammer
Last modified: Tue Apr 12 11:22:45 CEST 2005