avatar avatar 我的文献 有穷时间投影时序逻辑的完备公理系统 作者 舒新峰; 段振华 单位 西安电子科技大学计算理论与技术研究所; 西安电子科技大学ISN国家重点实验室; 西安邮电学院计算机学院 期刊 软件学报 时间 2011年03期 关键词 投影时序逻辑; 公理系统; 完备性证明; 定理证明; 形式化方法 基金 国家自然科学基金(60433010,60910004,60873018,91018010,61003078,61003079); 国家重点基础研究发展计划(973)(2010CB328102); 中央高校基本科研业务费专项资金(JY10000903004)
摘要
为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.
下载 浏览 cnki {{liketext}}
©2020 - iData {{ message }} 关闭