### 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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages
- Logic/General logic/Decidability of theories

### Related publications

- TRAYTEL, D., & NIPKOW, T. (2015). Verified decision procedures for MSO on words based on derivatives of regular expressions. Journal of Functional Programming, 25. https://doi.org/10.1017/s0956796815000246
- author's copy

### Session MSO_Regex_Equivalence

- List_More
- Pi_Regular_Set
- Pi_Regular_Exp
- Pi_Derivatives
- Pi_Regular_Operators
- Pi_Regular_Exp_Dual
- Pi_Equivalence_Checking
- Init_Normalization
- PNormalization
- Formula
- M2L
- M2L_Normalization
- M2L_Equivalence_Checking
- WS1S
- WS1S_Normalization
- WS1S_Equivalence_Checking
- M2L_Examples
- WS1S_Examples

### Depends on

- Deriving class instances for datatypes
- List Index

### Auto-related entries

- Unified Decision Procedures for Regular Expression Equivalence
- A Codatatype of Formal Languages
- The Myhill-Nerode Theorem Based on Regular Expressions

## Cite

×

MSO_Regex_Equivalence-AFP

    @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   = {June},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/MSO_Regex_Equivalence.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Jun 12, 2014 : Isabelle2013-2