Minimal Proof Search for Modal Logic K Model Checking
Saffidine, Abdallah (2012), Minimal Proof Search for Modal Logic K Model Checking, in Farinas del Cerro, Luis; Herzig, Andreas; Mengin, Jérôme, Logics in Artificial Intelligence 13th European Conference, JELIA 2012, Toulouse, France, September 26-28, 2012, Proceedings, Springer : Berlin, p. 346-358. http://dx.doi.org/10.1007/978-3-642-33353-8_27
TypeCommunication / Conférence
External document linkhttp://arxiv.org/abs/1207.1832v2
Conference title13th European Conference on Logics in Artificial Intelligence, JELIA 2012
Book titleLogics in Artificial Intelligence 13th European Conference, JELIA 2012, Toulouse, France, September 26-28, 2012, Proceedings
Book authorFarinas del Cerro, Luis; Herzig, Andreas; Mengin, Jérôme
Series titleLecture Notes in Computer Science
Number of pages498
MetadataShow full item record
Abstract (EN)Most modal logics such as S5, LTL, or ATL are extensions of Modal Logic K. While the model checking problems for LTL and to a lesser extent ATL have been very active research areas for the past decades, the model checking problem for the more basic MMLK has important applications as a formal framework for perfect information multi-player games on its own. We present MPS, an effort number based algorithm solving the model checking problem for MMLK. We prove two important properties for MPS beyond its correctness. The (dis)proof exhibited by MPS is of minimal cost for a general definition of cost, and MPS is an optimal algorithm for finding (dis)proofs of minimal cost. Optimality means that any comparable algorithm either needs to explore a bigger or equal state space than MPS, or is not guaranteed to find a (dis)proof of minimal cost on every input. As such, our work relates to A* and AO* in heuristic search, to Proof Number Search and DFPN+ in two-player games, and to counterexample minimization in software model checking.
Subjects / KeywordsMinimal Proof Search (MPS)
Showing items related by title and author.