Abstract
We continue the study of combinatorial property testing. For a property \psi, an
ɛ-test for \psi, for 0 \leq ɛ \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
ɛ-far from satisfying \psi, where ɛ-far essentially means that an ɛ-fraction of x needs to be changed in order for it to satisfy \psi. In (Proceedings of the 40th IEEE Symposium on Foundations of Computer Science, 1999, pp. 645–655), Alon et al. show that regular languages are ɛ-testable with a constant (depends on \psi and
ɛ and independent of x) number of queries. We extend the result in (Proceedings of the 40th IEEE Symposium on Foundations of Computer Science, 1999, pp. 645–655) to \omega-regular languages: given a nondeterministic Büchi automaton on infinite words and a small ɛ, we describe an algorithm that gets as input an infinite lasso-shape word w 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 is in 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 \omega-regular languages are used for the specification of the behavior of nonterminating reactive systems, and computations correspond to lasso-shape words.
ɛ-test for \psi, for 0 \leq ɛ \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
ɛ-far from satisfying \psi, where ɛ-far essentially means that an ɛ-fraction of x needs to be changed in order for it to satisfy \psi. In (Proceedings of the 40th IEEE Symposium on Foundations of Computer Science, 1999, pp. 645–655), Alon et al. show that regular languages are ɛ-testable with a constant (depends on \psi and
ɛ and independent of x) number of queries. We extend the result in (Proceedings of the 40th IEEE Symposium on Foundations of Computer Science, 1999, pp. 645–655) to \omega-regular languages: given a nondeterministic Büchi automaton on infinite words and a small ɛ, we describe an algorithm that gets as input an infinite lasso-shape word w 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 is in 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 \omega-regular languages are used for the specification of the behavior of nonterminating reactive systems, and computations correspond to lasso-shape words.
Original language | English |
---|---|
Pages (from-to) | 71-92 |
Number of pages | 22 |
Journal | Theoretical Computer Science |
Volume | 329 |
Issue number | 1-3 |
Publication status | Published - 2004 |