[1]虞蕾.PSL可满足问题的计算复杂度[J].计算机技术与发展,2010,(02):16-20.
YU Lei.Computational Complexity of Satisfiability Problems for PSL[J].,2010,(02):16-20.
点击复制
PSL可满足问题的计算复杂度(
)
《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]
- 卷:
-
- 期数:
-
2010年02期
- 页码:
-
16-20
- 栏目:
-
智能、算法、系统工程
- 出版日期:
-
1900-01-01
文章信息/Info
- Title:
-
Computational Complexity of Satisfiability Problems for PSL
- 文章编号:
-
1673-629X（2010）02-0016-05
- 作者:
-
虞蕾1; 2
-
[1]国防科学技术大学计算机学院[2]第二炮兵工程学院计算机系
- Author(s):
-
YU Lei1; 2
-
[1]Computer School, National University of Defense Technology[2]Department of Computer Science, Second Artillery Engineering College
-
- 关键词:
-
PSL; 可满足性问题; 计算复杂度
- Keywords:
-
property specification language; satisfiability problem; computational complexity
- 分类号:
-
TP301.5
- 文献标志码:
-
A
- 摘要:
-
PSL是一种用于描述并行系统的属性规约语言，包括线性时序逻辑FL和分支时序逻辑OBE两部分。由于OBE就是CTL，因此论文重点研究FL逻辑。理论上已证明许多难解的问题都可多项式变换为“可满足性”问题，“可满足性”问题是研究时序逻辑的核心问题之一，并已成为程序验证的一种有力工具；而计算复杂度是“可满足性”问题需要解决的最深刻的方向之一，其研究意义在于它可作为解决一类问题的难度的标准。文中在利用“铺砖模型”基础上，推导并得出FL的“可满足性”问题的计算复杂度为EXPSPACE—hard，这对正确评价解决该问题
- Abstract:
-
PSL is a property specification language which describes parallel systems and is divided into two parts, i.e. FL and OBE. Because OBE is essentially the temporal logic CTL（computation tree logic）, and PSL formulas with clock statements can be easily rewri
备注/Memo
- 备注/Memo:
-
中国博士后科学基金（20080431401）虞蕾（1978-），女，浙江浦江人，博士后，讲师，研究方向为模型检验和航迹规划。
更新日期/Last Update:
1900-01-01