{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:37:32Z","timestamp":1759639052647},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540792277"},{"type":"electronic","value":"9783540792284"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79228-4_4","type":"book-chapter","created":{"date-parts":[[2008,4,29]],"date-time":"2008-04-29T05:07:56Z","timestamp":1209445676000},"page":"47-58","source":"Crossref","is-referenced-by-count":11,"title":["Propositional Projection Temporal Logic, B $\\ddot{u}$ chi Automata and \u03c9-Regular Expressions"],"prefix":"10.1007","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":"297","reference":[{"key":"4_CR1","first-page":"46","volume-title":"Proceedings of the 18th IEEE Symposium on Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201367.2 IEEE, New York (1977)"},{"key":"4_CR2","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":"4_CR3","unstructured":"Rosner, R., Pnueli, A.: A choppy logic. In: First Annual IEEE Symposium on Logic In Computer Science. LICS, pp. 306\u2013314 (1986)"},{"key":"4_CR4","unstructured":"Moszkowski, B.: Reasoning about digital circuits. Ph.D Thesis, Department of Computer Science, Stanford University. TRSTAN-CS-83-970 (1983)"},{"key":"4_CR5","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)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/978-3-540-72504-6_46","volume-title":"Theory and Applications of Models of Computation","author":"Z. Duan","year":"2007","unstructured":"Duan, Z., Tian, C.: Decidability of Propositional Projection Temporal Logic with Infinite Models. In: Cai, J.-Y., Cooper, S.B., Zhu, H. (eds.) TAMC 2007. LNCS, vol.\u00a04484, pp. 521\u2013532. Springer, Heidelberg (2007)"},{"key":"4_CR7","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":"4_CR8","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)"},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P.L. Wolper","year":"1983","unstructured":"Wolper, P.L.: Temporal logic can be more expressive. Information and Control\u00a056, 72\u201399 (1983)","journal-title":"Information and Control"},{"issue":"5","key":"4_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"4_CR11","unstructured":"Arden, D.: Delayed-logic and finite-state machines. In: Theory of Computing Machine Design, Univ. of Michigan Press, pp. 1\u201335 (1960)"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/567446.567462","volume-title":"POPL 1980: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"D. Gabbay","year":"1980","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL 1980: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 163\u2013173. ACM Press, New York (1980)"},{"key":"4_CR13","unstructured":"Sistla, A.P.: Theoretical issues in the design and verification of distributed systems. PhD thesis, Harvard University (1983)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1007\/3-540-12896-4_383","volume-title":"Logics of Programs","author":"M.Y. Vardi","year":"1984","unstructured":"Vardi, M.Y., Wolper, P.: Yet another process logic. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol.\u00a0164, pp. 501\u2013512. Springer, Heidelberg (1984)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: POPL 1988, pp. 250\u2013259 (1988)","DOI":"10.1145\/73560.73582"},{"key":"4_CR16","volume-title":"Counter-Free Automata (M.I.T research monograph no.65)","author":"R. McNaughton","year":"1971","unstructured":"McNaughton, R., Papert, S.A.: Counter-Free Automata (M.I.T research monograph no.65). The MIT Press, Cambridge (1971)"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Barringer, H., Kuiper, R., Pnueli, A.: Now You May Compose Temporal Logic Specifications. In: Proc. 16th STOC, pp. 51\u201363 (1984)","DOI":"10.1145\/800057.808665"},{"key":"4_CR18","unstructured":"Barringer, H., Kuiper, R., Pnueli, A.: The Compositional Temporal Approach to CSP-like Language. In: Proc.IFIP Conference, The Role of Abstract Models in Information Processing (January 1985)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/3-540-15648-8_19","volume-title":"A Temporal Approach to Process Modeling, Logics of Programs","author":"V. Nguyen","year":"1985","unstructured":"Nguyen, V., Demers, A., Gries, D., Owicki, S.: Logic of Programs 1985. LNCS, vol.\u00a0193, pp. 237\u2013254. Springer, Heidelberg (1985)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Nguyen, V., Gries, D., Owicki, S.: A Model and Temporal Proof System for Networks of Processes. In: Proc. 12th POPL, pp. 121\u2013131 (1985)","DOI":"10.1145\/318593.318624"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0304-3975(85)90225-7","volume":"38","author":"D. Harel","year":"1985","unstructured":"Harel, D., Peleg, D.: Process Logic with Regular Formulas. Theoretical Computer Science\u00a038, 307\u2013322 (1985)","journal-title":"Theoretical Computer Science"},{"key":"4_CR22","unstructured":"Tian, C., Duan, Z.: Complexity of Propositional Projection Temporal Logic with Star. Technical Report No.25, Institute of computing Theory and Technology, Xidian University, Xian P.R.China (2007)"},{"key":"4_CR23","unstructured":"Arden, D.: Delayed-logic and finite-state machines. In: Theory of Computing Machine Design, pp. 1\u201335. Univ. of Michigan Press (1960)"},{"key":"4_CR24","volume-title":"Communicating and Mobile System: The -Calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile System: The -Calculus. Cambridge University Press, Cambridge (1999)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79228-4_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:14:22Z","timestamp":1619522062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79228-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540792277","9783540792284"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79228-4_4","relation":{},"subject":[]}}