[Club2] talk by Dmitriy Traytel, Wed. 27, 13:00, Turing

[Andrei Popescu]

Dear All,  
Next week, Dmitriy will give a talk on his formalization of monadic second-order logic. Please note the unusual hour---13 instead of 14.  
Best regards,   Andrei 
Dmitriy TraytelA Verified Decision Procedure for MSO on Words Based on Derivatives of Regular Expressions==========================================================================================Wed. March. 27, 13:00, Room 00.09.055 ("Alan Turing") 
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130320/7d12f4fa/attachment.html>