{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T17:13:17Z","timestamp":1772039597978,"version":"3.50.1"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,11,20]],"date-time":"2007-11-20T00:00:00Z","timestamp":1195516800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2008,2]]},"DOI":"10.1007\/s00236-007-0062-z","type":"journal-article","created":{"date-parts":[[2007,11,19]],"date-time":"2007-11-19T04:09:55Z","timestamp":1195445395000},"page":"43-78","source":"Crossref","is-referenced-by-count":125,"title":["A decision procedure for propositional projection temporal logic with infinite models"],"prefix":"10.1007","volume":"45","author":[{"given":"Zhenhua","family":"Duan","sequence":"first","affiliation":[]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[]},{"given":"Li","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,11,20]]},"reference":[{"key":"62_CR1","unstructured":"Moszkowski, B.C.: Reasoning about digital circuits. PhD Thesis, Stanford University. TRSTAN-CS-83-970 (1983)"},{"key":"62_CR2","unstructured":"Rosner, R., Pnueli, A.: A choppy logic. In: First annual IEEE symposium on logic in computer science, LICS, pp. 306\u2013314 (1986)"},{"key":"62_CR3","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\u201900), LICS, p. 241, (2000)","DOI":"10.1109\/LICS.2000.855773"},{"issue":"5","key":"62_CR4","doi-asserted-by":"crossref","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. and Ravn A.P. (1991). A calculus of duration. Inf. Process. Lett. 40(5): 269\u2013275","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"62_CR5","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1093\/logcom\/13.2.195","volume":"13","author":"H. Bowman","year":"2003","unstructured":"Bowman H. and Thompson S. (2003). A decision procedure and complete axiomatization of interval temporal logic with projection. J. Logic Comput. 13(2): 195\u2013239","journal-title":"J. Logic Comput."},{"key":"62_CR6","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Complete proof systems for first order interval temporal logic. In: Proceedings of LICS\u201995, pp. 36\u201343 (1995)","DOI":"10.1109\/LICS.1995.523242"},{"key":"62_CR7","unstructured":"Wang, H., Xu, Q.: Temporal logics over infinite intervals. Technical Report 158, UNU\/IIST, Macau (1999)"},{"key":"62_CR8","doi-asserted-by":"crossref","unstructured":"Halpern, J., Manna, Z., Moszkowski, B.: A hardware semantics based on temporal intervals. In: Proceedings of the 10th international conlloquium on automata, Languages and Programming, vol. 154. Springer, LNCS, Barcelona (1983)","DOI":"10.1007\/BFb0036915"},{"key":"62_CR9","doi-asserted-by":"crossref","unstructured":"Kono, S.: A combination of clausal and non-clausal temporal logic programs. In: Lecture notes in artificial intelligence, vol. 897, pp. 40\u201357. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-58976-7_3"},{"key":"62_CR10","doi-asserted-by":"crossref","unstructured":"Bowman, H., Thompson, S.: A Tableau method for interval temporal logic with projection. In: de Swart, H. (ed.) TABLEAUX98, LNAI 1397, Springer, Berlin (1998)","DOI":"10.1007\/3-540-69778-0_17"},{"key":"62_CR11","unstructured":"Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle Upon Tyne (1996)"},{"key":"62_CR12","volume-title":"Temporal Logic and Temporal Logic Programming Language","author":"Z. Duan","year":"2006","unstructured":"Duan Z. (2006). Temporal Logic and Temporal Logic Programming Language. Science press, Beijing"},{"key":"62_CR13","doi-asserted-by":"crossref","unstructured":"Duan, Z., Koutny, M., Holt, C.: Projection in temporal logic programming. In: Pfenning, F. (ed.) Proceedings of logic programming and automatic reasoning, Lecture Notes in Artificial Intelligence, vol. 822, pp. 333\u2013344. Springer, Heidelberg (1994)","DOI":"10.1007\/3-540-58216-9_48"},{"key":"62_CR14","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF02973464","volume":"19","author":"Z. Duan","year":"2004","unstructured":"Duan Z. and Koutny M. (2004). A framed temporal logic programming language. J. Comput. Sci. Technol. 19: 333\u2013344","journal-title":"J. Comput. Sci. Technol."},{"key":"62_CR15","doi-asserted-by":"crossref","unstructured":"Duan, Z., Yang, X., Kounty, M.: Semantics of framed temporal logic programs. In: Proceedings of ICLP 2005, vol. 3668, pp. 256\u2013270. LNCS, Barcelona (2005)","DOI":"10.1007\/11562931_27"},{"key":"62_CR16","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.C.: Compositional reasoning about projected and infinite time. In: Proceeding of the first IEEE international conference on engineering of complex computer systems (ICECCS\u201995), pp. 238\u2013245. IEEE Computer Society Press (1995)","DOI":"10.1109\/ICECCS.1995.479336"},{"key":"62_CR17","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. and Pnueli A. (1992). The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg"},{"key":"62_CR18","unstructured":"Duan, Z., Zhang, L.: A decision procedure for propositional projection temporal logic. Technical Report No.1, Institute of computing Theory and Technology, Xidian University, Xi\u2019an, People\u2019s Republic of China, http:\/\/www.paper.edu.cn\/en\/paper.php?serial_number=200611-427 (2005)"},{"key":"62_CR19","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S.A. Kripke","year":"1963","unstructured":"Kripke S.A. (1963). Semantical analysis of modal logic I: normal propositional calculi. Z. Math. Logik Grund. Math. 9: 67\u201396","journal-title":"Z. Math. Logik Grund. Math."},{"key":"62_CR20","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. Foundations of Computing. MIT, Cambridge"},{"issue":"5","key":"62_CR21","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann G.J. (1997). The Model Checker Spin. IEEE Trans. Softw. Eng. 23(5): 279\u2013295","journal-title":"IEEE Trans. Softw. Eng."},{"key":"62_CR22","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"2","key":"62_CR23","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/0022-0000(82)90003-4","volume":"25","author":"D. Harel","year":"1982","unstructured":"Harel D., Kozen D. and Parikh R. (1982). Process logic: expressiveness, decidability, completeness. J. Comput. Syst. Sci. 25(2): 144\u2013170","journal-title":"J. Comput. Syst. Sci."},{"issue":"4","key":"62_CR24","doi-asserted-by":"crossref","first-page":"935","DOI":"10.1137\/0214066","volume":"14","author":"A. Chandra","year":"1985","unstructured":"Chandra A., Halpern J., Meyer A. and Parikh R. (1985). Equations between regular terms and an application to process logic. SIAM J. Comput. 14(4): 935\u2013942","journal-title":"SIAM J. Comput."},{"key":"62_CR25","volume-title":"Executing Temporal Logic Programs","author":"B. Moszkowski","year":"1986","unstructured":"Moszkowski B. (1986). Executing Temporal Logic Programs. Cambridge University Press, Cambridge"},{"key":"62_CR26","volume-title":"Modelling and Analysis of Hybrid Systems","author":"Z. Duan","year":"2005","unstructured":"Duan Z. (2005). Modelling and Analysis of Hybrid Systems. Science Press, Beijing"},{"issue":"1-3","key":"62_CR27","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/S0303-2647(99)00087-8","volume":"55","author":"Z. Duan","year":"2000","unstructured":"Duan Z., Holcombe M. and Bell A. (2000). A logic for biosystems. Biosystems 55(1-3): 93\u2013105","journal-title":"Biosystems"},{"key":"62_CR28","doi-asserted-by":"crossref","unstructured":"Paech, B.: Gentzen-systems for propositional temporal logics. In: Borger, E., Kleine Buning, H., Richter, M.M. (eds.) Proceedings of the 2nd workshop on computer science logic, Duisburg (FRG), vol. 385, pp. 240\u2013253. Springer, Heidelberg (1988)","DOI":"10.1007\/BFb0026305"},{"key":"62_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE symposium on foundations of computer science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"62_CR30","doi-asserted-by":"crossref","unstructured":"Tian, C., Duan, Z.: Model Checking Propositional Projection Temporal Logic Based on SPIN, ICFEM 2007, LNCS4789, pp. 246-265, Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-76650-6_15"},{"key":"62_CR31","doi-asserted-by":"crossref","unstructured":"Kr\u00f6ger, F.: Temporal Logic of Programs. EATCS Monographs on Theoretical Computer Science, vol. 8. Springer, Heidelberg (1987)","DOI":"10.1007\/978-3-642-71549-5_5"},{"key":"62_CR32","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P.L. Wolper","year":"1983","unstructured":"Wolper P.L. (1983). Temporal logic can be more expressive. Inf. Control 56: 72\u201399","journal-title":"Inf. Control"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-007-0062-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-007-0062-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-007-0062-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T09:41:54Z","timestamp":1558690914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-007-0062-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11,20]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,2]]}},"alternative-id":["62"],"URL":"https:\/\/doi.org\/10.1007\/s00236-007-0062-z","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,11,20]]}}}