[isabelle-dev] Fwd: [isabelle] New AFP entry: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

[Dmitriy Traytel]

I'm following the suggestion of announcing who will fix a new AFP entry 
for the development version.

Of course, I will take care of MSO_Regex_Equivalence once it is merged 
into the development branch. The patch is actually already prepared.

Dmitriy


-------- Original-Nachricht --------
Betreff: 	[isabelle] New AFP entry: Decision Procedures for MSO on Words 
Based on Derivatives of Regular Expressions
Datum: 	Thu, 12 Jun 2014 22:35:58 +0200
Von: 	Tobias Nipkow <nipkow at in.tum.de>
An: 	Isabelle Users <isabelle-users at cl.cam.ac.uk>



Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Dmitriy Traytel and Tobias Nipkow

Monadic second-order logic on finite words (MSO) is a decidable yet expressive
logic into which many decision problems can be encoded. Since MSO formulas
correspond to regular languages, equivalence of MSO formulas can be reduced to
the equivalence of some regular structures (e.g. automata). We verify an
executable decision procedure for MSO formulas that is not based on automata but
on regular expressions.

Decision procedures for regular expression equivalence have been formalized
before, usually based on Brzozowski derivatives. Yet, for a straightforward
embedding of MSO formulas into regular expressions an extension of regular
expressions with a projection operation is required. We prove total correctness
and completeness of an equivalence checker for regular expressions extended in
that way. We also define a language-preserving translation of formulas into
regular expressions with respect to two different semantics of MSO.

The formalization is described in this ICFP 2013 functional pearl:
http://www21.in.tum.de/~nipkow/pubs/icfp13.html

http://afp.sourceforge.net/entries/MSO_Regex_Equivalence.shtml

Enjoy!



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140613/e9cb9bba/attachment.html>