Formalizing Symbolic Decision Procedures for Regular Languages
Dmitriy Traytel · 2015
We study decision procedures for the equivalence of regular languages represented as regular expressions or logical formulas. Traditional algorithms in this context dispose of this symbolic representation by translating it into finite automata, which then are minimized and checked for structural equality. We develop concise algorithms that avoid this explicit translation by working with the symbolic structures directly. Our procedures are specified and proved correct in the proof assistant Isabelle.