A Verified Decision Procedure for MSO on Words Based on Derivatives of Regular Expressions
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). However, formal verification of automata is a
difficult task. Instead, the recursive data structure of regular
expressions simplifies the formalization, notably by offering a
structural induction principle.
Decision procedures of 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 semantics-preserving translation of MSO formulas into
regular expressions. Our results have been formalized and verified in
the theorem prover Isabelle. Using Isabelle's code generation
facility, this yields a formally verified algorithm that decides
equivalence of MSO formulas.
pdf
@inproceedings{TraytelN-ICFP2013,author={Dmitriy Traytel and Tobias Nipkow},
title={A Verified Decision Procedure for MSO on Words Based on Derivatives of Regular Expressions},
booktitle={Proc.\ ACM SIGPLAN International Conference on Functional Programming (ICFP 2013)},
pages={3-12},year=2013}
This conference paper has been superseded by an extended
journal version.