{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,31]],"date-time":"2024-03-31T21:41:06Z","timestamp":1711921266869},"reference-count":40,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2010,10,27]],"date-time":"2010-10-27T00:00:00Z","timestamp":1288137600000},"content-version":"unspecified","delay-in-days":26,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2010,10]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1017\/s0960129510000241","type":"journal-article","created":{"date-parts":[[2010,10,27]],"date-time":"2010-10-27T07:48:27Z","timestamp":1288165707000},"page":"865-914","source":"Crossref","is-referenced-by-count":10,"title":["Axiomatic semantics of projection temporal logic programs"],"prefix":"10.1017","volume":"20","author":[{"given":"XIAOXIAO","family":"YANG","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ZHENHUA","family":"DUAN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"QIAN","family":"MA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2010,10,27]]},"reference":[{"key":"S0960129510000241_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/S0096-0551(98)00009-5"},{"key":"S0960129510000241_ref7","unstructured":"Duan Z. (1996) An Extended Interval Temporal Logic and A Framing Technique for Temporal Logic Programming, Ph. D. Thesis, University of Newcastle upon Tyne. (Technical Report No. 556.)"},{"key":"S0960129510000241_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"S0960129510000241_ref17","first-page":"296","volume-title":"Proceedings of the European Conference on Artificial Intelligence (ECAI-88)","author":"Hrycej","year":"1988"},{"key":"S0960129510000241_ref30","unstructured":"Pnueli A. (1977) The temporal semantics of concurrent programs, Tel-Aviv University."},{"key":"S0960129510000241_ref25","unstructured":"Orgun M. A. and Wadge W. W. (1988) Chronolog: A Temporal Logic Programming Language and Its Formal Semantics, Department of Computer Science, University of Victoria, B.C., Canada."},{"key":"S0960129510000241_ref32","first-page":"511","article-title":"Cactus: A Branching Time Logic Programming Language. Proceedings of the 1st International Joint Conference Qualitative and Quantitative Practical Reasoning","volume":"1244","author":"Rondogiannis","year":"1997","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129510000241_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"},{"key":"S0960129510000241_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.001"},{"key":"S0960129510000241_ref13","first-page":"197","volume-title":"Temporal Logics and Their Applications","author":"Gabbay","year":"1987"},{"key":"S0960129510000241_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"S0960129510000241_ref35","first-page":"425","volume-title":"Proceedings of IFIP Congress 83","author":"Tang","year":"1983"},{"key":"S0960129510000241_ref26","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1093\/oso\/9780198537755.003.0002","volume-title":"Intensional Logics for Programming","author":"Orgun","year":"1992"},{"key":"S0960129510000241_ref21","unstructured":"Ma Q. , Duan Z. and Yang X. (2010) Case Study of MSVL Axiom System. Technical Report available at http:\/\/lcs.ios.ac.cn\/~xzx\/case.pdf."},{"key":"S0960129510000241_ref37","unstructured":"Wadge W. W. (1988) Tense Logic Programming. A Respectable Alternative. In: Proceedings of the 1988 International Symposium on Lucid and Intensional Programming, Sidney, B.C., Canada 26\u201332."},{"key":"S0960129510000241_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80070-7"},{"key":"S0960129510000241_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00139-4"},{"key":"S0960129510000241_ref5","volume-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"S0960129510000241_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"S0960129510000241_ref6","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"S0960129510000241_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BF02944904"},{"key":"S0960129510000241_ref9","first-page":"333","article-title":"Projection in temporal logic programming. Proceedings of Logic Programming and Automatic Reasoning","volume":"822","author":"Duan","year":"1994","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129510000241_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-007-0062-z"},{"key":"S0960129510000241_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16492-8_119"},{"key":"S0960129510000241_ref14","first-page":"91","volume-title":"Temporal Logics and Their Applications","author":"Hale","year":"1987"},{"key":"S0960129510000241_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211086"},{"key":"S0960129510000241_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(93)90016-A"},{"key":"S0960129510000241_ref24","volume-title":"Executing temporal logic programs","author":"Moszkowski","year":"1986"},{"key":"S0960129510000241_ref19","unstructured":"Jones C. B. (1981) Development Mehods for Computer Programs including a Notion of Interference, Ph. D. thesis, Oxford University."},{"key":"S0960129510000241_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"S0960129510000241_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"S0960129510000241_ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"S0960129510000241_ref27","unstructured":"Owicki S. (1975) Axiomatic Proof Techniques for Parallel Programs, Ph. D. thesis, Department of Computer Science, Cornell University."},{"key":"S0960129510000241_ref29","unstructured":"Owre S. , Shankar N. , Rushby J. M. and Stringer-Calvert D. W. J. (1999) PVS Language Reference, Computer Science Laboratory, SRI International, Menlo Park, CA."},{"key":"S0960129510000241_ref31","volume-title":"Proceedings of IFIP Working Conference on the Role of Abstract Models in Computer Science","author":"de Roever","year":"1985"},{"key":"S0960129510000241_ref3","first-page":"239","volume-title":"Proceedings of the Tenth International Conference on Logic Programming","author":"Brzoska","year":"1993"},{"key":"S0960129510000241_ref34","unstructured":"Shankar N. , Owre S. , Rushby J. M. and Stringer-Calvert D. W. J. (1999) PVS Prover Guide, Computer Science Laboratory, SRI International, Menlo Park, CA."},{"key":"S0960129510000241_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79228-4_4"},{"key":"S0960129510000241_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211617"},{"key":"S0960129510000241_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.001"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129510000241","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,31]],"date-time":"2024-03-31T21:03:07Z","timestamp":1711918987000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129510000241\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,10]]},"references-count":40,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2010,10]]}},"alternative-id":["S0960129510000241"],"URL":"https:\/\/doi.org\/10.1017\/s0960129510000241","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,10]]}}}