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

摘要：

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

关键词：PSL、可满足性问题、计算复杂度

所属期刊栏目：20

分类号：TP301.5(计算技术、计算机技术)

资助基金：中国博士后科学基金20080431401

在线出版日期：2010-04-21（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：16-20,24