Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Dmitriy Traytel, Tobias Nipkow · 2014
Monadic second-order logic on finite words (MSO) is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced to the equivalence of some regular struc-tures (e.g. automata). We verify an executable decision procedure for MSO formulas that is not based on automata but on regular expres-sions. Decision procedures for regular expression equivalence have been formalized before (e.g. in Isabelle/HOL [1]), usually based on Brzo-zowski derivatives. Yet, for a straightforward embedding of MSO for-mulas into regular expressions an extension of regular expressions with a projection operation is required. We prove total correctness and com-pleteness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formu-