This thesis studies decision procedures for the equivalence of regular languages
represented 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 efficiently
minimized and checked for structural equality.
We develop procedures that avoid this explicit translation by working with the
symbolic structures directly. This results in concise functional algorithms that are
easy to reason about, even formally. Indeed, the presented decision procedures are
specified 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 derivatives
and their cousins. For formulas, the development of such operations is the main
theoretical contribution of this thesis.
The main technical contribution is the formalization of a uniform framework for
deciding equivalence of regular languages and the instantiation of this framework
by 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 logic
on finite words under two different existing semantics (WS1S and M2L(Str)).