{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T18:28:34Z","timestamp":1780338514731,"version":"3.54.1"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,1,28]],"date-time":"2009-01-28T00:00:00Z","timestamp":1233100800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10703-009-0067-z","type":"journal-article","created":{"date-parts":[[2009,1,27]],"date-time":"2009-01-27T22:26:05Z","timestamp":1233095165000},"page":"83-103","source":"Crossref","is-referenced-by-count":57,"title":["From liveness to promptness"],"prefix":"10.1007","volume":"34","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","published-online":{"date-parts":[[2009,1,28]]},"reference":[{"issue":"3","key":"67_CR1","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1145\/377978.377990","volume":"2","author":"R Alur","year":"2001","unstructured":"Alur R, Etessami K, La Torre S, Peled D (2001) Parametric temporal logic for model measuring. ACM Trans Comput Log 2(3):388\u2013407","journal-title":"ACM Trans Comput Log"},{"key":"67_CR2","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern B, Schneider FB (1985) Defining liveness. Inform Process Lett 21:181\u2013185","journal-title":"Inform Process Lett"},{"key":"67_CR3","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/3-540-58179-0_53","volume-title":"Proc 6th conference on computer aided verification","author":"I Beer","year":"1994","unstructured":"Beer I, Ben-David S, Geist D, Gewirtzman R, Yoeli M (1994) Methodology and system for practical formal verification of reactive hardware. In: Proc 6th conference on computer aided verification, Stanford, June 1994. Lecture notes in computer science, vol\u00a0818. Springer, New York, pp 182\u2013193"},{"key":"67_CR4","doi-asserted-by":"crossref","unstructured":"Biere A, Artho C, Schuppan V (2002) Liveness checking as safety checking. In: Proc 7th international workshop on formal methods for industrial critical systems. Electronic notes in theoretical computer science, vol\u00a066:2","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"67_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 HN, Somenzi F (2000) An algorithm for strongly connected component analysis in nlog\u2009n symbolic steps. In: Formal methods in computer aided design. Lecture notes in computer science, vol\u00a01954. Springer, New York, pp 37\u201354"},{"key":"67_CR6","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"JR B\u00fcchi","year":"1969","unstructured":"B\u00fcchi JR, Landweber LHG (1969) Solving sequential conditions by finite-state strategies. Trans Am Math Soc 138:295\u2013311","journal-title":"Trans Am Math Soc"},{"key":"67_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/11691372_17","volume-title":"Proc 12th international conference on tools and algorithms for the construction and analysis of systems","author":"K Chatterjee","year":"2006","unstructured":"Chatterjee K, Henzinger TA (2006) Finitary winning in \u03c9-regular games. In: Proc 12th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol\u00a03920. Springer, New York, pp 257\u2013271"},{"key":"67_CR8","volume-title":"A practical introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner C, Fisman D (2006) A practical introduction to PSL. Springer, New York"},{"key":"67_CR9","first-page":"997","volume-title":"Handbook of theoretical computer science","author":"EA Emerson","year":"1990","unstructured":"Emerson EA (1990) Temporal and modal logic. In: Van Leeuwen J (ed) Handbook of theoretical computer science, vol\u00a0B. MIT Press, Cambridge, pp 997\u20131072, chap\u00a016"},{"key":"67_CR10","doi-asserted-by":"crossref","unstructured":"Emerson EA, Jutla C (1991) Tree automata, \u03bc-calculus and determinacy. In: Proc 32nd IEEE symp on foundations of computer science, San Juan, October 1991, pp 368\u2013377","DOI":"10.1109\/SFCS.1991.185392"},{"key":"67_CR11","unstructured":"Emerson EA, Lei C-L (1986) Efficient model checking in fragments of the propositional \u03bc-calculus. In: Proc 1st symp on logic in computer science, Cambridge, June 1986, pp 267\u2013278"},{"key":"67_CR12","series-title":"Lecture notes in computer science","first-page":"136","volume-title":"Proc 2nd conference on computer aided verification","author":"EA Emerson","year":"1990","unstructured":"Emerson EA, Mok AK, Sistla AP, Srinivasan J (1990) Quantitative temporal reasoning. In: Proc 2nd conference on computer aided verification. Lecture notes in computer science, vol\u00a0531. Springer, New York, pp 136\u2013145"},{"key":"67_CR13","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-18088-5_22","volume-title":"Proc 14th international coll on automata, languages, and programming","author":"T Hafer","year":"1987","unstructured":"Hafer T, Thomas W (1987) Computation tree logic CTL \u22c6 and path quantifiers in the monadic theory of the binary tree. In: Proc 14th international coll on automata, languages, and programming. Lecture notes in computer science, vol\u00a0267. Springer, New York, pp 269\u2013279"},{"key":"67_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/978-3-540-71209-1_36","volume-title":"Proc 13th international conference on tools and algorithms for the construction and analysis of systems","author":"F Horn","year":"2007","unstructured":"Horn F (2007) Faster algorithms for finitary games. In: Proc 13th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol\u00a04424. Springer, New York, pp 472\u2013484"},{"key":"67_CR15","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1007\/3-540-60246-1_160","volume-title":"Proc 20th international symp on mathematical foundations of computer science","author":"D Janin","year":"1995","unstructured":"Janin D, Walukiewicz I (1995) Automata for the modal \u03bc-calculus and related results. In: Proc 20th international symp on mathematical foundations of computer science. Lecture notes in computer science. Springer, New York, pp 552\u2013562"},{"key":"67_CR16","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/3-540-61604-7_60","volume-title":"Proc 7th conference on concurrency theory","author":"D Janin","year":"1996","unstructured":"Janin D, Walukiewicz I (1996) On the expressive completeness of the propositional \u03bc-calculus with respect to the monadic second order logic. In: Proc 7th conference on concurrency theory. Lecture notes in computer science, vol\u00a01119. Springer, New York, pp 263\u2013277"},{"key":"67_CR17","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi MY (2005) Safraless decision procedures. In: Proc 46th IEEE symp on foundations of computer science, Pittsburgh, October 2005, pp 531\u2013540","DOI":"10.1109\/SFCS.2005.66"},{"key":"67_CR18","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 (1992) The temporal logic of reactive and concurrent systems: Specification. Springer, Berlin"},{"key":"67_CR19","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"DE Muller","year":"1995","unstructured":"Muller DE, Schupp PE (1995) Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. Theor Comput Sci 141:69\u2013107","journal-title":"Theor Comput Sci"},{"key":"67_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proc 18th IEEE symp on foundation of computer science, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"67_CR21","series-title":"NATO advanced summer institutes","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and models of concurrent systems","author":"A Pnueli","year":"1985","unstructured":"Pnueli A (1985) In transition from global to modular temporal reasoning about programs. In: Apt K (ed) Logics and models of concurrent systems. NATO advanced summer institutes, vol\u00a0F-13. Springer, New York, pp 123\u2013144"},{"key":"67_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proc 16th ACM symp on principles of programming languages, Austin, January 1989, pp 179\u2013190","DOI":"10.1145\/75277.75293"},{"key":"67_CR23","first-page":"1","volume":"141","author":"MO Rabin","year":"1969","unstructured":"Rabin MO (1969) Decidability of second order theories and automata on infinite trees. Trans Am Math Soc 141:1\u201335","journal-title":"Trans Am Math Soc"},{"key":"67_CR24","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"AP Sistla","year":"1987","unstructured":"Sistla AP, Vardi MY, Wolper P (1987) The complementation problem for B\u00fcchi automata with applications to temporal logic. Theor Comput Sci 49:217\u2013237","journal-title":"Theor Comput Sci"},{"issue":"2","key":"67_CR25","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan RE (1972) Depth first search and linear graph algorithms. SIAM J Comput 1(2):146\u2013160","journal-title":"SIAM J Comput"},{"key":"67_CR26","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":"8th international conference on verification, model checking, and abstract interpretation","author":"MY Vardi","year":"2007","unstructured":"Vardi MY (2007) Automata-theoretic model checking revisited. In: 8th international conference on verification, model checking, and abstract interpretation. Lecture notes in computer science, vol\u00a04349. Springer, New York, pp 137\u2013150"},{"key":"67_CR27","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proc 1st symp on logic in computer science, Cambridge, June 1986, pp 332\u2013344"},{"issue":"1","key":"67_CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi MY, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1\u201337","journal-title":"Inf Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0067-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0067-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0067-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:03Z","timestamp":1559253663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0067-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,28]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["67"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0067-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1,28]]}}}