Myhill-Nerode Theorem for Nominal G-Automata

This work formalizes the Myhill-Nerode theorems for \(G\)-automata and nominal \(G\)-automata. The Myhill-Nerode theorem for (nominal) \(G\)-automata states that, given \(A\) an orbit finite (nominal) \(G\)-set and a \(G\)-language \(L \subseteq A^{\ast}\), the following are equivalent:

• The set of equivalence classes of \(L{/}\equiv_{\text{MN}}\), with respect to the Myhill-Nerode equivalence relation, \(\equiv_{\text{MN}}\), is orbit finite.
• \(L\) is recognized by a deterministic (nominal) \(G\)-automaton with an orbit finite set of states.

The proofs formalized are based on on those from an article by M. Bojanczyk, B. Klin and S. Lasota.