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

Computational Complexity of Satisfiability Problems for PSL

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

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 rewritten to uncloeked formulas, this work studies with emphasis on the unclocked FL logic. It has long been verified that many hard problems can be translated into the correspongding satisfiability（SAT） problems in polynomial time, and SAT problems are central for temporal logic in order to be a useful tool in program verification. The computational complexity is one of the most impotant theories to be resloved for SAT problems in order to bring on the hardness criterion for one series of problems. The complexity of FL has been studied with the help of the computation model of＂tiling＂ and the result shows the satisfiability of FL is EXPSPACE - hard, which has important values for evaluating the efficiency and further determining the improvement of FL SAT problems＇ algorithms.