Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

 

Title: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Authors: Dmitriy Traytel (traytel /at/ inf /dot/ ethz /dot/ ch) and Tobias Nipkow
Submission date: 2014-06-12
Abstract: 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.
BibTeX: 
@article{MSO_Regex_Equivalence-AFP,
  author  = {Dmitriy Traytel and Tobias Nipkow},
  title   = {Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/MSO_Regex_Equivalence.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Deriving, List-Index
Status: [skipped] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document
Browse theories
Download this entry
Older releases: