A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem

A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem

Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 674-680. https://doi.org/10.24963/ijcai.2017/94

Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking large systems. Since then, it has been applied to many different problems. It especially proved to be an 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 a CEGAR and a RECAR approach 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.
Keywords:
Constraints and Satisfiability: Modeling/Formulation
Knowledge Representation, Reasoning, and Logic: Non-classical logics for Knowledge Representation
Constraints and Satisfiability: Satisfiability