线性μ-演算交换深度的可判定性及其复杂度

摘要：

模态μ-演算被十分广泛地应用在模型验证技术中.影响模态μ-演算检验复杂度的主要瓶颈来源于规约公式的交换深度.讨论了线性μ-演算交换深度的可判定性以及求解复杂度.证明了线性μ-演算交换深度是可判定的；同时证明了对于长为l的公式判定及求解的复杂度为2O(l logl).

关键词： 线性μ-演算 交换深度 ω-自动机 可判定性 模型验证 检验复杂度

作者: 刘万伟 王戟 陈火旺

作者单位: 国防科学技术大学计算机学院并行与分布处理国家重点实验室,长沙,410073

会议类型: 国内会议

会议名称: 2007全国理论计算机科学学术年会

会议地点: 南宁

会议语种:中文

页码: 1-6

在线出版日期: 2007-11-01（万方平台首次上网日期，不代表论文的发表时间）