The automata-theoretic approach to model checking requires two basic
ingredients: a translation from logic to automata, and an algorithm
for checking language emptiness. LTL model checking has
traditionally been based on (generalized) Büchi automata. Weak
alternating automata provide an attractive alternative because there
is an elegant and linear-time translation from LTL. However, due to
their intricate combinatorial structure, no direct algorithm for
deciding the emptiness problem for these automata has been known,
and implementations have relied on an exponential translation of
weak alternating to nondeterministic Büchi automata. In this paper,
we fill this gap by proposing an algorithm to decide language
emptiness for the subclass of weak alternating automata that result
from the translation of LTL formulas. Our approach makes use of two
observations: first, runs of weak alternating automata can be
represented as dags and second, the transition graphs of linear weak
alternating automata are of restricted combinatorial structure. Our
algorithm computes strongly connected components of the graph of
reachable configurations, the emptiness criterion being expressed in
terms of the set of self loops that can be avoided within an SCC.
@TechReport{merz:emptiness-waa,
author = {Stephan Merz and Ali Sezgin},
title = {Emptiness of Linear Weak Alternating Automata},
institution = {LORIA},
year = 2003,
month = dec
}
Stephan Merz
Last modified: Wed Jun 4 13:18:57 CEST 2003