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
Type
Communication / ConférenceExternal document link
http://arxiv.org/abs/1207.1832v2Date
2012Conference title
13th European Conference on Logics in Artificial Intelligence, JELIA 2012Conference date
2012-09Conference city
ToulouseConference country
FranceBook title
Logics in Artificial Intelligence 13th European Conference, JELIA 2012, Toulouse, France, September 26-28, 2012, ProceedingsBook author
Farinas del Cerro, Luis; Herzig, Andreas; Mengin, JérômePublisher
Springer
Series title
Lecture Notes in Computer ScienceSeries number
7519Published in
Berlin
ISBN
978-3-642-33352-1
Number of pages
498Pages
346-358
Publication identifier
Metadata
Show full item recordAuthor(s)
Saffidine, AbdallahAbstract (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 / Keywords
Minimal Proof Search (MPS)Related items
Showing items related by title and author.
-
Saffidine, Abdallah; Cazenave, Tristan (2012) Communication / Conférence
-
Cazenave, Tristan; Jouandeau, Nicolas; Saffidine, Abdallah (2012) Communication / Conférence
-
Cazenave, Tristan; Saffidine, Abdallah (2011) Communication / Conférence
-
Saffidine, Abdallah; Cazenave, Tristan (2012) Communication / Conférence
-
Cazenave, Tristan; Saffidine, Abdallah; Schofield, Michael John; Thielscher, Michael (2016) Communication / Conférence