{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:37:58Z","timestamp":1759639078375,"version":"3.40.3"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319312194"},{"type":"electronic","value":"9783319312200"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-31220-0_14","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:59:52Z","timestamp":1457773192000},"page":"195-205","source":"Crossref","is-referenced-by-count":0,"title":["PPTL_SPIN: A SPIN Based Model Checker for Propositional Projection Temporal Logic"],"prefix":"10.1007","author":[{"given":"Xiaoming","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Inform. 45(1), 43\u201378 (2008)","journal-title":"Acta Inform."},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.tcs.2014.02.011","volume":"554","author":"Z Duan","year":"2014","unstructured":"Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theor. Comput. Sci. 554, 169\u2013190 (2014). doi:\n                      10.1016\/j.tcs.2014.02.011","journal-title":"Theor. Comput. Sci."},{"key":"14_CR3","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":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-76650-6_15","volume-title":"Formal Methods and Software Engineering","author":"C Tian","year":"2007","unstructured":"Tian, C., Duan, Z.: Model checking propositional projection temporal logic based on SPIN. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 246\u2013265. Springer, Heidelberg (2007)"},{"key":"14_CR5","unstructured":"Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. Ph.D. thesis, University of Newcastle upon Tyne (1996)"},{"issue":"18","key":"14_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. Theor. Comput. Sci. 412(18), 1729\u20131744 (2011). doi:\n                      10.1016\/j.tcs.2010.12.047","journal-title":"Theor. Comput. Sci."},{"key":"14_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-16901-4_8","volume-title":"Formal Methods and Software Engineering","author":"Z Duan","year":"2010","unstructured":"Duan, Z., Tian, C.: An improved decision procedure for propositional projection temporal logic. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 90\u2013105. Springer, Heidelberg (2010)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"issue":"5","key":"14_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-79228-4_4","volume-title":"Theory and Applications of Models of Computation","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Tian, C., Duan, Z.: Propositional projection temporal logic, B\u00fcchi automata and \n                      \n                        \n                      \n                      $$\\omega $$\n                      \n                        \n                          \u03c9\n                        \n                      \n                    -regular expressions. In: Agrawal, M., Du, D.-Z., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol. 4978, pp. 47\u201358. Springer, Heidelberg (2008)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE Symposium Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-31220-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T14:59:10Z","timestamp":1559401150000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-31220-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319312194","9783319312200"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-31220-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}