Email Gateway (Aug 18 2022 at 12:56): Email Gateway (Aug 18 2022 at 12:56):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I'm looking for an Isabelle-formalization of nondeterministic finite
automata, that also generates executable code.
In particular, I need the following operations:
Membership query (directly on nondet. automata, without converting to
det. automata first)
Union, Intersection,
Substitution, in its general case, i.e. by a function :: \Sigma ->
\Gamma fsm
Especially the substitution operation seems tricky with the
Functional-Automata formalization in afp, because it stores no explicit
information about the alphabet.
Are there other formalizations of FSMs out there, from which I could start ?
Or can I extend the Functional-Automata in that direction ?
Regards, and thanks in advance for any suggestions
Peter
Email Gateway (Aug 18 2022 at 12:57):From: Tobias Nipkow <nipkow@in.tum.de>
Stefan Berghofer and Markus Reiter have developed a library of
executable constructions on automata. It is a bit specialized (the
alphabet are bit vectors) and does not have all your operations, but it
may be a good starting point.
Tobias
Peter Lammich wrote:
Last updated: May 03 2024 at 08:18 UTC