I am trying to demonstrate the following idea without success.
There are infinitely many $n \in \mathbb{N}$ such that: There is a non-deterministic Buchi automata of size $n$ such that a deterministic Rabin Automata accepting the same language has at least $n!$ states.
Any help would be appreciated
This is Theorem 1.30 in the chapter "Omega-Automata" in the book "Automata, Logics, and Infinite Games: A Guide to Current Research" edited by Erich Grädel, Wolfgang Thomas and Thomas Wilke. They have a proof as well (and a literature referene to the original publication).
Note that instead of the nondeterminstic Buchi automaton having $n$ states, it needs to have $O(n)$ states to make the proof work. The problem is then defined slightly differently to make this precise.
Note that it is a bit confusing if you write "Buchi automata" and "deterministic Rabin automata" in the same question if the former are meant to be "nondeterministic Buchi automata". There is ample work both on deterministic and non-deterministic Buchi automata, so spelling out which variant is meant is important.
Usually, when defining the size of a Rabin automaton, we take into consideration the automaton's index (the number of Rabin pairs) and not only the number of states. What you asked for is well-known, and here are the known lower bounds of the $NBW \to DRW$ translation. Where $NBWs$ is an abbreviation for nondeterministic Buchi word automata, and $DRWs$ is for deterministic Rabin word automata.
In 1988 Max Michel showed a lower bound of $2^{\Omega(nlogn)}$ states and index in $O(n)$. Then, later in 1999 Christof Löding extended the result, and showed that there is no equivalent DRW with less than $2^{\Omega(nlogn)}$ states regardless of the index. Finally, in 2009, Thomas Colcombet and Konard Zdanowski, gave a tight lower bound of $\Omega((1.64n)^n)$, for a large alphabet.
Are you sure you didn't get them mixed up?
It seems like for any Buchi automaton with accepting states F, we can build the equivalent Rabin automaton with accepting conditions $\Omega = \{(\{\}, F)\}$ that accepts the same language.
(I.e., any infinite sequence $\rho$ has to intersect some state in $F$ infinitely often and has no restrictions on what states it can't hit infinitely often.)
I'm using the acceptance condition here https://en.wikipedia.org/wiki/Ω-automaton#Acceptance_conditions. Was there a different formulation you had in mind?
