{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T20:47:08Z","timestamp":1775249228908,"version":"3.50.1"},"reference-count":34,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":3791,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Computer and System Sciences"],"published-print":{"date-parts":[[2003,3]]},"DOI":"10.1016\/s0022-0000(03)00005-9","type":"journal-article","created":{"date-parts":[[2003,4,30]],"date-time":"2003-04-30T23:27:29Z","timestamp":1051745249000},"page":"393-426","source":"Crossref","is-referenced-by-count":30,"title":["The complexity of the temporal logic with \u201cuntil\u201d over general linear time"],"prefix":"10.1016","volume":"66","author":[{"given":"M.","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0022-0000(03)00005-9_BIB1","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, A. Pnueli, A really abstract concurrent model and its temporal logic, in: Proceedings of the Thirteenth ACM Symposium on the Principles of Programming Languages, St. Petersberg Beach, FL, January 1986, ACM, New York.","DOI":"10.1145\/512644.512660"},{"issue":"2","key":"10.1016\/S0022-0000(03)00005-9_BIB2","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1305\/ndjfl\/1093870149","article-title":"Axioms for tense logic I","volume":"23","author":"Burgess","year":"1982","journal-title":"Notre Dame J. Formal Logic"},{"issue":"2","key":"10.1016\/S0022-0000(03)00005-9_BIB3","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1305\/ndjfl\/1093870820","article-title":"The decision problem for linear temporal logic","volume":"26","author":"Burgess","year":"1985","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB4","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, Temporal and modal logic, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Vol. B, Elsevier, Amsterdam, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB5","doi-asserted-by":"crossref","unstructured":"D. Gabbay, I. Hodkinson, M. Reynolds, Temporal Logic: Mathematical Foundations and Computational Aspects, Vol. 1, Oxford University Press, Oxford, 1994.","DOI":"10.1007\/BFb0013976"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB6","series-title":"Logic Colloquium \u201990, Proceedings ASL European Meeting 1990, Helsinki","first-page":"89","article-title":"Temporal expressive completeness in the presence of gaps","volume":"Vol. 2","author":"Gabbay","year":"1993"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB7","doi-asserted-by":"crossref","unstructured":"D.M. Gabbay, A. Pnueli, S. Shelah, J. Stavi, On the temporal analysis of fairness, in: Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, 1980, pp. 163\u2013173.","DOI":"10.1145\/567446.567462"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB8","first-page":"5","article-title":"Elementary properties of ordered abelian groups","volume":"3","author":"Gurevich","year":"1964","journal-title":"Algebra and Logic"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB9","series-title":"Logic at Work. Essays Dedicated to the Memory of Helena Rasiowa","first-page":"158","article-title":"Mosaics and step-by-step. Remarks on \u201cA modal logic of relations\u201d","volume":"Vol. 24","author":"Hirsch","year":"1999"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB10","series-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft","year":"1979"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB11","unstructured":"H. Kamp, Tense logic and the theory of linear order, Ph.D. Thesis, University of California, Los Angeles, 1968."},{"key":"10.1016\/S0022-0000(03)00005-9_BIB12","doi-asserted-by":"crossref","unstructured":"Y. Kesten, Z. Manna, A. Pnueli, Temporal verification of simulation and refinement, in: A Decade of Concurrency: Reflections and Perspective: REX School\/Symposium, Noordwijkerhout, the Netherlands, June 1\u20134, 1993, Springer, Berlin, 1994, pp. 273\u2013346.","DOI":"10.1007\/3-540-58043-3_22"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB13","doi-asserted-by":"crossref","first-page":"109","DOI":"10.4064\/fm-59-1-109-116","article-title":"On the elementary theory of linear order","volume":"59","author":"L\u00e4uchli","year":"1966","journal-title":"Fund. Math."},{"key":"10.1016\/S0022-0000(03)00005-9_BIB14","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of International Conference, TABLEAUX 2000, Saint Andrews, Scotland, July 2000","first-page":"324","article-title":"The mosaic method for temporal logics","volume":"Vol. 1847","author":"Marx","year":"2000"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB15","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","article-title":"Testing and generating infinite sequences by finite automata","volume":"9","author":"McNaughton","year":"1966","journal-title":"Informa. and Control"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB16","doi-asserted-by":"crossref","unstructured":"A.R. Meyer, Weak monadic second order theory of successor is not elementary-recursive, in: Proceedings, Logic Colloquium, Springer Lecture Notes in Mathematics, Vol. 453, Springer, Berlin, 1975, pp. 132\u2013154.","DOI":"10.1007\/BFb0064872"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB17","unstructured":"I. N\u00e9meti, Free algebras and decidability in algebraic logic, Ph.D. Thesis, Hungarian Academy of Sciences, Budapest, 1986 (in Hungarian)."},{"key":"10.1016\/S0022-0000(03)00005-9_BIB18","series-title":"Logic Colloquium \u201992","first-page":"171","article-title":"Decidable version of first order logic and cylindric-relativized set algebras","author":"N\u00e9meti","year":"1995"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB19","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00713542","article-title":"On the size of refutation Kripke models for some linear modal and tense logics","volume":"39","author":"Ono","year":"1980","journal-title":"Studia Logica"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB20","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, in: Proceedings of the Eighteenth IEEE Symposium on Foundations of Computer Science, Providence, RI, 1977, pp. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB21","doi-asserted-by":"crossref","unstructured":"V.R. Pratt, Models of program logics, in: Proceedings 20th IEEE Symposium on Foundations of Computer Science, San Juan, 1979, pp. 115\u2013122.","DOI":"10.1109\/SFCS.1979.24"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB22","series-title":"Time and Modality","author":"Prior","year":"1957"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB23","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Amer. Math. Soc. Trans."},{"key":"10.1016\/S0022-0000(03)00005-9_BIB24","doi-asserted-by":"crossref","first-page":"669","DOI":"10.1093\/logcom\/8.5.669","article-title":"On the decidability of continuous time specification formalisms","volume":"8","author":"Rabinovich","year":"1998","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0022-0000(03)00005-9_BIB25","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BF00370112","article-title":"An axiomatization for Until and Since over the reals without the IRR rule","volume":"51","author":"Reynolds","year":"1992","journal-title":"Studia Logica"},{"issue":"3","key":"10.1016\/S0022-0000(03)00005-9_BIB26","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1305\/ndjfl\/1039700748","article-title":"A decidable temporal logic of parallelism","volume":"38","author":"Reynolds","year":"1997","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB27","unstructured":"M. Reynolds, The complexity of the temporal logic over the reals, submitted. Version available at http:\/\/www.it.murdoch.edu.au\/~mark\/research\/online."},{"key":"10.1016\/S0022-0000(03)00005-9_BIB28","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","article-title":"Relationships between non-deterministic and deterministic tape complexities","volume":"4","author":"Savitch","year":"1970","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0022-0000(03)00005-9_BIB29","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"Complexity of propositional linear temporal logics","volume":"32","author":"Sistla","year":"1985","journal-title":"J. ACM"},{"issue":"2","key":"10.1016\/S0022-0000(03)00005-9_BIB30","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1006\/inco.1993.1006","article-title":"Reasoning in a restricted temporal logic","volume":"102","author":"Sistla","year":"1993","journal-title":"J. Inform. Comput."},{"key":"10.1016\/S0022-0000(03)00005-9_BIB31","unstructured":"L. Stockmeyer, The complexity of decision problems in automata and logic, Ph.D. Thesis, MIT Press, Cambridge, MA, 1974."},{"key":"10.1016\/S0022-0000(03)00005-9_BIB32","doi-asserted-by":"crossref","unstructured":"P. van Emde Boas, Machine models and simulations, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Vol. A, Elsevier, Amsterdam, 1990.","DOI":"10.1016\/B978-0-444-88071-0.50006-0"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB33","doi-asserted-by":"crossref","unstructured":"M. Vardi, L. Stockmeyer, Improved upper and lower bounds for modal logics of programs, in: 17th ACM Symposium on Theory of Computing, Proceedings, ACM, New York, 1985, pp. 240\u2013251.","DOI":"10.1145\/22145.22173"},{"key":"10.1016\/S0022-0000(03)00005-9_BIB34","series-title":"Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa","article-title":"A modal logic of relations","author":"Venema","year":"1999"}],"container-title":["Journal of Computer and System Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000003000059?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000003000059?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,19]],"date-time":"2020-03-19T17:13:57Z","timestamp":1584638037000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0022000003000059"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["S0022000003000059"],"URL":"https:\/\/doi.org\/10.1016\/s0022-0000(03)00005-9","relation":{},"ISSN":["0022-0000"],"issn-type":[{"value":"0022-0000","type":"print"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}