Print this Page


Links' Seminars and Public Events Add to google calendar
Tue, June 6, 2017
to Fri, June 9, 2017
 all day
Add event to google

Fri, June 9, 2017
10:30 am
12:30 pm
Add event to google
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.
"Lille-Salle B21"

Permanent link to this article: