ω-Regular Languages Are Testable with a Constant Number of Queries

Abstract

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