{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T08:07:34Z","timestamp":1790496454850,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540733676","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_44","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"406-419","source":"Crossref","is-referenced-by-count":7,"title":["From Liveness to Promptness"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"3","key":"44_CR1","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1145\/377978.377990","volume":"2","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., Torre, S.L., Peled, D.: Parametric temporal logic for model measuring. ACM ToCL\u00a02(3), 388\u2013407 (2001)","journal-title":"ACM ToCL"},{"key":"44_CR2","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. IPL\u00a021, 181\u2013185 (1985)","journal-title":"IPL"},{"key":"44_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: Proc. 7th FMICS, ENTCS, vol. 66(2) (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"44_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/3-540-58179-0_53","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1994","unstructured":"Beer, I., Ben-David, S., Geist, D., Gewirtzman, R., Yoeli, M.: Methodology and system for practical formal verification of reactive hardware. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 182\u2013193. Springer, Heidelberg (1994)"},{"key":"44_CR5","series-title":"Lecture Notes in Computer Science","first-page":"37","volume-title":"Formal Methods in Computer-Aided Design","author":"R. Bloem","year":"2000","unstructured":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n logn symbolic steps. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 37\u201354. Springer, Heidelberg (2000)"},{"key":"44_CR6","doi-asserted-by":"publisher","first-page":"295","DOI":"10.2307\/1994916","volume":"138","author":"J.R. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.G.: Solving sequential conditions by finite-state strategies. Trans. AMS\u00a0138, 295\u2013311 (1969)","journal-title":"Trans. AMS"},{"key":"44_CR7","volume-title":"A Practical Introduction to PSL","author":"C. Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)"},{"key":"44_CR8","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional \u03bc-calculus. In: Proc. 1st LICS, pp. 267\u2013278 (1986)"},{"key":"44_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/BFb0023727","volume-title":"Computer-Aided Verification","author":"E.A. Emerson","year":"1991","unstructured":"Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 136\u2013145. Springer, Heidelberg (1991)"},{"key":"44_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin (1992)"},{"key":"44_CR11","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"44_CR12","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In: Transition from global to modular temporal reasoning about programs. Logics and Models of Concurrent Systems, vol. F-13 of NATO Advanced Summer Institutes, pp. 123\u2013144 (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"44_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"issue":"2","key":"44_CR14","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM Journal of Computing\u00a01(2), 146\u2013160 (1972)","journal-title":"SIAM Journal of Computing"},{"key":"44_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-540-69738-1_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 137\u2013150. Springer, Heidelberg (2007)"},{"key":"44_CR16","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st LICS, pp. 332\u2013344 (1986)"},{"issue":"1","key":"44_CR17","first-page":"1","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C\u00a0115(1), 1\u201337 (1994)","journal-title":"I&C"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:36Z","timestamp":1619518116000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_44","relation":{},"subject":[]}}