## Verified Decision Procedures for MSO on Words Based on Derivatives of
Regular Expressions

#### Abstract

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 structures (e.g. automata). This paper
presents a verified functional decision procedure for MSO formulas that is not
based on automata but on regular expressions. Functional languages are ideally
suited for this task: regular expressions are data types and functions on them
are defined by pattern matching and recursion and are verified by structural
induction.

Decision procedures for regular expression equivalence have been formalized
before, usually based on Brzozowski derivatives. Yet, for a straightforward
embedding of MSO formulas into regular expressions an extension of regular
expressions with a projection operation is required. We prove total
correctness and completeness of an equivalence checker for regular expressions
extended in that way. We also define a language-preserving translation of
formulas into regular expressions with respect to two different semantics of
MSO. Our results have been formalized and verified in the theorem prover
Isabelle. Using Isabelle's code generation facility, this yields purely
functional, formally verified programs that decide equivalence of MSO
formulas.

*Keywords:* MSO, WS1S, decision procedure, regular expressions,
Brzozowski derivatives, interactive theorem proving, Isabelle

Article draft