Abstract

We solve the open problems of translating, when possible, all common classes of nondeterministic word automata to deterministic and nondeterministic co-Büchi word automata. The handled classes include Büchi, parity, Rabin, Streett and Muller automata. The translations follow a unified approach and are all asymptotically tight.

The problem of translating Büchi automata to equivalent co-Büchi automata was solved in [2], leaving open the problems of translating automata with richer acceptance conditions. For these classes, one cannot easily extend or use the construction in [2]. In particular, going via an intermediate Büchi automaton is not optimal and might involve a blow-up exponentially higher than the known lower bound. Other known translations are also not optimal and involve a doubly exponential blow-up.

We describe direct, simple, and asymptotically tight constructions, involving a 2Θ(n) blow-up. The constructions are variants of the subset construction, and allow for symbolic implementations. Beyond the theoretical importance of the results, the new constructions have various applications, among which is an improved algorithm for translating, when possible, LTL formulas to deterministic Büchi word automata.

References

  1. 1.
    Accellera. Accellera organization inc. (2006), http://www.accellera.org
  2. 2.
    Boker, U., Kupferman, O.: Co-ing Büchi made tight and helpful. In: Proc. 24th IEEE Symp. on Logic in Computer Science, pp. 245–254 (2009)Google Scholar
  3. 3.
    Boker, U., Kupferman, O., Rosenberg, A.: Alternation removal in büchi automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 76–87. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  4. 4.
    Cai, Y., Zhang, T., Luo, H.: An improved lower bound for the complementation of Rabin automata. In: Proc. 24th IEEE Symp. on Logic in Computer Science, pp. 167–176 (2009)Google Scholar
  5. 5.
    Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic ω-automata vis-a-vis deterministic Büchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol. 834, pp. 378–386. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  6. 6.
    Kupferman, O.: Tightening the exchange rates between automata. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 7–22. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Kupferman, O., Morgenstern, G., Murano, A.: Typeness for ω-regular automata. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 324–338. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    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
  9. 9.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, pp. 531–540 (2005)Google Scholar
  10. 10.
    Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)MATHGoogle Scholar
  11. 11.
    Landweber, L.H.: Decision problems for ω–automata. Mathematical Systems Theory 3, 376–384 (1969)MathSciNetCrossRefGoogle Scholar
  12. 12.
    McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Information and Control 9, 521–530 (1966)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Morgenstern, A., Schneider, K.: From LTL to symbolically represented deterministic automata. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 279–293. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  15. 15.
    Safra, S., Vardi, M.Y.: On ω-automata and temporal logic. In: Proc. 21st ACM Symp. on Theory of Computing, pp. 127–137 (1989)Google Scholar
  16. 16.
    Seidl, H., Niwiński, D.: On distributive fixed-point expressions. Theoretical Informatics and Applications 33(4-5), 427–446 (1999)MathSciNetCrossRefGoogle 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.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Udi Boker
    • 1
  • Orna Kupferman
    • 1
  1. 1.School of Computer Science and EngineeringHebrew UniversityIsrael

Personalised recommendations