Unified Decision Procedures for Regular Expression Equivalence

Tobias Nipkow; Dmitriy Traytel

doi:10.1007/978-3-319-08970-6_29

Unified Decision Procedures for Regular Expression Equivalence

Tobias Nipkow, Dmitriy Traytel

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

19 Citationer (Scopus)

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 we prove a quotient relation between the automata produced by them. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way.

Originalsprog	Engelsk
Titel	ITP 2014 - Interactive Theorem Proving : 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings
Redaktører	Gerwin Klein, Ruben Gamboa
Antal sider	17
Vol/bind	8558
Forlag	Springer, Cham
Publikationsdato	2014
Sider	450-466
DOI	https://doi.org/10.1007/978-3-319-08970-6_29
Status	Udgivet - 2014
Udgivet eksternt	Ja

Navn	LNCS

Adgang til dokumentet

10.1007/978-3-319-08970-6_29

Citationsformater

Nipkow, T., & Traytel, D. (2014). Unified Decision Procedures for Regular Expression Equivalence. I G. Klein, & R. Gamboa (red.), ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings (Bind 8558, s. 450-466). Springer, Cham. https://doi.org/10.1007/978-3-319-08970-6_29

Unified Decision Procedures for Regular Expression Equivalence. / Nipkow, Tobias; Traytel, Dmitriy.
ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. red. / Gerwin Klein; Ruben Gamboa. Bind 8558 Springer, Cham, 2014. s. 450-466 (LNCS).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Nipkow, T & Traytel, D 2014, Unified Decision Procedures for Regular Expression Equivalence. i G Klein & R Gamboa (red), ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. bind 8558, Springer, Cham, LNCS, s. 450-466. https://doi.org/10.1007/978-3-319-08970-6_29

Nipkow T, Traytel D. Unified Decision Procedures for Regular Expression Equivalence. I Klein G, Gamboa R, red., ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. Bind 8558. Springer, Cham. 2014. s. 450-466. (LNCS). doi: 10.1007/978-3-319-08970-6_29

Nipkow, Tobias ; Traytel, Dmitriy. / Unified Decision Procedures for Regular Expression Equivalence. ITP 2014 - Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings. red. / Gerwin Klein ; Ruben Gamboa. Bind 8558 Springer, Cham, 2014. s. 450-466 (LNCS).

@inproceedings{9e5d7ac741dd47fd9868443cbcd57cb5,

title = "Unified Decision Procedures for Regular Expression Equivalence",

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 we prove a quotient relation between the automata produced by them. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way.",

author = "Tobias Nipkow and Dmitriy Traytel",

year = "2014",

doi = "10.1007/978-3-319-08970-6_29",

language = "English",

volume = "8558",

series = "LNCS",

pages = "450--466",

editor = "Gerwin Klein and Ruben Gamboa",

booktitle = "ITP 2014 - Interactive Theorem Proving",

publisher = "Springer, Cham",

}

TY - GEN

T1 - Unified Decision Procedures for Regular Expression Equivalence

AU - Nipkow, Tobias

AU - Traytel, Dmitriy

PY - 2014

Y1 - 2014

N2 - 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 we prove a quotient relation between the automata produced by them. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way.

AB - 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 we prove a quotient relation between the automata produced by them. The common framework makes it possible to compare the performance of the different decision procedures in a meaningful way.

U2 - 10.1007/978-3-319-08970-6_29

DO - 10.1007/978-3-319-08970-6_29

M3 - Article in proceedings

VL - 8558

T3 - LNCS

SP - 450

EP - 466

BT - ITP 2014 - Interactive Theorem Proving

A2 - Klein, Gerwin

A2 - Gamboa, Ruben

PB - Springer, Cham

ER -