2026-07-25T12:24:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3226 2024-03-06T10:33:58Z ddc:004 open_access

Tight Upper Bounds for Streett and Parity Complementation Cai, Yang Zhang, Ting Streett automata omega-automata parity automata complementation upper bounds Complementation of finite automata on infinite words is not only a fundamental problem in automata theory, but also serves as a cornerstone for solving numerous decision problems in mathematical logic, model-checking, program analysis and verification. For Streett complementation, a significant gap exists between the current lower bound 2^{Omega(n*log(n*k))} and upper bound 2^{O(n*k*log(n*k))}, where n is the state size, k is the number of Streett pairs, and k can be as large as 2^{n}. Determining the complexity of Streett complementation has been an open question since the late 80's. In this paper we show a complementation construction with upper bound 2^{O(n*log(n)+n*k*log(k))} for k=O(n) and 2^{O(n^{2}*log(n))} for k=Omega(n), which matches well the lower bound obtained in the paper arXiv:1102.2963. We also obtain a tight upper bound 2^{O(n*log(n))} for parity complementation. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yang Cai and Ting Zhang 2011 Is Part Of LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2011.112 urn:nbn:de:0030-drops-32269 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.112 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode