{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:57:47Z","timestamp":1725569867744},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_8","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T12:40:06Z","timestamp":1289220006000},"page":"90-105","source":"Crossref","is-referenced-by-count":3,"title":["An Improved Decision Procedure for Propositional Projection Temporal Logic"],"prefix":"10.1007","author":[{"given":"Zhenhua","family":"Duan","sequence":"first","affiliation":[]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S.A. Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic I: normal propositional calculi. Z. Math. Logik Grund. Math.\u00a09, 67\u201396 (1963)","journal-title":"Z. Math. Logik Grund. Math."},{"key":"8_CR2","unstructured":"Moszkowski, B.: Reasoning about digital circuits, Ph.D Thesis, Department of Computer Science, Stanford University, TRSTAN-CS-83-970 (1983)"},{"key":"8_CR3","unstructured":"Duan, Z.: An Extended Interval Temporal Logic and A Framing Technique for Temporal Logic Programming. PhD thesis, University of Newcastle Upon Tyne (May 1996)"},{"issue":"1","key":"8_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(1), 43\u201378 (2008)","journal-title":"Acta Informatica"},{"key":"8_CR5","unstructured":"Wang, H., Xu, Q.: Temporal logics over infinite intervals. Technical Report 158, UNU\/IIST, Macau (1999)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.C.: A Complete Axiomatization of Interval Temporal Logic with Infinite Time. In: 15th Annual IEEE Symposium on Logic in Computer Science. LICS, p. 241 (2000)","DOI":"10.1109\/LICS.2000.855773"},{"issue":"5","key":"8_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z. Chaochen","year":"1991","unstructured":"Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of duration. Information Processing Letters\u00a040(5), 269\u2013275 (1991)","journal-title":"Information Processing Letters"},{"issue":"2","key":"8_CR8","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1093\/logcom\/13.2.195","volume":"13","author":"H. Bowman","year":"2003","unstructured":"Bowman, H., Thompson, S.: A decision procedure and complete axiomatization of interval temporal logic with projection. Journal of logic and Computation\u00a013(2), 195\u2013239 (2003)","journal-title":"Journal of logic and Computation"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Complete proof systems for first order interval temporal logic. In: Proceedings of LICS 1995, pp. 36\u201343 (1995)","DOI":"10.1109\/LICS.1995.523242"},{"key":"8_CR10","volume-title":"Model Checking","author":"M. Clark","year":"2000","unstructured":"Clark, M., Gremberg, O., Peled, A.: Model Checking. The MIT Press, Cambridge (2000)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. Found. of Comp. Sci., pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"8_CR12","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":"C. Tian","year":"2008","unstructured":"Tian, C., Duan, Z.: Propositional Projection Temporal Logic, B\u00fcchi Automata and \u03c9-Expressions. In: Agrawal, M., Du, D.-Z., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol.\u00a04978, pp. 47\u201358. Springer, Heidelberg (2008)"},{"issue":"1","key":"8_CR13","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1017\/S096012950800738X","volume":"19","author":"C. Tian","year":"2009","unstructured":"Tian, C., Duan, Z.: Complexity of Propositional Projection Temporal Logic with Star. Mathematical Structure in Computer Science\u00a019(1), 73\u2013100 (2009)","journal-title":"Mathematical Structure in Computer Science"},{"key":"8_CR14","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. In: Foundations of Computing. The MIT Press, Cambridge"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-540-70918-3_2","volume-title":"STACS 2007","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: The B\u00fcchi Complementation Saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol.\u00a04393, pp. 12\u201322. Springer, Heidelberg (2007)"},{"key":"8_CR16","unstructured":"Katoen, J.-P.: Concepts, Algorithms, and Tools for Model Checking. Lecture Notes of the Course Mechanised Validation of Parrel Systems (1999)"},{"key":"8_CR17","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.\u00a04789, pp. 246\u2013265. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T23:38:42Z","timestamp":1553211522000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}