{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T21:57:32Z","timestamp":1775512652465,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540156482","type":"print"},{"value":"9783540395270","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15648-8_16","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:21:08Z","timestamp":1330194068000},"page":"196-218","source":"Crossref","is-referenced-by-count":239,"title":["The glory of the past"],"prefix":"10.1007","author":[{"given":"Orna","family":"Lichtenstein","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"16_CR1","unstructured":"Alpern, B., Schneider, F.B., \u2014 Defining Liveness, Cornell University, (Oct. 1984)."},{"key":"16_CR2","unstructured":"Barringer, H., Kuiper R., \u2014 A Temporal Logic Specification Method Supporting Hierarchical Development, University of Manchester, (Nov. 1983)."},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Barringer, H., Kuiper, R., Pnueli, A. \u2014 Now You May Compose Temporal Logic Specifications, 16th Symposium on Theory of Computing (April 84), 51\u201363.","DOI":"10.1145\/800057.808665"},{"key":"16_CR4","unstructured":"B\u00fcchi, J.R., \u2014 On a Decision Method in Restricted Second Order Arithmetic, Proc. Intern. Congr. Logic, and Philos. Sci. 1960, 1960, Stanford University Press (1962) 1\u201311."},{"key":"16_CR5","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J.R. B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R., \u2014 Weak Second Order Arithmetics and Finite Automata, Z. Math. Logik Grundlagen Math 6 (1960) 66\u201392.","journal-title":"Z. Math. Logik Grundlagen Math"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Burgess, J., \u2014 Basic Tense Logic, in Handbook of Philosophical Logic, Vol. 2 (D. Gabbay and F. Guenthner eds.) D. Reidel Pub. Co., (1984).","DOI":"10.1007\/978-94-009-6259-0_2"},{"key":"16_CR7","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Choueka, Y., \u2014 Theories of Automata on \u03c9-Tapes: A Simplified Approach, Journal of Computers and Systems Sciences 8 (1974) 117\u2013141.","journal-title":"Journal of Computers and Systems Sciences"},{"key":"16_CR8","unstructured":"Chen, Z.C., Hoare, C.A.R., \u2014 Partial Correctness of Communicating Processes and Protocols, Technical Monograph, PRG-20 Oxford University Computing Laboratory (May 1981)."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J., \u2014 On the Temporal Analysis of Fairness, Proc of the 7th ACM Symp. on Principles of Programming Languages (1980) 163\u2013173.","DOI":"10.1145\/567446.567462"},{"key":"16_CR10","unstructured":"Hoare, C.A.R., \u2014 A Calculus of Total Correctness for Communicating Precesses, Technical Monograph, RPG-23 Oxford University Computing Laboratory (May 1981)."},{"key":"16_CR11","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1109\/TCOM.1983.1095720","volume":"1","author":"B. Hailpern","year":"1983","unstructured":"Hailpern, B., Owicki, S., \u2014 Modular Verification of Computer Communication Protocols, IEEE Trans. on Communications, COM-31, 1 (Jan. 1983) 56\u201368.","journal-title":"IEEE Trans. on Communications"},{"key":"16_CR12","unstructured":"Kamp, H.W., \u2014 Tense Logic and the Theory of Linear Order, Ph.D. Thesis, University of California Los Angeles (1968)."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Koymans, R., Vytopil, J., DeRoever, W.P., \u2014 Real Time Programming and Asynchronous Message Passing, 2nd ACM Symp. of Distributed Computing, Montreal (1983) 187\u2013197.","DOI":"10.1145\/800221.806721"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Lamport, L., \u2014 What is Good in Temporal Logic?, Proceeding IFIP (1983) 657\u2013668.","DOI":"10.1145\/2402.322398"},{"key":"16_CR15","unstructured":"Lichtenstein, O., \u2014 Decidability and Completeness of a Temporal Proof System for Finite State Programs, M.Sc. Thesis, Tel Aviv University (1984)."},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A., \u2014 Checking That Finite State Concurrent Programs Satisfy Their Linear Specification, ACM Symp. on Principles of Programming Languages (1985).","DOI":"10.1145\/318593.318622"},{"key":"16_CR17","first-page":"4","volume":"5E-7","author":"J. Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M., \u2014 Proofs of Networks of Processes, IEEE Trans. on Software Engineering 5E-7, 4 (July 1981).","journal-title":"IEEE Trans. on Software Engineering"},{"key":"16_CR18","volume-title":"Counter Free Automata","author":"R. McNaughton","year":"1971","unstructured":"McNaughton, R., Papert, S., \u2014 Counter Free Automata, MIT press, Cambridge, Mass (1971)."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A., \u2014 Verification of Concurrent Programs: A Temporal Proof System, Proc. 4th School on Advanced Programming, Amsterdam (June 1982) 163\u2013255.","DOI":"10.21236\/ADA116035"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A., \u2014 How to Cook a Temporal Proof System for your Pet Programming Language Proc of the 10th ACM Symp. on Principles of Programming Languages (1983).","DOI":"10.1145\/567067.567082"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A., \u2014 Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs, Science and Computer Programming, Forthcoming.","DOI":"10.1016\/0167-6423(84)90003-0"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Nguyen, V., Gries, D., Owicki, S., \u2014 A Model and Temporal Proof System for Networks of Processes, Proc of the 12th ACM Symp. on Principles of Programming Languages (1985).","DOI":"10.1145\/318593.318624"},{"key":"16_CR23","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D., \u2014 An axiomatic Proof Technique for Parallel Programs, Acta Informatica 6 (1976) 319\u2013340.","journal-title":"Acta Informatica"},{"issue":"3","key":"16_CR24","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"Owicki, S., Lamport, L., \u2014 Proving Liveness Properties of Concurrent Programs, ACM TOPLAS 4,3 (July 1982) 455\u2013495.","journal-title":"ACM TOPLAS"},{"key":"16_CR25","unstructured":"Peikert, R., \u2014 Propositional Temporal Logic and \u03c9-regular Languages, Manuscript, ETH-Z\u00fcrich."},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Pnueli, A., \u2014 The Temporal Logic of Programs, 18th Annual Symp. on Foundation of Computer Science (1977) 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A., \u2014 In Transition from Global to Modular Temporal Reasoning about Programs, Proc. Advanced NATO Institute on Logic and Models for Verification and Specification of Concurrent Systems, La Colle-Sur-Loupe (Oct. 1984).","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A., \u2014 On the Extremely Fair Treatment of Probabilistic Algorithms, Proc. of the 15th Annual ACM Symp. on Theory of Computing (1983).","DOI":"10.1145\/800061.808757"},{"key":"16_CR29","unstructured":"Prior, \u2014 Past Present and Future, Oxford Press."},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Rescher, N., Urquhart, A., \u2014 Temporal Logic, Springer Verlag (1971).","DOI":"10.1007\/978-3-7091-7664-1"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Sistla, A.P., \u2014 Characterization of Safety and Liveness Properties in Temporal Logic, University of Massachusetts, Amherst (Nov. 1984).","DOI":"10.1145\/323596.323600"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"A.P. Sistla, E.M. Carke, The Complexity of Propositional Temporal Logic, 14th ACM Symposium on Thoery of Computing, (May 1982) 159\u2013167.","DOI":"10.1145\/800070.802189"},{"issue":"3","key":"16_CR33","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/S0019-9958(81)90663-X","volume":"48","author":"W. Thomas","year":"1981","unstructured":"Thomas, W., \u2014 A Combinatorial Approach to the Theory of \u03c9-Automata, Information and Control 48,3 (March 1981) 261\u2013283.","journal-title":"Information and Control"},{"key":"16_CR34","unstructured":"Vardi, M.Y., Wolper, P., \u2014 Expressiveness and Complexity of Languages for Describing Sequences, Stanford University."},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"Wolper, P., \u2014 Temporal Logic can be More Expressive, Proc. of the 22nd Annual Symp. on Foundation of Computer Science (1981) 340\u2013348.","DOI":"10.1109\/SFCS.1981.44"}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15648-8_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:22:23Z","timestamp":1742588543000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15648-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540156482","9783540395270"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-15648-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1985]]}}}