Advertisement

Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata

  • Orna Kupferman
  • Nir Piterman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)

Abstract

The nonemptiness problem for nondeterministic automata on infinite words can be reduced to a sequence of reachability queries. The length of a shortest witness to the nonemptiness is then polynomial in the automaton. Nonemptiness algorithms for alternating automata translate them to nondeterministic automata. The exponential blow-up that the translation involves is justified by lower bounds for the nonemptiness problem, which is exponentially harder for alternating automata. The translation to nondeterministic automata also entails a blow-up in the length of the shortest witness. A matching lower bound here is known for cases where the translation involves a 2 O(n) blow up, as is the case for finite words or Büchi automata.

Alternating co-Büchi automata and witnesses to their nonemptiness have applications in model checking (complementing a nondeterministic Büchi word automaton results in a universal co-Büchi automaton) and synthesis (an LTL specification can be translated to a universal co-Büchi tree automaton accepting exactly all the transducers that realize it). Emptiness algorithms for alternating co-Büchi automata proceed by a translation to nondeterministic Büchi automata. The blow up here is 2 O(n logn), and it follows from the fact that, on top of the subset construction, the nondeterministic automaton maintains ranks to the states of the alternating automaton. It has been conjectured that this super-exponential blow-up need not apply to the length of the shortest witness. Intuitively, since co-Büchi automata are memoryless, it looks like a shortest witness need not visit a state associated with the same set of states more than once. A similar conjecture has been made for the width of a transducer generating a tree accepted by an alternating co-Büchi tree automaton. We show that, unfortunately, this is not the case, and that the super-exponential lower bound on the witness applies already for universal co-Büchi word and tree automata.

References

  1. 1.
    Brzozowski, J.A., Leiss, E.: Finite automata and sequential networks. TCS 10, 19–35 (1980)CrossRefzbMATHGoogle Scholar
  2. 2.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pp. 1–12. Stanford Univ. Press (1962)Google Scholar
  3. 3.
    Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 2nd edn. Addison-Wesley, Reading (2000)zbMATHGoogle Scholar
  5. 5.
    Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Kupferman, O., Sheinvald-Faragy, S.: Finding shortest witnesses to the nonemptiness of automata on infinite words. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 492–508. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM ToCL 2(2), 408–429 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th FOCS, pp. 531–540 (2005)Google Scholar
  9. 9.
    Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)zbMATHGoogle Scholar
  10. 10.
    Liu, W.: A tighter analysis of Piterman determinization construction (2007), http://nlp.nudt.edu.cn/~lww/pubs.htm
  11. 11.
    McNaughton, R.: Testing and generating infinite sequences by a finite automaton. I&C 9, 521–530 (1966)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. TCS 32, 321–330 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. TCS 141, 69–107 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. LMCS 3(3), 5 (2007)zbMATHGoogle Scholar
  15. 15.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th POPL, pp. 179–190 (1989)Google Scholar
  16. 16.
    Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS 141, 1–35 (1969)MathSciNetzbMATHGoogle Scholar
  17. 17.
    Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, pp. 133–191 (1990)Google Scholar
  18. 18.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st LICS, pp. 332–344 (1986)Google Scholar
  19. 19.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C 115(1), 1–37 (1994)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Orna Kupferman
    • 1
  • Nir Piterman
    • 2
  1. 1.Hebrew UniversityIsrael
  2. 2.Imperial College LondonUK

Personalised recommendations