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

• 作者: 段振华 舒新峰
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 投影时序逻辑 公理系统 完备性证明 定理证明 形式化方法
• 年，卷（期）: 2011,（3）
• 页码范围: 366-380
• 分类号: TP301
• 字数: 14275字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2011.03918

摘要

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