Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Unified Decision Procedures for...


view this post on Zulip 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: Mar 28 2024 at 12:29 UTC