A complete axiom system for propositional projection temporal logic with cylinder computation model

详细信息    查看全文

• 作者：Nan Zhang ^{nanzhang@xidian.edu.cn" class="auth_mail" title="E-mail the corresponding author} ; Zhenhua Duan ; ^{zhhduan@mail.xidian.edu.cn" class="auth_mail" title="E-mail the corresponding author} ; Cong Tian ^{c.tian@mail.xidian.edu.cn" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Axiom system ; Multi-core ; Model ; Specification ; Verification
• 刊名：Theoretical Computer Science
• 出版年：2016
• 出版时间：4 January 2016
• 年：2016
• 卷：609
• 期：part_P3
• 页码：639-657
• 全文大小：512 K

文摘

To specify and verify multi-core parallel programs in a uniform framework, this paper proposes an axiom system for CCM–PPTL which extends that of PPTL by including transformation rules for sequence expressions and axioms as well as inference rules on the CCM construct. Further, the soundness and completeness of the extended axiom system are proved.