Advertisement

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

  • Hana Chockler
  • Orna Kupferman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2483)

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [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
  2. [AK]
    N. Alon and M. Krivelevich. Testing k-colorability. SIAM Journal on Discrete Mathematics. to appear.Google Scholar
  3. [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
  4. [AS85]
    B. Alpern and F.B. Schneider. Defining liveness. IPL, 21:181–185, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [BCCZ99]
    A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS, LNCS 1579, 1999.Google Scholar
  6. [BR00]
    M.A. Bender and D. Ron. Testing acyclicity of directed graphs in sublinear time. In 27th ICALP, 2000.Google Scholar
  7. [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
  8. [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
  9. [CGP99]
    E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.Google Scholar
  10. [dRLP98]
    W-P. de Roever, H. Langmaack, and A. Pnueli, editors. Compositionality: The Significant Difference. COMP, LNCS 1536, 1998.Google Scholar
  11. [Fix02]
    L. Fix. Application of ɛ-test to random simulation. Private communication, 2002.Google Scholar
  12. [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
  13. [GR97]
    O. Goldreich and D. Ron. Property testing in bounded degree graphs. In 25th STOC, pp. 406–415, 1997.Google Scholar
  14. [GR99]
    O. Goldreich and D. Ron. A sublinear bipartite tester for bounded degree graphs. Combinatorica, 19(3):335–373, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  15. [Hol91]
    G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991.Google Scholar
  16. [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
  17. [Lan69]
    L.H. Landweber. Decision problems forω-automata. Mathematical Systems Theory, 3:376–384, 1969.zbMATHCrossRefMathSciNetGoogle Scholar
  18. [McM93]
    K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  19. [McN66]
    R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521–530, 1966.zbMATHCrossRefMathSciNetGoogle Scholar
  20. [PR99]
    M. Parnas and D. Ron. Testing the diameter of graphs. In RANDOM, pp. 85–96, 1999.Google Scholar
  21. [PRR01]
    M. Parnas, D. Ron, and R. Rubinfeld. Testing parenthesis languages. In 5th RANDOM, pp. 261–272, 2001.Google Scholar
  22. [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
  23. [Rab69]
    M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1–35, 1969.zbMATHCrossRefMathSciNetGoogle Scholar
  24. [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
  25. [Saf88]
    S. Safra. On the complexity of ω-automata. In 29th FOCS, pp. 319–327, 1988.Google Scholar
  26. [Sip99]
    H.B. Sipma. Diagram-basedVerification of Discrete, Real-time and Hybrid Systems. PhD thesis, Stanford University, Stanford, California, 1999.Google Scholar
  27. [Sis94]
    A.P. Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6:495–511, 1994.zbMATHCrossRefGoogle Scholar
  28. [Tho90]
    W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pp. 165–191, 1990.Google Scholar
  29. [VW94]
    M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1): 1–37, November 1994.Google Scholar
  30. [Wes89]
    C.H West. Protocol validation in complex systems. In 8th PODC, pp. 303–312, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Hana Chockler
    • 1
  • Orna Kupferman
    • 1
  1. 1.School of Engineering and Computer ScienceHebrew UniversityJerusalemIsrael

Personalised recommendations