PhD defense of Valentin Montmirail - Practical resolution of satisfiability testing for modal logics
September 17th, 2018, 10 AM, salle des thèses de la faculté Jean Perrin
In this thesis, we explored the idea to use modern SAT technology that has seen considerable progress over the last years for solving various kinds of Modal Logics. We tackled the problem from various directions. For the NP-complete variants of Modal Logics it is a natural choice to encode them to SAT and use a SAT solver to decide them. In order to get an efficient Modal Logic solver, it requires several optimisations because otherwise the formulas will get too huge.
In the next step, we asked the question how to obtain smallest models when the considered formula is satisfiable and we came up with several solutions but we did not stop our work with the NP-complete logics.
For going beyond NP, we suggested a novel approach inspired by the successful CEGAR techniques that we named RECAR for Recursive Explore and Check Abstraction Refinement. We instantiated the framework RECAR within the solver MoSaiC and we demonstrated how, with efficient over- and under- abstractions, a SAT-based approach can solve PSPACE modal logics.