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

- 1 Citations
- 707 Downloads

## 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.

## Keywords

Model Check Regular Language Query Complexity Property Testing Input Word## Preview

Unable to display preview. Download preview PDF.

## References

- [AFKS99]N. Alon, E. Fischer, M. Krivelevich, and M. Szegedy. Efficient testing of large graphs. In
*40th IEEE FOCS*, pp. 645–655, 1999.Google Scholar - [AK]N. Alon and M. Krivelevich. Testing k-colorability.
*SIAM Journal on Discrete Mathematics*. to appear.Google Scholar - [AKNS99]N. Alon, M. Krivelevich, I. Newman, and M. Szegedy. Regular languages are testable with a constant number of queries. In
*40th IEEE FOCS*, pp. 645–655, 1999.Google Scholar - [AS85]B. Alpern and F.B. Schneider. Defining liveness.
*IPL*, 21:181–185, 1985.zbMATHCrossRefMathSciNetGoogle Scholar - [BCCZ99]A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In
*TACAS*,*LNCS*1579, 1999.Google Scholar - [BR00]M.A. Bender and D. Ron. Testing acyclicity of directed graphs in sublinear time. In
*27th ICALP*, 2000.Google Scholar - [Büc62]J.R. Büchi. On a decision method in restricted second order arithmetic. In
*ICLMPS 1960*, pp. 1–12, Stanford, 1962. Stanford University Press.Google Scholar - [CD88]E.M. Clarke and I.A. Draghicescu. Expressibility results for linear-time and branching-time logics. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors,
*REX Workshop*,*LNCS*354, pp. 428–437. 1988.Google Scholar - [CGP99]E.M. Clarke, O. Grumberg, and D. Peled.
*Model Checking*. MIT Press, 1999.Google Scholar - [dRLP98]W-P. de Roever, H. Langmaack, and A. Pnueli, editors.
*Compositionality: The Significant Difference. COMP*,*LNCS*1536, 1998.Google Scholar - [Fix02]L. Fix. Application of ɛ-test to random simulation. Private communication, 2002.Google Scholar
- [GGR98]O. Goldreich, S. Goldwasser, and D. Ron. Property testing and its connection to learning and approximation.
*Journal of ACM*, 45(4):653–750, 1998.zbMATHCrossRefMathSciNetGoogle Scholar - [GR97]O. Goldreich and D. Ron. Property testing in bounded degree graphs. In
*25th STOC*, pp. 406–415, 1997.Google Scholar - [GR99]O. Goldreich and D. Ron. A sublinear bipartite tester for bounded degree graphs.
*Combinatorica*, 19(3):335–373, 1999.zbMATHCrossRefMathSciNetGoogle Scholar - [Hol91]G. Holzmann.
*Design and Validation of Computer Protocols*. Prentice-Hall International Editions, 1991.Google Scholar - [KV01]O. Kupferman and M.Y. Vardi. Model checking of safety properties.
*Formal methods in System Design*, 19(3):291–314, November 2001.Google Scholar - [Lan69]L.H. Landweber. Decision problems forω-automata.
*Mathematical Systems Theory*, 3:376–384, 1969.zbMATHCrossRefMathSciNetGoogle Scholar - [McM93]K.L. McMillan.
*Symbolic Model Checking*. Kluwer Academic Publishers, 1993.Google Scholar - [McN66]R. McNaughton. Testing and generating infinite sequences by a finite automaton.
*Information and Control*, 9:521–530, 1966.zbMATHCrossRefMathSciNetGoogle Scholar - [PR99]M. Parnas and D. Ron. Testing the diameter of graphs. In
*RANDOM*, pp. 85–96, 1999.Google Scholar - [PRR01]M. Parnas, D. Ron, and R. Rubinfeld. Testing parenthesis languages. In
*5th RANDOM*, pp. 261–272, 2001.Google Scholar - [PRS01]M. Parnas, D. Ron, and A. Samorodnitsky. Proclaiming dictators and juntas or testing boolean formulae. In
*5th RANDOM*, pp. 273–284, 2001.Google Scholar - [Rab69]M.O. Rabin. Decidability of second order theories and automata on infinite trees.
*Transaction of the AMS*, 141:1–35, 1969.zbMATHCrossRefMathSciNetGoogle Scholar - [RS96]R. Rubinfeld and M. Sudan. Robust characterization of polynomials with applications to program testing.
*SI AM Journal on Computing*, 25(2): 252–271, 1996.zbMATHCrossRefMathSciNetGoogle Scholar - [Saf88]S. Safra. On the complexity of ω-automata. In
*29th FOCS*, pp. 319–327, 1988.Google Scholar - [Sip99]H.B. Sipma.
*Diagram-basedVerification of Discrete, Real-time and Hybrid Systems*. PhD thesis, Stanford University, Stanford, California, 1999.Google Scholar - [Sis94]A.P. Sistla. Safety, liveness and fairness in temporal logic.
*Formal Aspects of Computing*, 6:495–511, 1994.zbMATHCrossRefGoogle Scholar - [Tho90]W. Thomas. Automata on infinite objects.
*Handbook of Theoretical Computer Science*, pp. 165–191, 1990.Google Scholar - [VW94]M. Y. Vardi and P. Wolper. Reasoning about infinite computations.
*Information and Computation*, 115(1): 1–37, November 1994.Google Scholar - [Wes89]C.H West. Protocol validation in complex systems. In
*8th PODC*, pp. 303–312, 1989.Google Scholar