# Non-deterministic Büchi vs Rabin: Automaton size for LTL->automaton

Is there any general result to show that which automaton is more succinct? I have a set of LTL properties and I would like to know (show) which automaton is more efficient in term of state number and edge number.

• Can you expand the main body of your question to make it independent of the title? Try to be more elaborate. Mar 17 '17 at 11:35
• Have you checked any small examples? Mar 17 '17 at 14:05
• @MichaelKlein Yes, Actually Buchi was way better in my examples but I just wanted to know if it is a general argument or not. Mar 17 '17 at 14:27
• From a discussion with one of my friends for state numbers: "the rule of thumb is determinism costs 2EXP, nondeterminism costs EXP". So can we just recon that Rabin automaton, because it is deterministic, needs more states? Mar 21 '17 at 13:56

Consider a nondeterministic Büchi automaton $$\mathcal{A} = \langle \Sigma, Q, q_0, \delta, \alpha\rangle$$. The acceptance condition of $$\mathcal{A}$$ is a subset of states $$\alpha\subseteq Q$$, and an infinite run $$r = q_0, q_1, q_2, \ldots$$ over an infinite word $$\sigma_1\sigma_2\cdots$$ is accepting iff $$r$$ visits a state in $$\alpha$$ infinitely many times.
In Rabin automata, the acceptance condition is given by $$\alpha = \{\langle \alpha_1, \beta_1 \rangle, \langle \alpha_2, \beta_2 \rangle, \ldots , \langle \alpha_k, \beta_k \rangle \}$$, where $$\alpha_i, \beta_i\subseteq Q$$, for all $$i\in [k]$$. An infinite run $$r = q_0, q_1, q_2, \ldots$$ over an infinite word $$\sigma_1\sigma_2\cdots$$ is accepting iff for some $$i\in [k]$$, $$r$$ visits a state in $$\alpha_i$$ infinitely many times, and visits the states in $$\beta_i$$ finitely many times. The number $$k$$ is the index of the automaton, and is usually taken into account when defining the automaton's size.
Clearly, a Büchi condition $$\alpha$$ is equivalent to the Rabin condition $$\{ \langle \alpha, \emptyset \rangle\}$$. Thus, nondeterministic Büchi automata can be translated to nondeterministic Rabin automata with no blowup (they can be thought of as a simple fragment of Rabin automata - although they are equally expressive). So, nondeterministic Büchi automata cannot be more succinct than nondeterministic Rabin automata. However, a nondeterministic Rabin automaton with $$n$$ states, $$m$$ transitions, and index $$k$$, can be translated to a nondeterministic Büchi automaton with $$O(n\cdot k)$$ states, and $$O(k\cdot m)$$ transitions. The later translation is justified by a lower bound. So, nondeterministic Rabin automata are polynomially more succinct than nondeterministic Büchi automata, which is not significant.
Note that you can easily translate an LTL formula into a nondeterministic Büchi automaton (see section 6 here), and the translation has a tight exponential bound. However, following your comment, if you're interested in translating the LTL-formula into a deterministic automaton, then you can translate the Büchi automaton to a deterministic Rabin automaton (such determinization construction has a tight bound of $$2^{\Theta(n \log n)}$$). Also, the double exponential blow-up of translating LTL formulas to deterministic automata cannot be avoided (see theorem 26 here).