### Abstract

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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Related publications

- Nipkow, T., & Traytel, D. (2014). Unified Decision Procedures for Regular Expression Equivalence. Lecture Notes in Computer Science, 450–466. https://doi.org/10.1007/978-3-319-08970-6_29
- author's copy

### Session Regex_Equivalence

- Automaton
- Derivatives_Finite
- Deriv_PDeriv
- Deriv_Autos
- Position_Autos
- After2
- Before2
- Regex_Equivalence
- Examples
- Benchmark

### Depends on

- Efficient Mergesort
- Regular Sets and Expressions
- SpecCheck - Specification-Based Testing for Isabelle/ML

### Auto-related entries

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

## Cite

×

Regex_Equivalence-AFP

    @article{Regex_Equivalence-AFP,
      author  = {Tobias Nipkow and Dmitriy Traytel},
      title   = {Unified Decision Procedures for Regular Expression Equivalence},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/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
- Nov 30, 2014 : Isabelle2014
- Aug 28, 2014 : Isabelle2014
- Jan 30, 2014 : Isabelle2013-2