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 -