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

Question

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.

Answer 1

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.

A comprehensive overview of the translations can be found here (along with other relevant references).

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).