有穷时间投影时序逻辑的完备公理系统

摘要：

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection tamporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.

关键词：投影时序逻辑、公理系统、完备性证明、定理证明、形式化方法

所属期刊栏目：22

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

资助基金：国家自然科学基金60433010,60910004,60873018,91018010,61003078,61003079;国家重点基础研究发展计划9732010CB328102;中央高校基本科研业务费专项资金JY10000903004

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

页数：共15页

页码：366-380