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

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