PSL可满足问题的计算复杂度

• 作者: 虞蕾
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: PSL 可满足性问题 计算复杂度
• 年，卷（期）: 2010,（2）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 16-20,24
• 页数: 6页
• 分类号: TP301.5
• 字数: 6338字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2010.02.005

摘要

PSL是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL和分支时序逻辑OBE两部分.由于OBE就是CTL,因此论文重点研究FL逻辑.理论上已证明许多难解的问题都可多项式变换为"可满足性"问题,"可满足性"同题是研究时序逻辑的核心问题之一,并已成为程序验证的一种有力工具;而计算复杂度是"可满足性"问题需要解决的最深刻的方向之一,其研究意义在于它可作为解决一类问题的难度的标准.文中在利用"铺砖模型"基础上,推导并得出FL的"可满足性"问题的计算复杂度为EXPSPACE-hard,这对正确评价解决该问题的各种算法的效率,进而确定对已有算法的改进余地具有重要的指导意义.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	虞蕾	国防科学技术大学计算机学院	4	6	2.0	2.0