具有同步与完美回忆语义的认知\mu-演算的模型检测
计算机科学中的逻辑
2012-07-17 v4
摘要
我们证明了认知\mu-演算（epistemic \mu-calculus）某一片段的模型检测问题是可判定的。该片段允许在认知模态范围内以受限形式存在自由变量，从而避免了构建体现任何形式的公共知识的公式。我们的演算涵盖了已知的可判定认知 CTL/LTL 片段。其模态变体可以表达双人博弈中的获胜策略，其中一方具有不完美信息和不可观测目标；并且通过适当的编码，具有不完美信息和完美回忆的 ATL 模型检测问题的可判定实例，可以编码为该认知\mu-演算模型检测问题的实例。
引用
@article{arxiv.1204.2087,
title = {Model-checking an Epistemic \mu-calculus with Synchronous and Perfect Recall Semantics},
author = {Rodica Bozianu and Cătălin Dima and Constantin Enea},
journal= {arXiv preprint arXiv:1204.2087},
year = {2012}
}