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:
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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.