{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:42:08Z","timestamp":1777596128077,"version":"3.51.4"},"reference-count":28,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2009,2]]},"abstract":"<jats:p>This paper investigates the complexity of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Propositional Projection Temporal Logic (PPTL) is first extended to include <jats:italic>projection star<\/jats:italic>. Then, by reducing the emptiness problem of star-free expressions to the problem of the satisfiability of PPTL* formulas, the lower bound of the complexity for the satisfiability of PPTL* formulas is proved to be non-elementary. Then, to prove the decidability of PPTL*, the normal form, normal form graph (NFG) and labelled normal form graph (LNFG) for PPTL* are defined. Also, algorithms for transforming a formula to its normal form and LNFG are presented. Finally, a decision algorithm for checking the satisfiability of PPTL* formulas is formalised using LNFGs.<\/jats:p>","DOI":"10.1017\/s096012950800738x","type":"journal-article","created":{"date-parts":[[2009,2,20]],"date-time":"2009-02-20T20:49:19Z","timestamp":1235162959000},"page":"73-100","source":"Crossref","is-referenced-by-count":30,"title":["Complexity of propositional projection temporal logic with star"],"prefix":"10.1017","volume":"19","author":[{"given":"CONG","family":"TIAN","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ZHENHUA","family":"DUAN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,2,1]]},"reference":[{"key":"S096012950800738X_ref23","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"S096012950800738X_ref22","unstructured":"Stockmeyer L. (1974) The Complexity of Decision Problems in Automata Theory and Logic, Ph. D. thesis, MIT (available as Project MAC Technical Report 133)."},{"key":"S096012950800738X_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39910-0_22"},{"key":"S096012950800738X_ref19","first-page":"238","volume-title":"Engineering of Complex Computer Systems","author":"Moszkowski","year":"1995"},{"key":"S096012950800738X_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"S096012950800738X_ref12","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"S096012950800738X_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-007-0062-z"},{"key":"S096012950800738X_ref7","first-page":"333","article-title":"Projection in temporal logic programming","volume":"822","author":"Duan","year":"1994","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S096012950800738X_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72504-6_47"},{"key":"S096012950800738X_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/BF02944904"},{"key":"S096012950800738X_ref4","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Duan","year":"2006"},{"key":"S096012950800738X_ref21","unstructured":"Rosner R. and Pnueli A. (1986) A choppy logic. In: Proceedings, Symposium on Logic in Computer Science, IEEE Computer Society 306\u2013314."},{"key":"S096012950800738X_ref3","first-page":"932","article-title":"Equations between Regular Terms and an Application to Process Logic","volume":"14","author":"Chandra","year":"1985","journal-title":"SIAM J. Computing"},{"key":"S096012950800738X_ref2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.2.195"},{"key":"S096012950800738X_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/800057.808665"},{"key":"S096012950800738X_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2006.12.540"},{"key":"S096012950800738X_ref18","unstructured":"Moszkowski B. (1983) Reasoning about digital circuits, Ph. D. Thesis, Department of Computer Science, Stanford University."},{"key":"S096012950800738X_ref14","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19630090502"},{"key":"S096012950800738X_ref10","doi-asserted-by":"crossref","unstructured":"Dutertre B. (1995) Complete proof systems for first order interval temporal logic. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society 36\u201343.","DOI":"10.1109\/LICS.1995.523242"},{"key":"S096012950800738X_ref28","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","article-title":"A calculus of duration","volume":"40","author":"Zhou","year":"1991","journal-title":"Information Processing Letters"},{"key":"S096012950800738X_ref13","first-page":"40","article-title":"A combination of clausal and non-clausal temporal logic programs","volume":"897","author":"Kono","year":"1993","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S096012950800738X_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90003-4"},{"key":"S096012950800738X_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76650-6_15"},{"key":"S096012950800738X_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.001"},{"key":"S096012950800738X_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"},{"key":"S096012950800738X_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(03)00201-4"},{"key":"S096012950800738X_ref25","unstructured":"Tian C. and Duan Z. (2008) Propositional Projection Temporal Logic, B\u00fcchi Automata and \u03c9-Regular Expressions. In: Proceedings, Theory and Applications of Models of Computation 2008. 4978 47\u201358."},{"key":"S096012950800738X_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2007.05.036"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012950800738X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,3]],"date-time":"2019-04-03T20:19:57Z","timestamp":1554322797000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012950800738X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["S096012950800738X"],"URL":"https:\/\/doi.org\/10.1017\/s096012950800738x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2]]}}}