{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:13:26Z","timestamp":1725491606763},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540752905"},{"type":"electronic","value":"9783540752929"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75292-9_32","type":"book-chapter","created":{"date-parts":[[2007,9,11]],"date-time":"2007-09-11T06:43:07Z","timestamp":1189492987000},"page":"467-481","source":"Crossref","is-referenced-by-count":3,"title":["On the Expressive Power of QLTL"],"prefix":"10.1007","author":[{"given":"Zhilin","family":"Wu","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"32_CR1","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: On branching versus linear time temporal logic. Journal of the ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"Journal of the ACM"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-48683-6_22","volume-title":"Computer Aided Verification","author":"K. Etessami","year":"1999","unstructured":"Etessami, K.: Stutter-invariant languages, \u03c9-automata, and temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 236\u2013248. Springer, Heidelberg (1999)"},{"key":"32_CR3","first-page":"127","volume":"4","author":"T. French","year":"2003","unstructured":"French, T., Reynolds, M.: A Sound and Complete Proof System for QPTL. Advances in Modal Logic\u00a04, 127\u2013147 (2003)","journal-title":"Advances in Modal Logic"},{"key":"32_CR4","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/567446.567462","volume-title":"POPL 1980","author":"D.M. Gabbay","year":"1980","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the Temporal Analysis of Fairness. In: POPL 1980. Conference Record of the 7th ACM Symposium on Principles of Programming Languages, pp. 163\u2013173. ACM Press, New York (1980)"},{"key":"32_CR5","unstructured":"Kamp, H.W.: Tense Logic and the Theory of Linear Order. PhD thesis, UCLA, Los Angeles, California, USA (1968)"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: A Complete Proof Systems for QPTL. In: LICS, pp. 2\u201312 (1995)","DOI":"10.1109\/LICS.1995.523239"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/BFb0030294","volume-title":"Mathematical Foundations of Computer Science 1984","author":"D. Perrin","year":"1984","unstructured":"Perrin, D.: Recent results on automata and infinite words. In: Chytil, M.P., Koubek, V. (eds.) Mathematical Foundations of Computer Science 1984. LNCS, vol.\u00a0176, pp. 134\u2013148. Springer, Heidelberg (1984)"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th FOCS, pp. 46\u201351 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"32_CR9","volume-title":"Time and Modality","author":"A.N. Prior","year":"1957","unstructured":"Prior, A.N.: Time and Modality. Clarendon Press, Oxford (1957)"},{"key":"32_CR10","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D. Peled","year":"1997","unstructured":"Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters\u00a063, 243\u2013246 (1997)","journal-title":"Information Processing Letters"},{"key":"32_CR11","unstructured":"Sistla, A.P.: Theoretical issues in the design and verification of distributed systems. PHD thesis, Harvard University (1983)"},{"key":"32_CR12","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. TCS\u00a049, 217\u2013237 (1987)","journal-title":"TCS"},{"key":"32_CR13","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1993.1006","volume":"102","author":"A.P. Sistla","year":"1993","unstructured":"Sistla, A.P., Zuck, L.D.: Reasoning in a restricted temporal logic. Information and Computation\u00a0102, 167\u2013195 (1993)","journal-title":"Information and Computation"},{"key":"32_CR14","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1016\/S0019-9958(79)90629-6","volume":"42","author":"W. Thomas","year":"1979","unstructured":"Thomas, W.: Star-free regular sets of \u03c9-sequences. Inform. and Control\u00a042, 148\u2013156 (1979)","journal-title":"Inform. and Control"},{"key":"32_CR15","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/S0019-9958(81)90663-X","volume":"48","author":"W. Thomas","year":"1981","unstructured":"Thomas, W.: A combinatorial approach to the theory of \u03c9-automata. Inform. and Control\u00a048, 261\u2013283 (1981)","journal-title":"Inform. and Control"},{"key":"32_CR16","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on Infinite Objects. In: Van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 133\u2013191. Elsevier Science Publishers, Amsterdam (1990)"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: POPL\u201988. Proceedings of the 15th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 250\u2013259 (1988)","DOI":"10.1145\/73560.73582"},{"key":"32_CR18","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. Inform. and Control\u00a056, 72\u201399 (1983)","journal-title":"Inform. and Control"},{"key":"32_CR19","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.) Logics of Programs. LNCS, vol.\u00a0164, pp. 501\u2013512. Springer, Heidelberg (1984)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75292-9_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:59:01Z","timestamp":1619506741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75292-9_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540752905","9783540752929"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75292-9_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}