Skip to Main content Skip to Navigation
Conference papers

On Checking Kripke Models for Modal Logic K

Abstract : This article presents our work toward a rigorous experimental comparison of state-of-the-art solvers for the resolution of the satisfiability of formulae in modal logic K. Our aim is to provide a pragmatic way to verify the answers provided by those solvers. For this purpose, we propose a certificate format and a checker to validate Kripke models for modal logic K. We present some experimental results using efficient solvers modified to incorporate this verification step. We have been able to validate at least one certificate for 67 percent of the satisfi-able problems, which provides a set of benchmark with independently checked solution which can be used to validate new solvers. We discuss the limits of our approach in the last part of this article.
Document type :
Conference papers
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Valentin Montmirail <>
Submitted on : Monday, August 26, 2019 - 5:54:20 PM
Last modification on : Wednesday, August 28, 2019 - 1:23:31 AM
Long-term archiving on: : Friday, January 10, 2020 - 4:28:34 AM


Files produced by the author(s)


  • HAL Id : hal-02271413, version 1



Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail. On Checking Kripke Models for Modal Logic K. Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, July 2nd, 2016., Jul 2016, Coimbra, Portugal. ⟨hal-02271413⟩



Record views


Files downloads