%0 Journal Article
%T Complete Axiomatization for Projection Temporal Logic with Finite Time<br>有穷时间投影时序逻辑的完备公理系统
%A SHE Xin-Feng
%A DUAN Zhen-Hua
%A <br>舒新峰
%A 段振华
%J 软件学报
%D 2011
%I 
%X 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.
%K projection temporal logic
%K axiomatization
%K completeness proof
%K theorem proving
%K formal method<br>投影时序逻辑
%K 公理系统
%K 完备性证明
%K 定理证明
%K 形式化方法
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=995E8F87112E625EAE2601C2D4C3536B&yid=9377ED8094509821&vid=BC12EA701C895178&iid=38B194292C032A66&sid=2E41258BCB9A7DB2&eid=A7AE820C12CC9AD3&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=16