{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:43:19Z","timestamp":1777596199501,"version":"3.51.4"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2017,5,25]],"date-time":"2017-05-25T00:00:00Z","timestamp":1495670400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s11704-016-6059-4","type":"journal-article","created":{"date-parts":[[2017,5,25]],"date-time":"2017-05-25T10:05:40Z","timestamp":1495706740000},"page":"762-785","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["MSVL: a typed language for temporal logic programming"],"prefix":"10.1007","volume":"11","author":[{"given":"Xiaobing","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liang","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,5,25]]},"reference":[{"issue":"5","key":"6059_CR1","doi-asserted-by":"crossref","first-page":"1100","DOI":"10.1109\/TSE.2011.102","volume":"38","author":"S Y Liu","year":"2012","unstructured":"Liu S Y, Chen Y T, Nagoya F, McDermid J A. Formal specificationbased inspection for verification of programs. IEEE Transactions on Software Engineering, 2012, 38(5): 1100\u20131122","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"6059_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10703-010-0099-4","volume":"37","author":"S U J Lee","year":"2010","unstructured":"Lee S U J, Dobbie G, Sun J, Groves L. Theorem prover approach to semistructured data design. Formal Methods in System Design, 2010, 37(1): 1\u201360","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"6059_CR3","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s11704-013-1268-6","volume":"7","author":"Z Y Liu","year":"2013","unstructured":"Liu Z Y, Pang J, Zhang C Y. Design and formal verification of a CEM protocol with transparent TTP. Frontiers of Computer Science, 2013, 7(2): 279\u2013297","journal-title":"Frontiers of Computer Science"},{"issue":"1","key":"6059_CR4","first-page":"4","volume":"12","author":"Z J Ding","year":"2013","unstructured":"Ding Z J, Jiang C J, Zhou M C. Design, analysis and verification of real-time systems based on time petri net refinement. ACM Transactions on Embedded Computing Systems, 2013, 12(1): 4","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"6059_CR5","doi-asserted-by":"crossref","DOI":"10.1002\/9781119991472","volume-title":"An Introduction to Practical Formal Methods Using Temporal Logic","author":"M Fisher","year":"2011","unstructured":"Fisher M. An Introduction to Practical Formal Methods Using Temporal Logic. Chichester: John Wiley & Sons, 2011"},{"issue":"4","key":"6059_CR6","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10009-014-0306-5","volume":"16","author":"C Gherghina","year":"2014","unstructured":"Gherghina C, David C, Qin S, Chin W N. Expressive program verification via structured specifications. International Journal on Software Tools for Technology Transfer, 2014, 16(4): 363\u2013380","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"1","key":"6059_CR7","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1145\/357980.358021","volume":"26","author":"C A R Hoare","year":"1983","unstructured":"Hoare C A R. Communicating sequential processes. Communications of the ACM, 1983, 26(1): 100\u2013106","journal-title":"Communications of the ACM"},{"key":"6059_CR8","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1982","unstructured":"Milner R. A Calculus of Communicating Systems. Secaucus, NJ: Springer-Verlag New York, Inc., 1982"},{"issue":"1","key":"6059_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner R, Parrow J, Walker D. A calculus of mobile processes, i. Information and Computation, 1992, 100(1): 1\u201340","journal-title":"Information and Computation"},{"key":"6059_CR10","volume-title":"Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics Series","author":"D Perrin","year":"2004","unstructured":"Perrin D, Pin J \u00c9. Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics Series. London, San Diego (Calif.): Academic, 2004"},{"issue":"4","key":"6059_CR11","doi-asserted-by":"crossref","first-page":"729","DOI":"10.1007\/s00165-013-0280-9","volume":"26","author":"J S Dong","year":"2014","unstructured":"Dong J S, Liu Y, Sun J, Zhang X. Towards verification of computation orchestration. Formal Aspects of Computing, 2014, 26(4): 729\u2013759","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"6059_CR12","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z H Duan","year":"2008","unstructured":"Duan Z H, Yang X X, Koutny M. Framed temporal logic programming. Science of Computer Programming, 2008, 70(1): 31\u201361","journal-title":"Science of Computer Programming"},{"key":"6059_CR13","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-540-88194-0_12","volume-title":"In: Proceedings of the 10th International Conference on Formal Methods and Software Engineering.","author":"Z H Duan","year":"2008","unstructured":"Duan Z H, Tian C. A unified model checking approach with projection temporal logic. In: Proceedings of the 10th International Conference on Formal Methods and Software Engineering. 2008, 167\u2013186"},{"issue":"1","key":"6059_CR14","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1016\/j.jlap.2008.08.001","volume":"78","author":"X X Yang","year":"2008","unstructured":"Yang X X, Duan Z H. Operational semantics of framed tempura. The Journal of Logic and Algebraic Programming, 2008, 78(1): 22\u201351","journal-title":"The Journal of Logic and Algebraic Programming"},{"issue":"5","key":"6059_CR15","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1017\/S0960129510000241","volume":"20","author":"X X Yang","year":"2010","unstructured":"Yang X X, Duan Z H, Ma Q. Axiomatic semantics of projection temporal logic programs. Mathematical Structures in Computer Science, 2010, 20(5): 865\u2013914","journal-title":"Mathematical Structures in Computer Science"},{"key":"6059_CR16","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/j.tcs.2013.12.014","volume":"554","author":"N Zhang","year":"2014","unstructured":"Zhang N, Duan Z H, Tian C, Du D Z. A formal proof of the deadline driven scheduler in PPTL axiomatic system. Theoretical Computer Science, 2014, 554: 229\u2013253","journal-title":"Theoretical Computer Science"},{"key":"6059_CR17","first-page":"72","volume-title":"Proceedings of the 17th IEEE International Conference on Computer Supported Cooperative Work in Design.","author":"P Zhang","year":"2013","unstructured":"Zhang P, Duan Z H, Tian C. Simulation of CTCS-3 protocol with temporal logic programming. In: Proceedings of the 17th IEEE International Conference on Computer Supported Cooperative Work in Design. 2013, 72\u201377"},{"key":"6059_CR18","first-page":"118","volume-title":"In: Proceedings of the International Workshop on Structured Object-Oriented Formal Language and Method.","author":"X B Wang","year":"2015","unstructured":"Wang X B, Sun T. A method based on MSVL for verification of the social network privacy policy. In: Proceedings of the International Workshop on Structured Object-Oriented Formal Language and Method. 2015, 118\u2013131"},{"key":"6059_CR19","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1016\/j.ins.2016.01.036","volume":"363","author":"Y Shi","year":"2016","unstructured":"Shi Y, Tian C, Duan Z H, Zhou M C. Model checking petri nets with MSVL. Information Sciences, 2016, 363: 274\u2013291","journal-title":"Information Sciences"},{"issue":"18","key":"6059_CR20","doi-asserted-by":"crossref","first-page":"1729","DOI":"10.1016\/j.tcs.2010.12.047","volume":"412","author":"C Tian","year":"2011","unstructured":"Tian C, Duan Z H. Expressiveness of propositional projection temporal logic with star. Theoretical Computer Science, 2011, 412(18): 1729\u20131744","journal-title":"Theoretical Computer Science"},{"key":"6059_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. New York, NY: Springer-Verlag New York, Inc., 1992"},{"key":"6059_CR22","doi-asserted-by":"crossref","first-page":"159","DOI":"10.4018\/978-1-4666-4253-9.ch010","volume-title":"Natural Computing for Simulation and Knowledge Discovery. IGI Global","author":"R Lefticaru","year":"2014","unstructured":"Lefticaru R, Tudose C, Ipate F. Towards automated verification of P systems using Spin. In: de Castro L N, ed. Natural Computing for Simulation and Knowledge Discovery. IGI Global, 2014, 159\u2013170"},{"issue":"2","key":"6059_CR23","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/1646353.1646361","volume":"53","author":"A Wright","year":"2010","unstructured":"Wright A. Type theory comes of age. Communications of the ACM, 2010, 53(2): 16\u201317","journal-title":"Communications of the ACM"},{"key":"6059_CR24","first-page":"257","volume-title":"Proceedings of the International Colloquium on Theoretical Aspects of Computing.","author":"S L Wang","year":"2006","unstructured":"Wang S L, Long Q, Qiu Z Y. Type Safety for FJ and FGJ. In: Proceedings of the International Colloquium on Theoretical Aspects of Computing. 2006, 257\u2013271"},{"issue":"1","key":"6059_CR25","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s11704-012-1307-8","volume":"7","author":"W Ke","year":"2013","unstructured":"Ke W, Liu Z M, Wang S L, Zhao L. A graph-based generic type system for object-oriented programs. Frontiers of Computer Science, 2013, 7(1): 109\u2013134","journal-title":"Frontiers of Computer Science"},{"key":"6059_CR26","first-page":"147","volume-title":"In: Proceedings of the International Symposium on Formal Methods.","author":"D Cousineau","year":"2012","unstructured":"Cousineau D, Doligez D, Lamport L, Merz S, Ricketts D, Vanzetto H. Tla + proofs. In: Proceedings of the International Symposium on Formal Methods. 2012, 147\u2013154"},{"key":"6059_CR27","first-page":"1","volume-title":"Multi-Agent Programming: Languages, Tools and Applications","author":"M Fisher","year":"2009","unstructured":"Fisher M, Hepple A. Executing logical agent specifications. In: El Fallah Seghrouchni A, Dix J, Dastani M, et al., eds. Multi-Agent Programming: Languages, Tools and Applications. Boston, MA: Springer US, 2009, 1\u201327"},{"key":"6059_CR28","first-page":"36","volume-title":"Proceedings of the International Colloquium on Theoretical Aspects of Computing.","author":"L Lamport","year":"2009","unstructured":"Lamport L. The PlusCal algorithm language. In: Proceedings of the International Colloquium on Theoretical Aspects of Computing. 2009, 36\u201360"},{"issue":"9","key":"6059_CR29","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1145\/2500468.2494558","volume":"56","author":"M Fisher","year":"2013","unstructured":"Fisher M, Dennis L, Webster M. Verifying autonomous systems. Communications of the ACM, 2013, 56(9): 84\u201393","journal-title":"Communications of the ACM"},{"key":"6059_CR30","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/978-3-319-04915-1_5","volume-title":"Proceedings of the 3rd International Workshop on Structured Object-Oriented Formal Language and Method.","author":"X B Wang","year":"2014","unstructured":"Wang X B, Duan Z H, Zhao L. Formalizing and implementing types in MSVL. In: Proceedings of the 3rd International Workshop on Structured Object-Oriented Formal Language and Method. 2014, 62\u201375"},{"key":"6059_CR31","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z H Duan","year":"2006","unstructured":"Duan Z H. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2006"},{"issue":"11","key":"6059_CR32","doi-asserted-by":"crossref","first-page":"1203","DOI":"10.1002\/1097-024X(200009)30:11<1203::AID-SPE338>3.0.CO;2-N","volume":"30","author":"E R Gansner","year":"2000","unstructured":"Gansner E R, North S C. An open graph visualization system and its applications to software engineering. Software Practice and Experience, 2000, 30(11): 1203\u20131233","journal-title":"Software Practice and Experience"},{"issue":"1","key":"6059_CR33","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1017\/S096012950800738X","volume":"19","author":"C Tian","year":"2009","unstructured":"Tian C, Duan Z H. Complexity of propositional projection temporal logic with star. Mathematical Structures in Computer Science, 2009, 19(1): 73\u2013100","journal-title":"Mathematical Structures in Computer Science"},{"key":"6059_CR34","volume-title":"The Art of Computer Programming, Vol 3: Sorting and Searching","author":"D E Knuth","year":"1998","unstructured":"Knuth D E. The Art of Computer Programming, Vol 3: Sorting and Searching. 2nd ed. Redwood City, CA: AddisonWesley Longman Publishing Co., Inc., 1998"},{"key":"6059_CR35","volume-title":"Principles of Concurrent and Distributed Programming","author":"M Ben-Ari","year":"2006","unstructured":"Ben-Ari M. Principles of Concurrent and Distributed Programming (Prentice-Hall International Series in Computer Science). 2nd ed. Boston, MA: Addison-Wesley Longman Publishing Co., Inc., 2006"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-016-6059-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-016-6059-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-016-6059-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,25]],"date-time":"2019-09-25T01:43:32Z","timestamp":1569375812000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-016-6059-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,25]]},"references-count":35,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["6059"],"URL":"https:\/\/doi.org\/10.1007\/s11704-016-6059-4","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5,25]]}}}