{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:25:11Z","timestamp":1761596711722},"reference-count":45,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1996,10,1]],"date-time":"1996-10-01T00:00:00Z","timestamp":844128000000},"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":6133,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1996,10]]},"DOI":"10.1016\/0304-3975(95)00254-5","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T21:06:05Z","timestamp":1027631165000},"page":"1-47","source":"Crossref","is-referenced-by-count":10,"title":["Interval logics and their decision procedures"],"prefix":"10.1016","volume":"166","author":[{"given":"Y.S","family":"Ramakrishna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.M","family":"Melliar-Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.E","family":"Moser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.K","family":"Dillon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G","family":"Kutty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(95)00254-5_BIB1","series-title":"Proc. Conf. Automated Deduction","first-page":"218","article-title":"Propositional temporal interval logic is PSPACE-complete","author":"Aaby","year":"1988"},{"key":"10.1016\/0304-3975(95)00254-5_BIB2_1","series-title":"CONCUR'90, Proc. Conf. Concurrency Theory","first-page":"57","article-title":"An axiomatization of Lamport's Temporal Logic of Actions","volume":"Vol. 458","author":"Abadi","year":"1990"},{"key":"10.1016\/0304-3975(95)00254-5_BIB2_2","series-title":"CONCUR'90, Proc. Conf. Concurrency Theory","article-title":"An axiomatization of Lamport's Temporal Logic of Actions","author":"Abadi","year":"1990"},{"key":"10.1016\/0304-3975(95)00254-5_BIB3","doi-asserted-by":"crossref","first-page":"832","DOI":"10.1145\/182.358434","article-title":"Maintaining knowledge about temporal intervals","volume":"26","author":"Allen","year":"1983","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(95)00254-5_BIB4","first-page":"181","article-title":"Defining liveness","volume":"21","author":"Alpern","year":"1985"},{"key":"10.1016\/0304-3975(95)00254-5_BIB5","first-page":"117","article-title":"Recognizing safety and liveness","volume":"2","author":"Alpern","year":"1987","journal-title":"Discrete Comput."},{"key":"10.1016\/0304-3975(95)00254-5_BIB6","series-title":"Logic, Methodology and Philosophy of Science, Proc. Congr.","first-page":"1","article-title":"On a decision method in restricted second-order arithmetic","author":"B\u00fcchi","year":"1990"},{"key":"10.1016\/0304-3975(95)00254-5_BIB7","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","article-title":"Theories of automata on \u03c9-tapes: A simplified approach","volume":"8","author":"Choueka","year":"1974","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/0304-3975(95)00254-5_BIB8","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1145\/192218.192226","article-title":"A graphical interval logic for specifying concurrent systems","volume":"3","author":"Dillon","year":"1994","journal-title":"ACM Trans. Software Eng. Methodology"},{"key":"10.1016\/0304-3975(95)00254-5_BIB9","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1006\/jvlc.1994.1004","article-title":"Visual specifications for temporal reasoning","volume":"1","author":"Dillon","year":"1994","journal-title":"J. Visual Lang. Comput."},{"key":"10.1016\/0304-3975(95)00254-5_BIB10","first-page":"789","article-title":"Temporal and modal logic","author":"Emerson","year":"1990"},{"key":"10.1016\/0304-3975(95)00254-5_BIB11","series-title":"Proc. 9th ACM Symp. Theory of Comput.","first-page":"286","article-title":"Propositional modal logic of programs","author":"Fischer","year":"1977"},{"key":"10.1016\/0304-3975(95)00254-5_BIB12","article-title":"Nicht-elementare untere schranken in der automaten-theorie","author":"F\u00fcer","year":"1978"},{"key":"10.1016\/0304-3975(95)00254-5_BIB13","series-title":"Proc. 2nd Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems","first-page":"1","article-title":"ISL: an interval logic for the specification of real-time programs","volume":"Vol. 571","author":"Goswami","year":"1992"},{"key":"10.1016\/0304-3975(95)00254-5_BIB14","series-title":"Proc. 10th Int. Colloq. Automata, Languages and Programming","first-page":"278","article-title":"A hardware semantics based on temporal intervals","author":"Halpern","year":"1983"},{"key":"10.1016\/0304-3975(95)00254-5_BIB15","doi-asserted-by":"crossref","first-page":"935","DOI":"10.1145\/115234.115351","article-title":"A propositional modal logic of time intervals","volume":"38","author":"Halpern","year":"1991","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(95)00254-5_BIB16","series-title":"Proc. 29th IEEE Found. Comput. Sci.","first-page":"328","article-title":"The complexity of tree automata and logics of programs","author":"Emerson","year":"1988"},{"key":"10.1016\/0304-3975(95)00254-5_BIB17","series-title":"Proc. 7th IEEE Logic in Comput. Sci.","first-page":"382","article-title":"Progress measures, immediate determinacy, and a subset construction for tree automata","author":"Klarlund","year":"1992"},{"key":"10.1016\/0304-3975(95)00254-5_BIB18","article-title":"A graphical environment for temporal reasoning","author":"Kutty","year":"1994"},{"key":"10.1016\/0304-3975(95)00254-5_BIB19","first-page":"313","article-title":"Axiomatizations of interval logics","volume":"XXIV","author":"Kutty","year":"1995","journal-title":"Fund. Inf."},{"key":"10.1016\/0304-3975(95)00254-5_BIB20_1","article-title":"The temporal logic of actions","author":"Lamport","year":"1991","journal-title":"Tech. Report 79"},{"key":"10.1016\/0304-3975(95)00254-5_BIB20_2","article-title":"The temporal logic of actions","author":"Lamport","year":"1990","journal-title":"Tech. Rep. 57"},{"key":"10.1016\/0304-3975(95)00254-5_BIB21","series-title":"Proc. Brooklyn Workshop Logic of Programs","first-page":"196","article-title":"The glory of the past","volume":"Vol. 193","author":"Lichtenstein","year":"1985"},{"key":"10.1016\/0304-3975(95)00254-5_BIB22","doi-asserted-by":"crossref","unstructured":"A. Mazurkiewicz, Basic notions of trace theory, in: Proc. REX Workshop on Linear Time, Branching Time and Partial Order in Logics and Models of Concurrency, Lecture Notes in Computer Science, Vol. 354, 285\u2013363.","DOI":"10.1007\/BFb0013025"},{"key":"10.1016\/0304-3975(95)00254-5_BIB23","series-title":"CONCURRENCY 88: Proc. Int. Conf. Concurrency","first-page":"106","article-title":"A graphical representation of interval logic","volume":"Vol. 335","author":"Melliar-Smith","year":"1988"},{"key":"10.1016\/0304-3975(95)00254-5_BIB24","doi-asserted-by":"crossref","first-page":"257","DOI":"10.3233\/FI-1994-2141","article-title":"Soundness and completeness of axiomatizations for temporal logics without next","volume":"XXI","author":"Moser","year":"1994","journal-title":"Fundam. Inform."},{"key":"10.1016\/0304-3975(95)00254-5_BIB25","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","article-title":"On theories with a combinatorial definition of \u201cequivalence\u201d","volume":"43","author":"Newman","year":"1942","journal-title":"Ann. Math."},{"key":"10.1016\/0304-3975(95)00254-5_BIB26","series-title":"proc. CMU Workshop on Logics of Programs","first-page":"403","article-title":"A low-level language for obtaining decision procedures for classes of temporal logics","volume":"Vol. 164","author":"Plaisted","year":"1983"},{"key":"10.1016\/0304-3975(95)00254-5_BIB27","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Trans. AMS"},{"key":"10.1016\/0304-3975(95)00254-5_BIB28","article-title":"Interval logics for temporal specification and verification","author":"Ramakrishna","year":"1993"},{"key":"10.1016\/0304-3975(95)00254-5_BIB29","doi-asserted-by":"crossref","first-page":"387","DOI":"10.3233\/FI-1995-2444","article-title":"On the satisfiability problem for Lamport's propositional temporal logic of actions and some of its extensions","volume":"XXIV","author":"Ramakrishna","year":"1995","journal-title":"Fundam. Inform."},{"key":"10.1016\/0304-3975(95)00254-5_BIB30","series-title":"Proc. 12th Found. Softw. Tech. & Theoret. Comput. Sci.","first-page":"51","article-title":"An automata-theoretic decision procedure for future interval logic","volume":"Vol. 652","author":"Ramakrishna","year":"1992"},{"key":"10.1016\/0304-3975(95)00254-5_BIB31","article-title":"Interval logics and their decision procedures, Part II: a real-time interval logic","volume":"170","author":"Ramakrishna","year":"1996","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(95)00254-5_BIB32","series-title":"Proc. 1st IEEE Logic Comput. Sci.","first-page":"306","article-title":"A choppy logic","author":"Rosner","year":"1986"},{"key":"10.1016\/0304-3975(95)00254-5_BIB33","series-title":"Proc. 29th IEEE Found. Comput. Sci.","first-page":"319","article-title":"On the complexity of omega-automata","author":"Safra","year":"1988"},{"key":"10.1016\/0304-3975(95)00254-5_BIB34","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","article-title":"Relationship between non-deterministic and deterministic tape complexities","volume":"4","author":"Savitch","year":"1970","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/0304-3975(95)00254-5_BIB35","series-title":"Proc. 2nd ACM Principles of Dist. Comput.","first-page":"173","article-title":"An interval logic for higher-level temporal reasoning","author":"Schwartz","year":"1983"},{"key":"10.1016\/0304-3975(95)00254-5_BIB36","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logic","volume":"32","author":"Sistla","year":"1985","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(95)00254-5_BIB37","series-title":"First-Order Logic","author":"Smullyan","year":"1968"},{"key":"10.1016\/0304-3975(95)00254-5_BIB38","article-title":"The complexity of decision problems in automata theory and logic","author":"Stockmeyer","year":"1974"},{"key":"10.1016\/0304-3975(95)00254-5_BIB39","first-page":"133","article-title":"Automata on infinite objects","author":"Thomas","year":"1990"},{"key":"10.1016\/0304-3975(95)00254-5_BIB40","series-title":"Proc. 1st IEEE Logic in Comput. Sci.","first-page":"183","article-title":"An automata-theoretic approach to automatic program verification","author":"Vardi","year":"1986"},{"key":"10.1016\/0304-3975(95)00254-5_BIB41","series-title":"Proc. 1st Int. Conf. Temporal Logic","first-page":"149","article-title":"Completeness through flatness in two-dimensional temporal logic","volume":"Vol. 827","author":"Venema","year":"1994"},{"key":"10.1016\/0304-3975(95)00254-5_BIB42","series-title":"Logique et Anlyse","first-page":"119","article-title":"The tableau method for temporal logic: An overvciew","author":"Wolper","year":"1985"},{"key":"10.1016\/0304-3975(95)00254-5_BIB43","series-title":"Proc. Conf. Temporal Logic in Specification","first-page":"75","article-title":"On the relation of programs and computations to models of temporal logic","volume":"Vol. 398","author":"Wolper","year":"1987"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397595002545?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397595002545?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,2,4]],"date-time":"2020-02-04T15:41:03Z","timestamp":1580830863000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397595002545"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,10]]},"references-count":45,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1996,10]]}},"alternative-id":["0304397595002545"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(95)00254-5","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1996,10]]}}}