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) |
| 会议日期 | MAY 18-22, |
| 会议地点 | Changsha, PEOPLES R CHINA |
| 关键词 | Logic programming Semantics |
| 页码 | 865-914 |
| 英文摘要 | 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. |
| 收录类别 | SCI,ACM,EI |
| 会议录 | Mathematical Structures in Computer Science
 |
| 会议录出版者 | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE |
| 会议录出版地 | 32 AVENUE OF THE AMERICAS, NEW YORK, NY 10013-2473 USA |
| 语种 | 英语 |
| ISSN号 | 0960-1295 |
| WOS记录号 | WOS:000284044600009 |
| 源URL | [http://124.16.136.157/handle/311060/8680]  |
| 专题 | 软件研究所_软件所图书馆_2010软件所会议论文 |
| 推荐引用方式 GB/T 7714 | 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,. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。