Rabin vs. Streett Automata

Author Udi Boker

Thumbnail PDF


  • Filesize: 0.49 MB
  • 15 pages

Document Identifiers

Author Details

Udi Boker

Cite AsGet BibTex

Udi Boker. Rabin vs. Streett Automata. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


The Rabin and Streett acceptance conditions are dual. Accordingly, deterministic Rabin and Streett automata are dual. Yet, when adding nondeterminsim, the picture changes dramatically. In fact, the state blowup involved in translations between Rabin and Streett automata is a longstanding open problem, having an exponential gap between the known lower and upper bounds. We resolve the problem, showing that the translation of Streett to Rabin automata involves a state blowup in $\Theta(n^2)$, whereas in the other direction, the translations of both deterministic and nondeterministic Rabin automata to nondeterministic Streett automata involve a state blowup in $2^{\Theta(n)}$. Analyzing this substantial difference between the two directions, we get to the conclusion that when studying translations between automata, one should not only consider the state blowup, but also the \emph{size} blowup, where the latter takes into account all of the automaton elements. More precisely, the size of an automaton is defined to be the maximum of the alphabet length, the number of states, the number of transitions, and the acceptance condition length (index). Indeed, size-wise, the results are opposite. That is, the translation of Rabin to Streett involves a size blowup in $\Theta(n^2)$ and of Streett to Rabin in $2^{\Theta(n)}$. The core difference between state blowup and size blowup stems from the tradeoff between the index and the number of states. (Recall that the index of Rabin and Streett automata might be exponential in the number of states.) We continue with resolving the open problem of translating deterministic Rabin and Streett automata to the weaker types of deterministic co-B\"uchi and B\"uchi automata, respectively. We show that the state blowup involved in these translations, when possible, is in $2^{\Theta(n)}$, whereas the size blowup is in $\Theta(n^2)$.
  • Finite automata on infinite words
  • translations
  • automata size
  • state space


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. U. Boker. On the (in)succinctness of Muller automata. In CSL, pages 12:1-12:16, 2017. Google Scholar
  2. U. Boker and O. Kupferman. Translating to co-Büchi made tight, unified, and useful. ACM Trans. Comput. Log., 13(4):29:1-29:26, 2012. Google Scholar
  3. U. Boker, O. Kupferman, and A. Rosenberg. Alternation removal in Büchi automata. In Proc. 37th Int. Colloq. on Automata, Languages, and Programming, volume 6199, pages 76-87, 2010. Google Scholar
  4. J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pages 1-12. Stanford University Press, 1962. Google Scholar
  5. Y. Cai and T. Zhang. Determinization complexities of ω automata. Submitted. Google Scholar
  6. Y. Cai and T. Zhang. A tight lower bound for Streett complementation. In FSTTCS, pages 339-350, 2011. Google Scholar
  7. Y. Cai, T. Zhang, and H. Luo. An improved lower bound for the complementation of Rabin automata. In LICS, pages 167-176, 2009. Google Scholar
  8. Y. Choueka. Theories of automata on ω-tapes: A simplified approach. Journal of Computer and Systems Science, 8:117-141, 1974. Google Scholar
  9. T. Colcombet and K. Zdanowski. A tight lower bound for determinization of transition labeled Büchi automata. In ICALP, pages 151-162, 2009. Google Scholar
  10. Y. Gurevich and L. Harrington. Trees, automata, and games. In Proc. 14th ACM Symp. on Theory of Computing, pages 60-65. ACM Press, 1982. Google Scholar
  11. S.C. Krishnan, A. Puri, and R.K. Brayton. Deterministic ω-automata vis-a-vis deterministic Büchi automata. In Algorithms and Computations, volume 834 of Lecture Notes in Computer Science, pages 378-386. Springer, 1994. Google Scholar
  12. O. Kupferman, G. Morgenstern, and A. Murano. Typeness for ω-regular automata. In 2nd Int. Symp. on Automated Technology for Verification and Analysis, volume 3299 of Lecture Notes in Computer Science, pages 324-338. Springer, 2004. Google Scholar
  13. W. Liu and J. Wang. A tighter analysis of Piterman’s Büchi determinization. Inf. Process. Lett., 109(16):941-945, 2009. Google Scholar
  14. C. Löding. Optimal bounds for the transformation of omega-automata. In Proc. 19th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 1738 of Lecture Notes in Computer Science, pages 97-109, 1999. Google Scholar
  15. R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521-530, 1966. Google Scholar
  16. M. Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 1988. Google Scholar
  17. S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321-330, 1984. Google Scholar
  18. A.W. Mostowski. Regular expressions for infinite trees and a standard form of automata. In Computation Theory, volume 208 of Lecture Notes in Computer Science, pages 157-168. Springer, 1984. Google Scholar
  19. D.E. Muller. Infinite sequences and finite machines. In Proc. 4th IEEE Symp. on Switching Circuit Theory and Logical design, pages 3-16, 1963. Google Scholar
  20. N. Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science, 3(3):5, 2007. Google Scholar
  21. M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1-35, 1969. Google Scholar
  22. S. Safra. Complexity of automata on infinite objects. PhD thesis, Weizmann Institute of Science, 1989. Google Scholar
  23. S. Safra. Exponential determinization for ω-automata with strong-fairness acceptance condition. In Proc. 24th ACM Symp. on Theory of Computing, 1992. Google Scholar
  24. S. Safra and M.Y. Vardi. On ω-automata and temporal logic. In Proc. 21st ACM Symp. on Theory of Computing, pages 127-137, 1989. Google Scholar
  25. S. Schewe. Büchi complementation made tight. In Proc. 26th Symp. on Theoretical Aspects of Computer Science, volume 3 of LIPIcs, pages 661-672. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2009. Google Scholar
  26. S. Schewe and T. Varghese. Determinising parity automata. In MFCS, pages 486-498, 2014. Google Scholar
  27. R.S. Streett. Propositional dynamic logic of looping and converse. Information and Control, 54:121-141, 1982. Google Scholar
  28. Qiqi Yan. Lower bounds for complementation of omega-automata via the full automata technique. Logical Methods in Computer Science, 4(1), 2008. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail