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

摘要

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection tamporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.%To verify the properties of concurrent and reactive systems based on the theorem proving approach, a complete axiomatization is formulized over finite domains for first order projection temporal logic (PTL) with finite time.First, the syntax, semantics and the axiomatization of PTL are presented; next, a normal form (NF) and a normal form graph (NFG) of PTL formulas are defined respectively; further, the algorithm for constructing the NFG is formalized upon the NF; moreover, the decision theorem for PTL formulas and the completeness of the axiomatic system have been proven to be based on the property that the NFG can-describe the models of PTL formulas; finally,an example is given to illustrate how to do system verification based on PTL and its axiomatic system, and the results indicate that the PTL based theorem proving approach can be conveniently applied to modeling and verification of concurrent systems.