Re: [isabelle] Automata library
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.
Peter Lammich wrote:
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)
Substitution, in its general case, i.e. by a function :: \Sigma ->
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and