Myhill-Nerode Theorem for Nominal G-Automata

Cárolos Laméris 📧

November 10, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Related publications

  • Bojańczyk, M., Klin, B., & Lasota, S. (2014). Automata theory in nominal sets. Logical Methods in Computer Science, Volume 10, Issue 3.

Session Nominal_Myhill_Nerode