Email Gateway (Aug 19 2022 at 13:25): Email Gateway (Aug 19 2022 at 13:25):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC