Email Gateway (Nov 23 2023 at 14:56): Email Gateway (Nov 23 2023 at 14:56):From: Tobias Nipkow <nipkow@in.tum.de>
Myhill-Nerode Theorem for Nominal G-Automata
Cárolos Laméris
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 subset A^*, the
following are equivalent:
The set of equivalence classes of L/==, with respect to the Myhill-Nerode
equivalence relation ==, 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.
https://www.isa-afp.org/entries/Nominal_Myhill_Nerode.html
Enjoy!
Last updated: Jan 04 2025 at 20:18 UTC