中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 2010软件所会议论文
题名:
axiomatic semantics of projection temporal logic programs
作者: Yang Xiaoxiao ; Duan Zhenhua ; Ma Qian
会议文集: Mathematical Structures in Computer Science
会议名称: 6th International Conference on Theory and Application of Models of Computation (TAMC 09)
会议日期: MAY 18-22,
出版日期: 2010
会议地点: Changsha, PEOPLES R CHINA
关键词: Logic programming ; Semantics
出版者: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE
出版地: 32 AVENUE OF THE AMERICAS, NEW YORK, NY 10013-2473 USA
收录类别: sci,acm,ei
ISSN: 0960-1295
部门归属: Yang, Xiaoxiao; Duan, Zhenhua; Ma, Qian Xidian Univ, Inst Comp Theory & Technol, Xian 710071, Peoples R China. Yang, Xiaoxiao; Duan, Zhenhua; Ma, Qian Xidian Univ, ISN Lab, Xian 710071, Peoples R China. Yang, Xiaoxiao Chinese Acad Sci, Comp Sci Lab, Inst Software, Beijing 100080, Peoples R China.
英文摘要: In this paper, we investigate the axiomatic semantics of the projection temporal logic programming language MSVL. To this end, we employ Propositional Projection Temporal Logic (PPTL) as an assertion language to specify the desired properties. We give a set of state axioms and state inference rules. In order to deduce a program over an interval, we also formalise a set of rules in terms of a Hoare logic-like triple. These rules enable us to deduce a program into its normal form and from the current state to the next one. They also enable us to verify properties over intervals. In this way, an axiom system for proving the correctness of MSVL programs is established. The axiom system is proved to be sound and relatively complete with respect to an operational model of MSVL, and give an example showing how the axiom system works. Finally, we employ a recently developed prototype verifier based on PVS as an example of semi-automatic verification using MSVL.
语种: 英语
Citation statistics:
内容类型: 会议论文
URI标识: http://ir.iscas.ac.cn/handle/311060/8680
Appears in Collections:中科院软件所图书馆_2010软件所会议论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
Yang Xiaoxiao,Duan Zhenhua,Ma Qian. axiomatic semantics of projection temporal logic programs[C]. 见:6th International Conference on Theory and Application of Models of Computation (TAMC 09). Changsha, PEOPLES R CHINA. MAY 18-22,.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Yang Xiaoxiao]'s Articles
[Duan Zhenhua]'s Articles
[Ma Qian]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Yang Xiaoxiao]‘s Articles
[Duan Zhenhua]‘s Articles
[Ma Qian]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace