具有同步与完美回忆语义的认知$\mu$-演算的模型检测
计算机科学与博弈论
2013-10-28 v1 计算机科学中的逻辑
摘要
我们确定了认知-演算模型检测问题的一个可判定子问题。该子问题实例中的公式允许在认知模态算子的作用域内以受限形式出现自由变量,从而避免了体现任何形式的公共知识。我们的子问题涵盖了已知的认知 CTL/LTL 的可判定片段,可以表达一方具有不完美信息且目标不可观测的双人博弈中的获胜策略,并且通过适当的编码,还可涵盖 ATLiR 模型检测问题的可判定实例。
关键词
引用
@article{arxiv.1310.6434,
title = {Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics},
author = {Rodica Bozianu and Catalin Dima and Constantin Enea},
journal= {arXiv preprint arXiv:1310.6434},
year = {2013}
}
备注
10 pages, Poster presentation at TARK 2013 (arXiv:1310.6382) http://www.tark.org