Institutional Repository
| axiomatic semantics of projection temporal logic programs | |
| Yang Xiaoxiao; Duan Zhenhua; Ma Qian | |
| 2010 | |
| Conference Name | 6th International Conference on Theory and Application of Models of Computation (TAMC 09) |
| Source | Mathematical Structures in Computer Science |
| Pages | 865-914 |
| Conference Date | MAY 18-22, |
| Conference Place | Changsha, PEOPLES R CHINA |
| Indexed Type | sci,acm,ei |
| Publish Place | 32 AVENUE OF THE AMERICAS, NEW YORK, NY 10013-2473 USA |
| Publisher | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE |
| ISSN | 0960-1295 |
| Department | 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. |
| English Abstract | 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. |
| Keyword | Logic Programming Semantics |
| Language | 英语 |
| WOS ID | WOS:000284044600009 |
| Citation statistics | |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/8680 |
| Collection | 2010软件所会议论文 |
| 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. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment