# Language equivalent states in a deterministic parity automaton

Given a deterministic parity automaton $\mathcal{A}$ with state set $Q$ and a state $q \in Q$, we denote with $\mathcal{A}_q$ the same automaton with initial state $q$. Two states $p$ and $q$ are language equivalent if $L(\mathcal{A}_p) = L(\mathcal{A}_q)$.

What is an efficient algorithm to compute the set of all language equivalent pairs, i.e. $\{ (p, q) \in Q \times Q \mid L(\mathcal{A}_p) = L(\mathcal{A}_q) \}$ ?

Two states in the automaton have different languages if and only if there exists a word that is accepted from one state, but not from the other. Checking if this is the case boils down to building a product of the automaton with itself, i.e., starting form the automaton $\mathcal{A'} = (Q, \Sigma, \delta, q_0, \mathcal{F})$, you build an automaton $\mathcal{A'} = (Q \times Q, \Sigma, \delta', (q_0,q_0), \mathcal{F}')$ such that for all $q,q' \in Q$, you have $\delta'((q,q'),a) = (\delta(q,a),\delta(q',a))$.

In this product automaton, you want to cycles along which the parity of the highest color visited infinitely often in the first factor of $Q \times Q$ is not the same as in the second copy. Whenever this is the case, then for every state $(q,q')$, we know that $q$ and $q'$ have different languages. Otherwise, if from state $(q,q')$, there is no way to reach a cycle along which one copy of the automaton accepts, but the other one does not, you know that the states have the same languages.

The technique is applied in the paper "SAT-Based Minimization of Deterministic ω-Automata" by Souheib Baarir and Alexandre Duret-Lutz, which bases on a similar construction for deterministic Buchi automata from earlier work. They use a SAT solver to guess an automaton that is equivalent to a given one and add SAT clauses that enforce that in a product between the two automata, you do not have reachable cycles along which the acceptance of the cycle differs between the copies. After an equivalent automaton is fixed, their clauses become Horn clauses, so you can check this in polynomial time. In your case, you would just use the same automaton again.

• This idea came to my mind as well but I discarded it because checking all loops "by hand" can have exponential runtime. I will have a look at that paper and see if that approach works better. Thank you. Sep 5 '18 at 8:07
• Andreas, you don't have to check all the loops seperately, and that's the trick. Think of it as follows, you build a graph with vertices $(q_1,q_2,q'_1,q'_2,c,c')$, where the reachability of a vertex from another vertex $(q_1,q_2,q_1,q_2,0,0)$ represents that for some word w, you can reach q_2 from q_1 under w and q'_2 from q'_1 under w while the maximum color seen along the way is c and c', respectively. Then, you only have to search for paths from $(q_1,q_2,q_1,q_2,0,0)$ to $(q_1,q_2,q_1,q_2,c,c')$ with differently-paritied c and c'. Then, all you do are simple graph searches. Sep 5 '18 at 8:27
• In the Duret-Lutz paper, they use this idea for full omega-regular automata, while a Buchi-only version of it appeared in earlier work. Sep 5 '18 at 8:28
• If I understand correctly, the complexity is quartic in the number of states? That is certainly better than an exponential runtime but not what I would consider efficient, as it becomes unfeasible for automata of size at least 100. Sep 5 '18 at 12:41
• @AndreasT Yes, your intuition is correct (and you need to add an additional factor that is quadratic in the number of colors). Note that in automata theory, pretty much all constructions are computationally expensive. Yet, they can be used for many languages of practical relevance since you can do a couple of optimizations. Tools such as "Rabinizer" solve doubly-exponential problems. It's the same here - while the worst case size for the graph is quite large, you can probably come up with a few tricky so that the approach does not scale so bad in practice. Sep 6 '18 at 7:41

DCTLib provided a reasonable answer, though it has complexity $$n^4 k^2$$, which is unsuited for my purpose of use. Another algorithm was proposed to me.

1. From $$\mathcal{A}$$ with state set $$Q$$ and parity function $$c : Q \rightarrow \mathbb{N}$$ (I use min even acceptance), build a labelled $$\mathcal{B}$$ with state set $$Q \times Q$$ and state labels $$d : (p, q) \mapsto (c(p), c(q))$$.

2. Let the parity colors that are used by $$\mathcal{A}$$ be $$0, \dots, k$$ (if $$0$$ doesn't occur, slight adaptions have to be made). For every $$i, j \in \{0, \dots, k\}$$, build $$\mathcal{B}_{i,j}$$, which is constructed from $$\mathcal{B}$$ by removing all state pairs whose first label component is less than $$i$$ or whose second label component is less than $$j$$.

3. Collect lists $$S_{i,j} \subseteq 2^{Q \times Q}$$ that contain all strongly connected components of $$\mathcal{B}_{i,j}$$ and a list $$S = \bigcup_{i,j} S_{i,j}$$.

4. Remove from $$S$$ all those SCCs $$s \subseteq Q \times Q$$ in which the lowest parity of the two components differs, i.e. $$\min \{ x \mid \exists p \in s: d(p) \in \{x\} \times \mathbb{N} \} \not\equiv_{\mod 2} \min \{ y \mid \exists p \in s: d(p) \in \mathbb{N} \times \{y\} \}$$

5. For any two states $$p, q \in Q$$, those states are not language equivalent iff there is a pair $$(p', q') \in \bigcup S$$ that is reachable from $$(p, q)$$ in $$\mathcal{B}$$.

As soon as the automata $$\mathcal{B}_{i,j}$$ are built, there are only algorithms of linear run time applied, so in total this allows us to compute the language equivalence in $$\mathcal{O}(n^2 k^2)$$.