Nos partenaires

CNRS

Rechercher





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

Séminaires

 

L’IRIT étant localisé sur plusieurs sites, ses séminaires sont organisés et ont lieu soit à l’Université Toulouse 3 Paul Sabatier (UT3), l’Université Toulouse 1 Capitole (UT1), l’INP-ENSEEIHT ou l’Université Toulouse 2 Jean Jaurès (UT2J).

 

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 :

Abstract

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.

 

Retour