模态μ演算片段递归方案模型检测的复杂性
计算机科学中的逻辑
2015-07-01 v2 编程语言
摘要
Ong已经证明，由n阶递归方案生成的可能无限有秩树的模态μ演算模型检测问题（等价于交替奇偶树自动机（APT）接受问题）是n-EXPTIME完全的。我们考虑APT的两个子类，并研究各自接受问题的复杂性。主要结果是：对于具有单一优先级的APT，该问题仍然是n-EXPTIME完全的；而对于具有析取转移函数的APT，该问题是(n-1)-EXPTIME完全的。这项研究受到Kobayashi近期工作的启发，该工作表明函数式程序的资源使用验证可以归约为递归方案的模型检测。作为一个应用，我们证明资源使用验证问题是(n-1)-EXPTIME完全的。
引用
@article{arxiv.1109.5267,
title = {Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus},
author = {Naoki Kobayashi and C. -H. Luke Ong},
journal= {arXiv preprint arXiv:1109.5267},
year = {2015}
}