%0 Journal Article
%T 有穷时间投影时序逻辑的完备公理系统
%A 舒新峰？
%A 段振华？
%J 软件学报
%P 366-380
%D 2011
%R 10.3724/SP.J.1001.2011.03918
%X 为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projectiontemporallogic,简称ptl)的一个完备公理系统.在介绍ptl的语法、语义并给出公理系统后,提出了ptl公式的正则形(normalform,简称nf)和正则图(normalformgraph,简称nfg).基于nf给出了nfg的构造算法,并利用nfg可描述公式模型的性质证明ptl公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了ptl及其公理系统在系统验证中的应用.结果表明,基于ptl的定理证明方法可方便用于并发系统的建模与验证.
%K 投影时序逻辑
%K 公理系统
%K 完备性证明
%K 定理证明
%K 形式化方法
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3918&flag=1