A note on omega automata

$\omega$-automata are finite state automata interpreted on infinite words. Non-deterministic $\omega$-automata are quintuples $(Q,\Sigma,I,T,\mathcal F)$, where $Q$ is a finite set of states, $I$ is a non-empty set of initial states, $T:Q\times\Sigma\times Q\to Q$ is a transition relation, and $\mathcal F$ is an acceptance condition.
The Rabin condition is in form of $\mathcal F=\{(A_i,R_i):i\in J\}$, and run is accepting iff there exists $j\in J$ such that it visits $A_j$ i.o. but visits $R_i$ only finitely many times.
The Streett condition is $\mathcal F=\{(A_i,R_i):i\in J\}$ such that a run is accepting iff there exists $j\in J$ such that it visits $A_j$ i.o. or visits $R_i$ only finitely many times.
The parity automata are $\omega$-automata with a priority function $p:Q\to [c]$ for some $c\in\mathbb N.$ A run $\pi$ is accepting iff $\lim\sup p(\pi(n))$ is even. Parity automata can be simulated by $\omega$-automata with the Rabin acceptance conditions: just define $J:=\mathbb N$, $A_n:={s\in S: p(s)\le 2n\}$, and $R_n:={s\in S: p(s)\le 2n-1\}$.


Parity Automata.