{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:56:17Z","timestamp":1759146977691,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230243"},{"type":"electronic","value":"9783540301240"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30124-0_24","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T12:27:59Z","timestamp":1267532879000},"page":"295-309","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Intuitionistic LTL and a New Characterization of Safety and Liveness"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Maier","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,9,9]]},"reference":[{"issue":"3","key":"24_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems\u00a017(3), 507\u2013534 (1995)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60246-1_155","volume-title":"Mathematical Foundations of Computer Science 1995","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Merz, S.: An abstract account of composition. In: H\u00e1jek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol.\u00a0969, pp. 499\u2013508. Springer, Heidelberg (1995)"},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(93)90151-I","volume":"114","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Plotkin, G.D.: A logical view of composition. Theoretical Computer Science\u00a0114, 3\u201330 (1993)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"24_CR4","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters\u00a021(4), 181\u2013185 (1985)","journal-title":"Information Processing Letters"},{"issue":"3","key":"24_CR5","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed Computing\u00a02(3), 117\u2013126 (1987)","journal-title":"Distributed Computing"},{"key":"24_CR6","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1109\/LICS.1996.561317","volume-title":"Proceedings of the 11th IEEE Symposium on Logic in Computer Science (LICS)","author":"R. Davies","year":"1996","unstructured":"Davies, R.: A temporal-logic approach to binding-time analysis. In: Proceedings of the 11th IEEE Symposium on Logic in Computer Science (LICS), pp. 184\u2013195. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 27\u201339. Springer, Heidelberg (2003)"},{"key":"24_CR8","first-page":"995","volume-title":"Handbook of Theoretical Computer Science","author":"E. Allen Emerson","year":"1990","unstructured":"Allen Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 995\u20131072. Elsevier, Amsterdam (1990)"},{"issue":"6","key":"24_CR9","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0020-0190(93)90074-J","volume":"47","author":"H. Peter Gumm","year":"1993","unstructured":"Peter Gumm, H.: Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions. Information Processing Letters\u00a047(6), 291\u2013294 (1993)","journal-title":"Information Processing Letters"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0304-3975(96)00069-2","volume":"167","author":"B. Jonsson","year":"1996","unstructured":"Jonsson, B., Tsay, Y.-K.: Assumption\/guarantee specifications in lineartime temporal logic. Theoretical Computer Science\u00a0167, 47\u201372 (1996)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"24_CR11","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering\u00a03(2), 125\u2013143 (1977)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol.\u00a0193, pp. 196\u2013218. Springer, Heidelberg (1985)"},{"key":"24_CR13","unstructured":"Maier, P.: A Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning. PhD thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken (July 2003)"},{"key":"24_CR14","unstructured":"Maier, P.: Intuitionistic LTL and a new characterization of safety and liveness. Technical Report MPI-I-2004-2-002, Max-Planck-Institut f\u00fcr Informatik (2004)"},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1109\/LICS.2001.932512","volume-title":"Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS)","author":"P. Manolios","year":"2001","unstructured":"Manolios, P., Trefler, R.: Safety and liveness in branching time. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS), pp. 366\u2013374. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"24_CR16","first-page":"325","volume-title":"Proceedings of the 22nd ACM Symposium on Principles of Distributed Computing (PODC)","author":"P. Manolios","year":"2003","unstructured":"Manolios, P., Trefler, R.: A lattice-theoretic characterization of safety and liveness. In: Proceedings of the 22nd ACM Symposium on Principles of Distributed Computing (PODC), pp. 325\u2013333. ACM Press, New York (2003)"},{"key":"24_CR17","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1016\/B978-0-934613-04-0.50032-6","volume-title":"Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK)","author":"G. Plotkin","year":"1986","unstructured":"Plotkin, G., Stirling, C.: A framework for intuitionistic modal logics. In: Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), pp. 399\u2013406. Morgan Kaufmann, San Francisco (1986)"},{"key":"24_CR18","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science\u00a013, 45\u201360 (1981)","journal-title":"Theoretical Computer Science"},{"key":"24_CR19","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A. Prasad Sistla","year":"1994","unstructured":"Prasad Sistla, A.: Safety, liveness and fairness in temporal logic. Formal Aspects of Computing\u00a06, 495\u2013511 (1994)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30124-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T20:03:19Z","timestamp":1579723399000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30124-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230243","9783540301240"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30124-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]},"assertion":[{"value":"9 September 2004","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}