[isabelle] New AFP entry: Unified Decision Procedures for Regular Expression Equivalence



Unified Decision Procedures for Regular Expression Equivalence
Tobias Nipkow, Dmitriy Traytel

We formalize a unified framework for verified decision procedures for regular
expression equivalence. Five recently published formalizations of such
decision procedures (three based on derivatives, two on marked regular
expressions) can be obtained as instances of the framework. We discover that
the two approaches based on marked regular expressions, which were previously
thought to be the same, are different, and one seems to produce uniformly
smaller automata.  The common framework makes it possible to compare the
performance of the different decision procedures in a meaningful way.

http://afp.sourceforge.net/entries/Regex_Equivalence.shtml
http://www.in.tum.de/~nipkow/pubs/regex_equiv.pdf

Enjoy!
Tobias and Dmitriy




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