A Tight Lower Bound for Streett Complementation

Authors Yang Cai, Ting Zhang

Thumbnail PDF


  • Filesize: 480 kB
  • 12 pages

Document Identifiers

Author Details

Yang Cai
Ting Zhang

Cite AsGet BibTex

Yang Cai and Ting Zhang. A Tight Lower Bound for Streett Complementation. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 339-350, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Finite automata on infinite words (omega-automata) proved to be a powerful weapon for modeling and reasoning infinite behaviors of reactive systems. Complementation of omega-automata is crucial in many of these applications. But the problem is non-trivial; even after extensive study during the past two decades, we still have an important type of omega-automata, namely Streett automata, for which the gap between the current best lower bound 2^(Omega(n lg nk)) and upper bound 2^(O (nk lg nk)) is substantial, for the Streett index size k can be exponential in the number of states n. In a previous work we showed a construction for complementing Streett automata with the upper bound 2^(O(n lg n+nk lg k)) for k = O(n) and 2^(O(n^2 lg n)) for k = omega(n). In this paper we establish a matching lower bound 2^(Omega (n lg n+nk lg k)) for k = O(n) and 2^(Omega (n^2 lg n)) for k = omega(n), and therefore showing that the construction is asymptotically optimal with respect to the ^(Theta(.)) notation.
  • omega-automata
  • Streett automata
  • complementation
  • lower bounds


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
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