{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:12:04Z","timestamp":1761610324186,"version":"build-2065373602"},"reference-count":32,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"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":6053,"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":[[1997]]},"DOI":"10.1016\/s1571-0661(05)80472-4","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T08:37:08Z","timestamp":1117010228000},"page":"161-184","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Specification in CTL+Past, Verification in CTL"],"prefix":"10.1016","volume":"7","author":[{"given":"F.","family":"Laroussinie","sequence":"first","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Ph.","family":"Schnoebelen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/S1571-0661(05)80472-4_BIB1","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1093\/comjnl\/30.2.134","article-title":"Up and down the temporal way","volume":"30","author":"Barringer","year":"1987","journal-title":"The Computer Journal"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB2","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, Y. Lakhnech, and S. Yovine. Model checking for extended timed temporal logics. In Proc. 4th Int. Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'96), Uppsala, Sweden, Sep. 1996, volume 1135 of Lecture Notes in Computer Science, pages 306-326. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61648-9_48"},{"issue":"2","key":"10.1016\/S1571-0661(05)80472-4_BIB3","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB4","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Gr\u00fcimberg, and D. Long. Verification tools for finite-state concurrent systems. In A Decade of Concurrency, Proc. REX School\/Symp., Noordwijkerhout, NL, June 1993, volume 803 of Lecture Notes in Computer Science, pages 124-175. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58043-3_19"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB5","first-page":"995","article-title":"Temporal and modal logic","author":"Emerson","year":"1990"},{"issue":"1","key":"10.1016\/S1571-0661(05)80472-4_BIB6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","article-title":"Decision procedures and expressiveness in the temporal logic of branching time","volume":"30","author":"Emerson","year":"1985","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB7","doi-asserted-by":"crossref","unstructured":"D. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In Proc. Workshop Temporal Logic in Specification, Altrincham, UK, Apr. 1987, volume 398 of Lecture Notes in Computer Science, pages 409-448. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51803-7_36"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB8","doi-asserted-by":"crossref","unstructured":"D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proc. 7th ACM Symp. Principles of Programming Languages (POPL'80), Las Vegas, Nevada, Jan. 1980, pages 163-173, 1980.","DOI":"10.1145\/567446.567462"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB9","doi-asserted-by":"crossref","unstructured":"T. Hafer and W. Thomas. Computation tree logic CTL\u2217 and path quantifiers in the monadic theory of the binary tree. In Proc. 14th Int. Coll. Automata, Languages, and Programming (ICALP'87), Karlsruhe, FRG, July 1987, volume 267 of Lecture Notes in Computer Science, pages 269-279. Springer-Verlag, 1987.","DOI":"10.1007\/3-540-18088-5_22"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB10","doi-asserted-by":"crossref","unstructured":"R. Hale. Using temporal logic for prototyping: the design of a lift controller. In Proc. Workshop Temporal Logic in Specification, Altrincham, UK, Apr. 1987, volume 398 of Lecture Notes in Computer Science, pages 375-408. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51803-7_35"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB11","doi-asserted-by":"crossref","unstructured":"Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli. A decision algorithm for full prepositional temporal logic. In Proc. 5th Int. Conf. Computer-Aided Verification (CAV'93), Elounda, Greece, June 1993, volume 697 of Lecture Notes in Computer Science, pages 97-109. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_9"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB12","doi-asserted-by":"crossref","unstructured":"R. Koymans, J. Vytopil, and W. P. de Roever. Real-time programming and asynchronous message passing. In Proc. 2nd ACM Symp. Principles of Distributed Computing (PODC'83), Montreal, Canada, Aug. 1983, pages 187-197, 1983.","DOI":"10.1145\/800221.806721"},{"issue":"4","key":"10.1016\/S1571-0661(05)80472-4_BIB13","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1093\/logcom\/6.4.523","article-title":"Buy one, get one free!!!","volume":"6","author":"Kupferman","year":"1996","journal-title":"J. Logic and Computation"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB14","unstructured":"O. Kupferman and A. Pnueli. Once and for all. In Proc. 10th IEEE Symp. Logic in Computer Science (LICS'95), San Diego, CA, June 1995, pages 25-35, 1995."},{"issue":"1","key":"10.1016\/S1571-0661(05)80472-4_BIB15","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/0304-3975(94)00204-V","article-title":"Translations between modal logics of reactive systems","volume":"140","author":"Laroussinie","year":"1995","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/S1571-0661(05)80472-4_BIB16","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0304-3975(95)00035-U","article-title":"A hierarchy of temporal logics with past","volume":"148","author":"Laroussinie","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB17","series-title":"Actes des 2e Journes Toulousaines sur la Formalisation des Activits Concurrentes (FAC'96), Toulouse, France, Feb. 1996","first-page":"17","article-title":"Translations for model-checking temporal logic with past","author":"Laroussinie","year":"1996"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB18","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Proc. Logics of Programs Workshop, Brooklyn, NY, June 1985, volume 193 of Lecture Notes in Computer Science, pages 196-218. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB19","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The anchored version of the temporal framework. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Proc. REX School\/Workshop, Noordwijkerhout, NL, May-June 1988, volume 354 of Lecture Notes in Computer Science, pages 201\u2013284. Springer-Verlag, 1989.","DOI":"10.1007\/BFb0013024"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB20","series-title":"volume I: Specification","article-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Manna","year":"1992"},{"year":"1993","series-title":"Symbolic Model Checking","author":"McMillan","key":"10.1016\/S1571-0661(05)80472-4_BIB21"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB22","unstructured":"K.L. McMillan. The SMV system, symbolic model checking - an approach. Technical Report CMU-CS-92-131, Carnegie Mellon University, 1992."},{"issue":"4","key":"10.1016\/S1571-0661(05)80472-4_BIB23","doi-asserted-by":"crossref","first-page":"257","DOI":"10.3233\/FI-1994-2141","article-title":"Completeness and soundness of axiomatizations for temporal logics without next","volume":"21","author":"Moser","year":"1994","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB24","doi-asserted-by":"crossref","unstructured":"S. S. Pinter and P. Wolper. A temporal logic for reasoning about partially ordered computations (extended abstract). In Proc. 3rd ACM Symp. Principles of Distributed Computing, (PODC'84), Vancouver, B.C., Canada, Aug. 1984, pages 28-37, 1984.","DOI":"10.1145\/800222.806733"},{"issue":"3","key":"10.1016\/S1571-0661(05)80472-4_BIB25","doi-asserted-by":"crossref","first-page":"271","DOI":"10.3233\/FI-1992-17307","article-title":"An automata-theoretic decision procedure for prepositional temporal logic with Since and Until","volume":"17","author":"Ramakrishna","year":"1992","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB26","doi-asserted-by":"crossref","unstructured":"C. Stirling. Comparing linear and branching time temporal logics. In Proc. Workshop Temporal Logic in Specification, Altrincham, UK, Apr. 1987, volume 398 of Lecture Notes in Computer Science, pages 1-20. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51803-7_19"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB27","series-title":"Handbook of Logic in Computer Science","first-page":"477","article-title":"Modal and temporal logics","author":"Stirling","year":"1992"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB28","doi-asserted-by":"crossref","unstructured":"M. Y. Vardi. A temporal fixpoint calculus. In Proc. 15th ACM Symp. Principles of Programming Languages (POPL'88), San Diego, CA, Jan. 1988, pages 250-259, 1988.","DOI":"10.1145\/73560.73582"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB29","doi-asserted-by":"crossref","unstructured":"P. Wolper. On the relation of programs and computations to models of temporal logic. In Proc. Workshop Temporal Logic in Specification, Altrincham, UK, Apr. 1987, volume 398 of Lecture Notes in Computer Science, pages 75-123. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51803-7_23"},{"issue":"1","key":"10.1016\/S1571-0661(05)80472-4_BIB30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2275595","article-title":"Branching-time logic with quantification over branches: The point of view of modal logic","volume":"61","author":"Zanardo","year":"1996","journal-title":"J. Symbolic Logic"},{"issue":"3","key":"10.1016\/S1571-0661(05)80472-4_BIB31","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1093\/logcom\/3.3.249","article-title":"Ockhamist computational logic: Past-sensitive necessitation in CTL\u2217","volume":"3","author":"Zanardo","year":"1993","journal-title":"J. Logic and Computation"},{"key":"10.1016\/S1571-0661(05)80472-4_BIB32","unstructured":"L. Zuck. Past Temporal Logic. PhD thesis, Weizmann Institute, Rehovot, Israel, August 1986."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105804724?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105804724?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:09Z","timestamp":1761610029000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105804724"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"references-count":32,"alternative-id":["S1571066105804724"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80472-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Specification in CTL+Past, Verification in CTL","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)80472-4","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1997 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}