Paper Info
Title
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.
Year
DOI
Venue
2013
10.1145/2500365.2500612
Journal of Functional Programming
Keywords
Field
DocType
decision problem,decision procedure,mso formula,functional language,functional decision procedure,equivalence checker,verified decision procedure,regular expression,regular structure,regular expression equivalence,regular language,interactive theorem proving,regular expressions
Regular expression,Functional programming,Algebra,Computer science,Automated theorem proving,Algorithm,Decidability,Theoretical computer science,Equivalence (measure theory),Regular language,Pattern matching,Structural induction
Conference
Volume
Citations 
PageRank 
25
0
0.34
References 
Authors
23
2
Name
Order
Citations
PageRank
Dmitriy Traytel110122.55
Tobias Nipkow23056232.28