ISCAS OpenIR  > 2010软件所会议论文
axiomatic semantics of projection temporal logic programs
Yang Xiaoxiao; Duan Zhenhua; Ma Qian
2010
Conference Name6th International Conference on Theory and Application of Models of Computation (TAMC 09)
SourceMathematical Structures in Computer Science
Pages865-914
Conference DateMAY 18-22,
Conference PlaceChangsha, PEOPLES R CHINA
Indexed Typesci,acm,ei
Publish Place32 AVENUE OF THE AMERICAS, NEW YORK, NY 10013-2473 USA
PublisherMATHEMATICAL STRUCTURES IN COMPUTER SCIENCE
ISSN0960-1295
DepartmentYang, 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.
English AbstractIn 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.
KeywordLogic Programming Semantics
Language英语
WOS IDWOS:000284044600009
Citation statistics
Cited Times:9[WOS]   [WOS Record]     [Related Records in WOS]
Content Type会议论文
URIhttp://ir.iscas.ac.cn/handle/311060/8680
Collection2010软件所会议论文
Recommended Citation
GB/T 7714
Yang Xiaoxiao,Duan Zhenhua,Ma Qian. axiomatic semantics of projection temporal logic programs[C]. 32 AVENUE OF THE AMERICAS, NEW YORK, NY 10013-2473 USA:MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE,2010:865-914.
Files in This Item:
There are no files associated with this item.
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[Yang Xiaoxiao]'s Articles
[Duan Zhenhua]'s Articles
[Ma Qian]'s Articles
Baidu academic
Similar articles in Baidu academic
[Yang Xiaoxiao]'s Articles
[Duan Zhenhua]'s Articles
[Ma Qian]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Yang Xiaoxiao]'s Articles
[Duan Zhenhua]'s Articles
[Ma Qian]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.
 

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