Minimal Proof Search for Modal Logic K Model Checking

DOI10.1007/978-3-642-33353-8_27MaRDI QIDQ2915084zbMATH OpenOpenAlexFDO

Authors Abdallah Saffidine

Publication date 21 September 2012

Published in Logics in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1207.1832

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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 Multi-agent Modal Logic K (MMLK) has important applications as a formal framework for perfect information multi-player games on its own. We present Minimal Proof Search (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.

Recommendations

• Artificial Intelligence and Symbolic Computation
• Proof Search and Counter Model of Positive Minimal Predicate Logic
• Complexity of model checking for logics over Kripke models
• Machine-checked proof-theory for propositional modal logics
• Computing minimal models modulo subset-simulation for modal logics
• Algebraic Methodology and Software Technology
• Implementing a relational theorem prover for modal logic K
• scientific article; zbMATH DE number 2086523
• Bounded Model Checking for Partial Kripke Structures
• Minimal Axiomatization in Modal Logic

Cites work

• scientific article; zbMATH DE number 1982201 (Why is no real title available?)
• scientific article; zbMATH DE number 2149447 (Why is no real title available?)
• scientific article; zbMATH DE number 2087624 (Why is no real title available?)
• Depth-first iterative-deepening: An optimal admissible tree search
• Modal logic
• Model checking propositional dynamic logic with all extras
• Multiagent Systems
• Proof-number search
• Tableau-based model checking in the propositional mu-calculus

Cited in

(2)

• Proof Search and Counter Model of Positive Minimal Predicate Logic
• Evaluating optimised decision procedures for propositional modal \({\mathbf K}_{({\mathbf m})}\) satisfiability

Describes a project that uses

Uses Software

• MCMAS

This page was built for publication: Minimal Proof Search for Modal Logic K Model Checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2915084)