axiomatic semantics of projection temporal logic programs

ISCAS OpenIR > 2010软件所会议论文

	axiomatic semantics of projection temporal logic programs
	Yang Xiaoxiao; Duan Zhenhua; Ma Qian
	2010
会议名称	6th International Conference on Theory and Application of Models of Computation (TAMC 09)
会议录名称	Mathematical Structures in Computer Science
页码	865-914
会议日期	MAY 18-22,
会议地点	Changsha, PEOPLES R CHINA
收录类别	sci,acm,ei
出版地	32 AVENUE OF THE AMERICAS, NEW YORK, NY 10013-2473 USA
出版者	MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE
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.
关键词	Logic Programming Semantics
语种	英语
WOS记录号	WOS:000284044600009
引用统计	被引频次：9[WOS] [WOS记录] [WOS相关记录]
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/8680
专题	2010软件所会议论文
推荐引用方式 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.