\omega-regular Languages are Testable with a Constant Number of Queries
=========================================================================
We continue the study of combinatorial property testing. For a
property \psi, an \epsilon-test for \psi, for 0 < \epsilon \leq 1, is
a randomized algorithm that given an input x, returns "yes" if x
satisfies \psi, and returns "no" with high probability if x is
\epsilon-far from satisfying \psi, where \epsilon-far essentially
means that an \epsilon-fraction of x needs to be changed in order for
it to satisfy \psi. In [AKNS99], Alon et al. show that regular
languages are \epsilon-testable with a constant (depends on \psi and
\epsilon and independent of x) number of queries. We extend the
result in [AKNS99] to \omega-regular languages: given a
nondeterministic Buchi automaton A on infinite words and a small
\epsilon> 0, we describe an algorithm that gets as input an infinite
lasso-shape word of the form x \cdot y^\omega, for finite words x and
y, samples only a constant number of letters in x and y, returns "yes"
if w \in L(A), and returns "no" with probability 2/3 if w is
\epsilon-far from L(A). We also discuss the applicability of property
testing to formal verification, where \omega-regular languages are
used for the specification of the behavior of nonterminating reactive
systems, and computations correspond to lasso-shape words.