### Abstract

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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Related publications

- Bojańczyk, M., Klin, B., & Lasota, S. (2014). Automata theory in nominal sets. Logical Methods in Computer Science, Volume 10, Issue 3. https://doi.org/10.2168/lmcs-10(3:4)2014

### Session Nominal_Myhill_Nerode

- Nominal_Myhill_Nerode

## Cite

×

Nominal_Myhill_Nerode-AFP

    @article{Nominal_Myhill_Nerode-AFP,
      author  = {Cárolos Laméris},
      title   = {Myhill-Nerode Theorem for Nominal G-Automata},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Nominal_Myhill_Nerode.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest