{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:13:04Z","timestamp":1761610384647,"version":"build-2065373602"},"reference-count":23,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3984,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1016\/s1571-0661(05)80366-4","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T08:37:08Z","timestamp":1117010228000},"page":"87-104","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":2,"title":["Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past"],"prefix":"10.1016","volume":"68","author":[{"given":"Nicolas","family":"Markey","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80366-4_BIB1","first-page":"164","article-title":"A really temporal logic","author":"Alur","year":"1989"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB2","first-page":"35","article-title":"Real-time logics: Complexity and expressiveness","author":"Alur","year":"1993"},{"year":"1999","series-title":"\u201cModel Checking,\u201d","author":"Clarke","key":"10.1016\/S1571-0661(05)80366-4_BIB3"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB4","first-page":"84","article-title":"The complexity of propositional linear temporal logics in simple cases","volume":"174","author":"Demri","year":"2002"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB5","first-page":"995","article-title":"Temporal and modal logic. in:","volume":"Vol. B","author":"Emerson","year":"1990"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB6","first-page":"228","article-title":"First order logic with two variables and unary temporal logic","author":"Etessami","year":"1997"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB7","first-page":"409","article-title":"The declarative past and imperative future: Executable temporal logic for interactive systems","volume":"398","author":"Gabbay","year":"1989"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB8","series-title":"Proc. 7th ACM Symp. Principles of Programming Languages (POPL'80), Las Vegas, NV, USA, Jan. 1980","first-page":"163","article-title":"On the temporal analysis of fairness","author":"Gabbay","year":"1980"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB9","series-title":"Annals of Discrete Mathematics 24","first-page":"51","article-title":"Recurring dominos: Making the highly undecidable highly understandable","author":"Harel","year":"1985"},{"year":"1968","series-title":"\u201cTense Logic and the Theory of Linear Order,\u201d Ph.D. thesis. UCLA, Los Angeles, CA, USA","author":"Kamp","key":"10.1016\/S1571-0661(05)80366-4_BIB10"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB11","first-page":"97","article-title":"A decision algorithm for full propositional temporal logic","volume":"697","author":"Kesten","year":"1993"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB12","first-page":"255","article-title":"Specifying real-time properties with metric temporal logic","volume":"2","author":"Koymans","year":"1990"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB13","series-title":"Proc. 10th IEEE Symp. Logic in Computer Science (LICS'95), San Diego, CA, USA, June 1995","first-page":"25","article-title":"Once and for all","author":"Kupferman","year":"1995"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB14","series-title":"Proc. 17th IEEE Symp. Logic in Computer Science (LICS'2002), Copenhagen, Denmark, July 2002","first-page":"383","article-title":"Temporal logic with forgettable past","author":"Laroussinie","year":"2002"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB15","first-page":"303","article-title":"A hierarchy of temporal logics with past","volume":"148","author":"Laroussinie","year":"1995"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB16","first-page":"196","article-title":"The glory of the past","volume":"193","author":"Lichtenstein","year":"1985"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB17","first-page":"97","article-title":"Completing the temporal picture","volume":"83","author":"Manna","year":"1991"},{"year":"1992","series-title":"\u201cThe Temporal Logic of Reactive and Concurrent Systems: Specification,\u201d Springer","author":"Manna","key":"10.1016\/S1571-0661(05)80366-4_BIB18"},{"year":"1995","series-title":"\u201cTemporal Verification of Reactive Systems: Safety,\u201d Springer","author":"Manna","key":"10.1016\/S1571-0661(05)80366-4_BIB19"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB20","series-title":"Proc. 18th IEEE Symp. Foundations of Computer Science (FOCS'77), Providence, RI, USA, Oct.-Nov. 1977","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB21","series-title":"Fundamenta Informaticae 17","first-page":"271","article-title":"An automata-theoretic decision procedure for propositional temporal logic with Since and Until","author":"Ramakrishna","year":"1992"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB22","series-title":"Journal of the ACM 32","first-page":"733","article-title":"The complexity of propositional linear temporal logics","author":"Sistla","year":"1985"},{"key":"10.1016\/S1571-0661(05)80366-4_BIB23","series-title":"Information and Computation 115","first-page":"1","article-title":"Reasoning about infinite computations","author":"Vardi","year":"1994"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105803664?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105803664?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:07:10Z","timestamp":1761610030000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105803664"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["S1571066105803664"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80366-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)80366-4","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}