2026-07-21T19:27:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3347 2024-03-06T10:34:06Z ddc:004 open_access

A Tight Lower Bound for Streett Complementation Cai, Yang Zhang, Ting omega-automata Streett automata complementation lower bounds 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yang Cai and Ting Zhang 2011 Is Part Of LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2011.339 urn:nbn:de:0030-drops-33474 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.339 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode