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

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

Computational Complexity of Satisfiability Problems for PSL

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 unclocked 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 tem...