{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:56:59Z","timestamp":1725796619409},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319087825"},{"type":"electronic","value":"9783319087832"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08783-2_7","type":"book-chapter","created":{"date-parts":[[2014,7,5]],"date-time":"2014-07-05T10:04:30Z","timestamp":1404554670000},"page":"71-83","source":"Crossref","is-referenced-by-count":1,"title":["An Axiomatization for Cylinder Computation Model"],"prefix":"10.1007","author":[{"given":"Nan","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":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Heidelberg (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0031816","volume-title":"Formal Methods in Computer-Aided Design","author":"B. Brock","year":"1996","unstructured":"Brock, B., Kaufmann, M., Moore, J.: ACL2 theorems about commercial micro-processors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 275\u2013293. Springer, Heidelberg (1996)"},{"key":"7_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":"7_CR4","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 Informatica\u00a045, 43\u201378 (2008)","journal-title":"Acta Informatica"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-88194-0_12","volume-title":"Formal Methods and Software Engineering","author":"Z. Duan","year":"2008","unstructured":"Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Araki, K., Maibaum, T. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 167\u2013186. Springer, Heidelberg (2008)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1016\/j.tcs.2012.01.026","volume":"497","author":"Z. Duan","year":"2013","unstructured":"Duan, Z., Zhang, N., Koutny, M.: A complete proof system for propositional projection temporal logic. Theoretical Computer Science\u00a0497, 84\u2013107 (2013)","journal-title":"Theoretical Computer Science"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theoretical Computer Science (2014) doi:10.1016\/j.tcs.2014.02.011","DOI":"10.1016\/j.tcs.2014.02.011"},{"key":"7_CR8","unstructured":"Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press (1993)"},{"issue":"5","key":"7_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Trans. Softw. Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Symbolic Model Checking: An Approach to the State Explosion Problem, Dordrecht (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"7_CR11","series-title":"LNAI","first-page":"748","volume-title":"Proceedings of the 11th International Conference on Automated Deduction","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"7_CR13","unstructured":"Sistla, A.: Theoretical issues in the design and verification of distributed systems, Ph.D. Thesis. Harvard University (1983)"},{"issue":"18","key":"7_CR14","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. Theoretical Computer Science\u00a0412(18), 1729\u20131744 (2011)","journal-title":"Theoretical Computer Science"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Vardi, M.: A temporal fixpoint calculus. In: POPL 1988, pp. 250\u2013259 (1988)","DOI":"10.1145\/73560.73582"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Control\u00a056, 72\u201399 (1983)","journal-title":"Information and Control"},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1016\/j.tcs.2012.02.011","volume":"497","author":"N. Zhang","year":"2013","unstructured":"Zhang, N., Duan, Z., Tian, C.: A cylinder computation model for many-core parallel computing. Theoretical Computer Science\u00a0497, 68\u201383 (2013)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Computing and Combinatorics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08783-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T02:40:17Z","timestamp":1558924817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08783-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319087825","9783319087832"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08783-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}