principleMinor
Non-deterministic Büchi vs Rabin: Automaton size for LTL->automaton
Viewed 0 times
rabinnonltlsizebüchideterministicforautomaton
Problem
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.
Solution
Consider a nondeterministic Büchi automaton $A = \langle \Sigma, Q, q_0, \delta, \alpha\rangle$. The acceptance condition of $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).
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).
Context
StackExchange Computer Science Q#71652, answer score: 3
Revisions (0)
No revisions yet.