{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:33:40Z","timestamp":1773653620675,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540424970","type":"print"},{"value":"9783540446859","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44685-0_35","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:16:21Z","timestamp":1186740981000},"page":"519-535","source":"Crossref","is-referenced-by-count":29,"title":["Extended Temporal Logic Revisited"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,22]]},"reference":[{"key":"35_CR1","unstructured":"R. Armoni, L. Fix, A. Flaisher, R. Gerth, T. Kanza, A. Landver, S. Mador Haim, A. Tiemeyer, M.Y. Vardi, and Y. Zber. The ForSpec compiler. Submitted, 2001."},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"R. Armoni, L. Fix, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador Haim, A. Tiemeyer, E. Singerman, and M.Y. Vardi. The ForSpec temporal logic: A new temporal property-specification logic. Submitted, 2001.","DOI":"10.1007\/3-540-46002-0_21"},{"key":"35_CR3","series-title":"Lect Notes Comput Sci","first-page":"62","volume-title":"Temporal Logic in Specification","author":"B. Banieqbal","year":"1987","unstructured":"B. Banieqbal and H. Barringer. Temporal logic with fixed points. In Temporal Logic in Specification, LNCS 398, 62\u201374. Springer-Verlag, 1987."},{"key":"35_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/3-540-58179-0_53","volume-title":"6th CAV","author":"I. Beer","year":"1994","unstructured":"I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In 6th CAV, LNCS 818, 182\u2013193, Springer-Verlag, 1994."},{"key":"35_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"10th CAV","author":"I. Beer","year":"1998","unstructured":"I. Beer, S. Ben-David, and A. Landver. On-the-fly model checking of RCTL formulas. In 10th CAV, LNCS 1427, 184\u2013194. Springer-Verlag, 1998."},{"issue":"3","key":"35_CR6","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF01371727","volume":"26","author":"J.C. Birget","year":"1993","unstructured":"J.C. Birget. State-complexity of finite-state devices, state compressibility and incompressibility. Mathematical Systems Theory, 26(3):237\u2013269, 1993.","journal-title":"Mathematical Systems Theory"},{"key":"35_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/3-540-15670-4_2","volume-title":"Seminar in Concurrency","author":"H. Barringer","year":"1985","unstructured":"H. Barringer and R. Kuiper. Hierarchical development of concurrent systems in a framework. In Seminar in Concurrency, LNCS 197, 35\u201361. Springer-Verlag, 1985."},{"key":"35_CR8","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/0304-3975(80)90069-9","volume":"10","author":"J.A. Brzozowski","year":"1980","unstructured":"J.A. Brzozowski and E. Leiss. Finite automata and sequential networks. TCS, 10:19\u201335, 1980.","journal-title":"TCS"},{"issue":"5","key":"35_CR9","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1093\/logcom\/2.5.605","volume":"2","author":"E.M. Clarke","year":"1992","unstructured":"E.M. Clarke, O. Grumberg, and R.P. Kurshan. A synthesis of two approaches for verifying finite state concurrent systes. Logic and Computation, 2(5):605\u2013618, 1992.","journal-title":"Logic and Computation"},{"key":"35_CR10","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the Association for Computing Machinery, 28(1):114\u2013133, January 1981.","DOI":"10.1145\/322234.322243"},{"issue":"3","key":"35_CR12","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/176584.176587","volume":"41","author":"D. Drusinsky","year":"1994","unstructured":"D. Drusinsky and D. Harel. On the power of bounded concurrency I: Finite automata. Journal of the ACM, 41(3):517\u2013539, 1994.","journal-title":"Journal of the ACM"},{"key":"35_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BFb0030596","volume-title":"TAPSOFT","author":"E.A. Emerson","year":"1997","unstructured":"E.A. Emerson and R.J. Trefler. Generalized quantitative temporal reasoning: An automata theoretic approach. In TAPSOFT, LNCS 1214, 189\u2013200. Springer, 1997."},{"key":"35_CR14","series-title":"Lect Notes Comput Sci","volume-title":"TACAS","author":"B. Finkbeiner","year":"2001","unstructured":"B. Finkbeiner. Symbolic refinement checking with nondeterministic BDDs. In TACAS, LNCS 2031. Springer-Verlag, 2001."},{"key":"35_CR15","unstructured":"N. Francez. Program verification. Int. Computer Science. Addison-Weflay, 1992."},{"key":"35_CR16","series-title":"Lect Notes Comput Sci","first-page":"407","volume-title":"Temporal Logic in Specification","author":"D. Gabbay","year":"1987","unstructured":"D. Gabbay. The declarative past and imperative future. In Temporal Logic in Specification, LNCS 398, 407\u2013448. Springer-Verlag, 1987."},{"key":"35_CR17","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/S0304-3975(96)00119-3","volume":"143","author":"N. Globerman","year":"1996","unstructured":"N. Globerman and D. Harel. Complexity results for two-way and multipebble automata and their logics. TCS, 143:161\u2013184, 1996.","journal-title":"TCS"},{"issue":"1\u20133","key":"35_CR18","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J.G. Henriksen","year":"1999","unstructured":"J.G. Henriksen and P.S. Thiagarajan. Dynamic linear time temporal logic. Annals of Pure and Applied Logic, 96(1\u20133):187\u2013207, 1999.","journal-title":"Annals of Pure and Applied Logic"},{"key":"35_CR19","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. Weak alternating automata are not that weak. In 5th ISTCS, 147\u2013158. IEEE Computer Society Press, 1997.","DOI":"10.1109\/ISTCS.1997.595167"},{"key":"35_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/3-540-44612-5_45","volume-title":"25th MFCS","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman and M.Y. Vardi. \u03bc-calculus synthesis. In 25th MFCS, LNCS 1893, 497\u2013507. Springer-Verlag, 2000."},{"key":"35_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logics of Programs, LNCS 193, 196\u2013218, Springer-Verlag, 1985."},{"key":"35_CR22","doi-asserted-by":"crossref","unstructured":"A. R. Meyer. Weak monadic second order theory of successor is not elementary recursive. In Proc. Logic Colloquium, Vol. 453 of Lecture Notes in Mathematics, 132\u2013154. Springer-Verlag, 1975.","DOI":"10.1007\/BFb0064872"},{"key":"35_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, January 1992."},{"key":"35_CR24","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D.E. Muller","year":"1985","unstructured":"D.E. Muller and P.E. Schupp. The theory of ends, pushdown automata, and second-order logic. TCS, 37:51\u201375, 1985.","journal-title":"TCS"},{"key":"35_CR25","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. TCS, 54:267\u2013276, 1987.","journal-title":"TCS"},{"key":"35_CR26","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D.E. Muller","year":"1995","unstructured":"D.E. Muller and P.E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. TCS, 141:69\u2013107, 1995.","journal-title":"TCS"},{"key":"35_CR27","series-title":"Lect Notes Comput Sci","volume-title":"13th IC ALP","author":"D.E. Muller","year":"1986","unstructured":"D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In 13th IC ALP, LNCS 226, 1986."},{"key":"35_CR28","volume-title":"M.Sc. Thesis","author":"N. Piterman","year":"2000","unstructured":"N. Piterman. Extending temporal logic with \u03c9-automata. M.Sc. Thesis, The Weizmann Institute of Science, Israel, 2000, http:\/\/www.wisdom.weizmann.ac.il\/home\/nirp\/public_html\/publications\/msc_thesis.ps."},{"key":"35_CR29","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. The temporal semantics of concurrent programs. TCS, 13:45\u201360, 1981.","journal-title":"TCS"},{"key":"35_CR30","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 123\u2013144. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"35_CR31","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal ACM, 32:733\u2013749, 1985.","journal-title":"Journal ACM"},{"key":"35_CR32","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for B\u00fcchi automata with applications to temporal logic. TCS, 49:217\u2013237, 1987.","journal-title":"TCS"},{"key":"35_CR33","first-page":"261","volume":"48","author":"W. Thomas","year":"1981","unstructured":"W. Thomas. A combinatorial approach to the theory of \u03c9-automata. Information and Computation, 48:261\u2013283, 1981.","journal-title":"Information and Computation"},{"key":"35_CR34","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. A temporal fixpoint calculus. In 15th POPL, pages 250\u2013259, 1988.","DOI":"10.1145\/73560.73582"},{"key":"35_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M.Y. Vardi","year":"1996","unstructured":"M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, LNCS 1043, 238\u2013266, 1996."},{"key":"35_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"25th ICALP","author":"M.Y. Vardi","year":"1998","unstructured":"M.Y. Vardi. Reasoning about the past with two-way automata. In 25th ICALP LNCS 1443, 628\u2013641. Springer-Verlag, 1998."},{"key":"35_CR37","series-title":"Lect Notes Comput Sci","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":"M.Y. Vardi and P. Wolper. Yet another process logic. In Logics of Programs, LNCS 164, 501\u2013512. Springer-Verlag, 1984."},{"issue":"1","key":"35_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"},{"issue":"1\u20132","key":"35_CR39","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1\u20132):72\u201399, 1983.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2001 \u2014 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44685-0_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T07:24:48Z","timestamp":1737357888000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44685-0_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540424970","9783540446859"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-44685-0_35","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}