{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T17:54:11Z","timestamp":1776362051001,"version":"3.51.2"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1987,9,1]],"date-time":"1987-09-01T00:00:00Z","timestamp":557452800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Distrib Comput"],"published-print":{"date-parts":[[1987,9]]},"DOI":"10.1007\/bf01782772","type":"journal-article","created":{"date-parts":[[2005,6,20]],"date-time":"2005-06-20T20:39:32Z","timestamp":1119299972000},"page":"117-126","source":"Crossref","is-referenced-by-count":351,"title":["Recognizing safety and liveness"],"prefix":"10.1007","volume":"2","author":[{"given":"Bowen","family":"Alpern","sequence":"first","affiliation":[]},{"given":"Fred B.","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"BF01782772_CR1","unstructured":"Alpern B (1986) Proving temporal properties of concurrent programs: a non-temporal approach. PhD Thesis. Department of Computer Science, Cornell University (January 1986)"},{"issue":"4","key":"BF01782772_CR2","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0020-0190(86)90132-8","volume":"23","author":"B Alpern","year":"1986","unstructured":"Alpern B, Demers AJ, Schneider FB (1986) Safety without stuttering. Inf Proc Lett 23(4): 177\u2013180","journal-title":"Inf Proc Lett"},{"key":"BF01782772_CR3","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. Inf Proc Lett 21:181\u2013185","journal-title":"Inf Proc Lett"},{"key":"BF01782772_CR4","unstructured":"Alpern B, Schneider FB (1985) Verifying temporal properties without using temporal logic. Tech Rep TR 85-723, Department of Computer Science, Cornell University (December 1985)"},{"key":"BF01782772_CR5","doi-asserted-by":"crossref","unstructured":"Alpern B, Schneider FB (1987) Proving boolean combinations of deterministic properties. Proc 2nd Ann Symp Logic Comput Sci; IEEE Comput Soc, Ithaca, NY (June 1987)","DOI":"10.1007\/BF01782772"},{"issue":"2","key":"BF01782772_CR6","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson, EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Programm Languages Syst 8(2):244\u2013263","journal-title":"ACM Trans Programm Languages Syst"},{"key":"BF01782772_CR7","volume-title":"Automata Languages and Machines, Vol A","author":"S Eilenberg","year":"1974","unstructured":"Eilenberg S (1974) Automata Languages and Machines, Vol A. Academic Press, NY"},{"key":"BF01782772_CR8","unstructured":"Hopcroft JE, Ullman JD (1979) Introduction to Automata Theory, Languages and Computation. Addison-Wesley"},{"issue":"2","key":"BF01782772_CR9","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Software Eng SE-3, 2:125\u2013143","journal-title":"IEEE Trans Software Eng SE"},{"key":"BF01782772_CR10","first-page":"657","volume-title":"Information Processing '83","author":"L Lamport","year":"1983","unstructured":"Lamport L (1983) What good is temporal logic. In: Magon REA (ed) Information Processing '83. North-Holland, Amsterdam, pp 657\u2013668"},{"key":"BF01782772_CR11","series-title":"Lect Notes Comput","volume-title":"Distributed Systems \u2014 Methods and Tools for Specification, vol 190","author":"L Lamport","year":"1985","unstructured":"Lamport L (1985) Logical foundation. In: Paul M, Siegert HJ (eds) Distributed Systems \u2014 Methods and Tools for Specification, vol 190. Lect Notes Comput. Springer-Verlag, Berlin Heidelberg New York"},{"key":"BF01782772_CR12","doi-asserted-by":"crossref","unstructured":"Lichtenstein O, Pnueli O, Zuck L (1985) The glory of the past. Proc Workshop on Logics of Programs, vol 193 (June 1985). Brooklyn, NY. Lect. Notes Comput Sci, pp 196\u2013218","DOI":"10.1007\/3-540-15648-8_16"},{"key":"BF01782772_CR13","first-page":"141","volume-title":"The Correctness Problem in Computer Science (1981) International lectures in Computer Science","author":"Z Manna","year":"1981","unstructured":"Manna Z, Pnueli A (1981) Verification of concurrent programs: The temporal framework. In: Boyer RS, Moore JS (eds) The Correctness Problem in Computer Science (1981) International lectures in Computer Science. Academic Press, London, pp 141\u2013154"},{"key":"BF01782772_CR14","series-title":"Proc 14th Symp Principles of Programming Languages","first-page":"1","volume-title":"Specification and Verification of Concurrent Programs by \u2200-Automata","author":"Z Manna","year":"1987","unstructured":"Manna Z, Pnueli A (1987) Specification and Verification of Concurrent Programs by \u2200-Automata. Proc 14th Symp Principles of Programming Languages. ACM, Munich, (January 1987), pp 1\u201312."},{"key":"BF01782772_CR15","series-title":"Proc 4th Symp Principles of Distributed Computing","first-page":"39","volume-title":"On characterization of safety and liveness properties in temporal logic","author":"AP Sistla","year":"1985","unstructured":"Sistla AP (1985) On characterization of safety and liveness properties in temporal logic. Proc 4th Symp Principles of Distributed Computing. ACM, Minaki, (August 1985), pp 39\u201348"},{"key":"BF01782772_CR16","volume-title":"On characterization of safety and liveness properties in temporal logic","author":"AP Sistla","year":"1986","unstructured":"Sistla AP (1986) On characterization of safety and liveness properties in temporal logic. Tech Rep, GTE Lab, Waltham MA, (March 1986, revised July 1986)."},{"key":"BF01782772_CR17","series-title":"Proc 12th International Colloquium on Automata, Languages and Programming, ICALP'85. Nafplion Greece (July 1985) Lect Notes Comput","first-page":"465","volume-title":"The complementation problems for Buchi automata with applications to temporal logic (extended abstract)","author":"AP Sistla","year":"1985","unstructured":"Sistla AP, Yardi MY, Wolper P (1985) The complementation problems for Buchi automata with applications to temporal logic (extended abstract). Proc 12th International Colloquium on Automata, Languages and Programming, ICALP'85. Nafplion Greece (July 1985) Lect Notes Comput Sci Springer Verlag, New York 194:465\u2013474"},{"key":"BF01782772_CR18","series-title":"Proc 2nd Annual Symposium on Logic in Computer Science","volume-title":"Verification of concurrent programs: The automata-theoretic framework","author":"M Vardi","year":"1987","unstructured":"Vardi M (1987) Verification of concurrent programs: The automata-theoretic framework. Proc 2nd Annual Symposium on Logic in Computer Science. IEEE Comput Soc, Ithaca, NY (June 1987)"},{"issue":"1\u20132","key":"BF01782772_CR19","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper P (1983) Temporal logic can be more expressive. Control 56(1\u20132):72\u201399","journal-title":"Control"}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01782772.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01782772\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01782772","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,3]],"date-time":"2023-05-03T13:05:20Z","timestamp":1683119120000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01782772"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987,9]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1987,9]]}},"alternative-id":["BF01782772"],"URL":"https:\/\/doi.org\/10.1007\/bf01782772","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"value":"0178-2770","type":"print"},{"value":"1432-0452","type":"electronic"}],"subject":[],"published":{"date-parts":[[1987,9]]}}}