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 metadatas

Cited literature [35 references]  Display  Hide  Download

https://hal.univ-cotedazur.fr/hal-02271413
Contributor : Valentin Montmirail <>
Submitted on : Monday, August 26, 2019 - 5:54:20 PM
Last modification on : Wednesday, August 28, 2019 - 1:23:31 AM

File

paper-07.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02271413, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

8

Files downloads

5