Nos partenaires



Accueil du site > Français > Evénements > Séminaires > Séminaires IRIT-UPS

Séminaires IRIT-UPS



A Recursive Shortcut for CEGAR: Application to the Modal Logic K Satisfiability Problem

Jean-Marie LAGNIEZ - CRIL, Université d'Artois, Lens

Vendredi 23 Juin 2017, 14h30 - 16h00
UT3 Paul Sabatier, IRIT, Salle des Thèses
Version PDF :


Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking. Since then, it has been applied to many different problems. It is especially proved to be a highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both CEGAR and RECAR approaches for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered.