模态逻辑 K 模型检测的最小证明搜索
人工智能
2012-07-11 v2 计算机科学中的逻辑
摘要
大多数模态逻辑（如 S5、LTL 或 ATL）都是模态逻辑 K 的扩展。虽然 LTL 的模型检测问题以及较小程度上的 ATL 模型检测问题是过去几十年非常活跃的研究领域，但更基础的多智能体模态逻辑 K（MMLK）的模型检测问题本身作为完美信息多人博弈的形式化框架具有重要应用。我们提出了最小证明搜索（MPS），这是一种基于努力数的算法，用于解决 MMLK 的模型检测问题。除了正确性之外，我们还证明了 MPS 的两个重要性质。MPS 所展示的（反）证明对于一般的成本定义具有最小成本，并且 MPS 是寻找最小成本（反）证明的最优算法。最优性意味着任何可比的算法要么需要探索比 MPS 更大或相等的状态空间，要么无法保证在每个输入上都能找到最小成本的（反）证明。因此，我们的工作与启发式搜索中的 A* 和 AO*、双人博弈中的证明数搜索（Proof Number Search）和 DFPN+ 以及软件模型检测中的反例最小化相关。
引用
@article{arxiv.1207.1832,
title = {Minimal Proof Search for Modal Logic K Model Checking},
author = {Abdallah Saffidine},
journal= {arXiv preprint arXiv:1207.1832},
year = {2012}
}
备注
Extended version of the JELIA 2012 paper with the same title