Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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.
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.
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))$.
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$.
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}$.
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\} \}$
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)$.
