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.

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^{*}

, the following are equivalent:

The set of equivalence classes of $L / \equiv_{MN}$ , with respect to the Myhill-Nerode equivalence relation, $\equiv_{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