Institutional Repository
| 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 |
| 引用统计 | |
| 内容类型 | 会议论文 |
| 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. |
| 条目包含的文件 | 条目无相关文件。 | |||||
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论