Formalizing Symbolic Decision Procedures for Regular Languages
Research output: Book/Report › Doctoral thesis › Research
Standard
Formalizing Symbolic Decision Procedures for Regular Languages. / Traytel, Dmitriy.
Technische Universität München , 2015. 132 p.Research output: Book/Report › Doctoral thesis › Research
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - THES
T1 - Formalizing Symbolic Decision Procedures for Regular Languages
AU - Traytel, Dmitriy
PY - 2015/10/15
Y1 - 2015/10/15
N2 - This thesis studies decision procedures for the equivalence of regular languagesrepresented symbolically as regular expressions or logical formulas.Traditional decision procedures in this context rush to dispose of the concise symbolic representation by translating it into finite automata, which then are efficientlyminimized and checked for structural equality.We develop procedures that avoid this explicit translation by working with thesymbolic structures directly. This results in concise functional algorithms that areeasy to reason about, even formally. Indeed, the presented decision procedures arespecified and proved correct in the proof assistant Isabelle.The core idea, shared by all procedures under consideration, is the usage of a symbolic derivative operation that replaces the global transition table of the automaton.For regular expressions those are the increasingly popular Brzozowski derivativesand their cousins. For formulas, the development of such operations is the maintheoretical contribution of this thesis.The main technical contribution is the formalization of a uniform framework fordeciding equivalence of regular languages and the instantiation of this frameworkby various symbolic representations. Overall, this yields formally verified executable decision procedures for the equivalence of various kinds of regular expressions, Presburger arithmetic formulas, and formulas of monadic second-order logicon finite words under two different existing semantics (WS1S and M2L(Str)).
AB - This thesis studies decision procedures for the equivalence of regular languagesrepresented symbolically as regular expressions or logical formulas.Traditional decision procedures in this context rush to dispose of the concise symbolic representation by translating it into finite automata, which then are efficientlyminimized and checked for structural equality.We develop procedures that avoid this explicit translation by working with thesymbolic structures directly. This results in concise functional algorithms that areeasy to reason about, even formally. Indeed, the presented decision procedures arespecified and proved correct in the proof assistant Isabelle.The core idea, shared by all procedures under consideration, is the usage of a symbolic derivative operation that replaces the global transition table of the automaton.For regular expressions those are the increasingly popular Brzozowski derivativesand their cousins. For formulas, the development of such operations is the maintheoretical contribution of this thesis.The main technical contribution is the formalization of a uniform framework fordeciding equivalence of regular languages and the instantiation of this frameworkby various symbolic representations. Overall, this yields formally verified executable decision procedures for the equivalence of various kinds of regular expressions, Presburger arithmetic formulas, and formulas of monadic second-order logicon finite words under two different existing semantics (WS1S and M2L(Str)).
M3 - Doctoral thesis
BT - Formalizing Symbolic Decision Procedures for Regular Languages
PB - Technische Universität München
ER -
ID: 245668394