{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:04:35Z","timestamp":1743026675086,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319049144"},{"type":"electronic","value":"9783319049151"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-04915-1_5","type":"book-chapter","created":{"date-parts":[[2014,2,20]],"date-time":"2014-02-20T15:12:22Z","timestamp":1392909142000},"page":"62-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Formalizing and Implementing Types in MSVL"],"prefix":"10.1007","author":[{"given":"Xiaobing","family":"Wang","sequence":"first","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":[[2014,2,21]]},"reference":[{"key":"5_CR1","first-page":"995","volume-title":"In: Handbook of Theoretical Computer Science","author":"E Allen Emerson","year":"1995","unstructured":"Allen Emerson, E.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, pp. 995\u20131072. Elsevier, Amsterdam (1995)"},{"key":"5_CR2","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"5_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/BF02944904","volume":"19","author":"Z Duan","year":"2004","unstructured":"Duan, Z., Maciej, K.: A framed temporal logic programming language. J. Comput. Sci. Technol. 19, 341\u2013351 (2004)","journal-title":"J. Comput. Sci. Technol."},{"key":"5_CR5","series-title":"LNCS","first-page":"167","volume-title":"ICFEM 2008","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167\u2013186. Springer, Heidelberg (2008)"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"1729","DOI":"10.1016\/j.tcs.2010.12.047","volume":"412","author":"C Tian","year":"2011","unstructured":"Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412, 1729\u20131744 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR7","unstructured":"Cau, A., Moszkowski, B., Zedan, H.: Itl and tempura home page on the web. http:\/\/www.cse.dmu.ac.uk\/STRL\/ITL\/ (2013)"},{"key":"5_CR8","volume-title":"Temporal Logic Program Designing and Engineering","author":"Z Tang","year":"1999","unstructured":"Tang, Z.: Temporal Logic Program Designing and Engineering. Science Press, Beijing (1999)"},{"key":"5_CR9","unstructured":"Lamport, L.: The TLA Home Page. http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/tla.html (2013)"},{"key":"5_CR10","series-title":"LNCS (LNAI)","first-page":"3","volume-title":"PROMAS 2005","author":"M Fisher","year":"2006","unstructured":"Fisher, M.: MetateM: the story so far. In: Bordini, R.H., Dastani, M.M., Dix, J., El Fallah Seghrouchni, A. (eds.) PROMAS 2005. LNCS (LNAI), vol. 3862, pp. 3\u201322. Springer, Heidelberg (2006)"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1016\/j.sysarc.2004.12.003","volume":"51","author":"S Zhou","year":"2005","unstructured":"Zhou, S., Zedan, H., Cau, A.: Run-time analysis of time-critical systems. J. Syst. Archit. 51, 331\u2013345 (2005)","journal-title":"J. Syst. Archit."},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70, 31\u201361 (2008)","journal-title":"Sci. Comput. Program."},{"key":"5_CR13","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z Duan","year":"2006","unstructured":"Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2006)"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.jlap.2008.08.001","volume":"78","author":"X Yang","year":"2008","unstructured":"Yang, X., Duan, Z.: Operational semantics of framed tempura. J. Logic Algebraic Program. 78, 22\u201351 (2008)","journal-title":"J. Logic Algebraic Program."},{"key":"5_CR15","unstructured":"Duan, Z., Wang, X.: Implementing pointer in temporal logic programming languages. In: Proceedings of SBMF 2006, pp. 171\u2013184 (2006)"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-04915-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,19]],"date-time":"2023-01-19T17:13:02Z","timestamp":1674148382000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-04915-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319049144","9783319049151"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-04915-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"21 February 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}