TY - CHAP
T1 - omega-Regular Languages Are Testable with a Constant Number of Queries
AU - Chockler, Hana
AU - Kupferman, Orna
PY - 2002
Y1 - 2002
N2 - 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.
AB - 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.
M3 - Conference paper
VL - 2483
T3 - Lecture Notes in Computer Science
SP - 26
EP - 28
BT - Randomization and Approximation Techniques, 6th International Workshop (RANDOM)
PB - Springer
ER -