{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:24:42Z","timestamp":1745994282653,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540510802"},{"type":"electronic","value":"9783540461470"}],"license":[{"start":{"date-parts":[[1989,1,1]],"date-time":"1989-01-01T00:00:00Z","timestamp":599616000000},"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":[[1989]]},"DOI":"10.1007\/bfb0013032","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T01:06:46Z","timestamp":1132708006000},"page":"489-507","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["An efficient verification method for parallel and distributed programs"],"prefix":"10.1007","author":[{"given":"Shmuel","family":"Katz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"13_CR1","unstructured":"K. Abrahamson, Decidability and expressiveness of logics of programs, Ph.D. thesis, University of Washington at Seattle, 1980."},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"K.R. Apt","year":"1980","unstructured":"K.R. Apt, N. Francez, W.P. de Roever, A proof system for Communicating Sequential Processes, ACM TOPLAS Vol 2(1980), 359\u2013385.","journal-title":"ACM TOPLAS"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"K.M. Chandy, L. Lamport, Distributed snapshots: determining global states of distributed systems, ACM Transactions on Computer Systems, Vol. 3, No. 1","DOI":"10.1145\/214451.214456"},{"key":"13_CR4","unstructured":"P. Degano, R. De Nicola, U. Montanari, Partial ordering for CCS. In: Proceeding FCT 85, Lecture Notes in Computer Science, Springer-Verlag, 199, 520\u2013533."},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"E.W. Dijkstra, Guarded commands, Nondeterminancy and Formal Derivation of Programs, Communication of the ACM, 18(1975), 453\u2013457.","journal-title":"Communication of the ACM"},{"key":"13_CR6","unstructured":"E.W. Dijkstra, The distributed snapshot algorithm of K.M. Chandy and L. Lamport, EWD864a."},{"key":"13_CR7","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","volume":"2","author":"T. Elrad","year":"1982","unstructured":"Tz. Elrad, N. Francez, Decomposition of distributed programs into communication-closed layers, Science of Computer Programming 2(1982), 155\u2013173","journal-title":"Science of Computer Programming"},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"E.A. Emerson","year":"1983","unstructured":"E.A. Emerson, Alternative semantics for temporal logic, Theoretical Computer Science 26(1983), 121\u2013130.","journal-title":"Theoretical Computer Science"},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson, J.Y. Halpern, \"Sometimes\" and \"not never\" revisited: on branching versus linear time temporal logic, Journal of the ACM 33(1986), 151\u2013178. 30, 1985, 1\u201324.","journal-title":"Journal of the ACM"},{"key":"13_CR10","volume-title":"texts and monographs in computer science","author":"N. Francez","year":"1986","unstructured":"N. Francez, Fairness, texts and monographs in computer science (D. Gries, ed.), Springer-Verlag, New York, 1986."},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"C.A.R. Hoare, Communicating sequential processes, Communications of the ACM, 21 (1978), 666\u2013677.","journal-title":"Communications of the ACM"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"S. Katz, D. Peled, Interleaving Set Temporal Logic, 6\n                  th\n                 ACM Symposium on Principles of Distributed Computing, Vancouver, Canada, August 1987, 178\u2013190.","DOI":"10.1145\/41840.41855"},{"key":"13_CR13","unstructured":"L. Lamport, Paradigms for distributed programs: computing global states, In: Distributed systems \u2014 Methods and tools for specification, An advanced course, Munich, 1985, Edited by M. Paul and H.J. Siegert, Lecture notes in Computer Science, Springer-Verlag, 190, 454\u2013468."},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, Verification of concurrent programs: the temporal framework, In: The correctness problem in computer science, Edited by R.S. Boyer & J.S. Moore, 1981, 215\u2013273.","DOI":"10.21236\/ADA106750"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, How to cook a temporal proof system for your pet language, 10\n                  th\n                 Symposium on principles of programming languages, Austin, Texas, 1983, 141\u2013154.","DOI":"10.1145\/567067.567082"},{"key":"13_CR16","unstructured":"A. Mazurkiewicz, Trace semantics, Proceedings of an advanced course, Bad Honnef, September 1986, Lecture Notes in Computer Science, 255."},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki, L. Lamport, Proving liveness properties of concurrent programs, ACM transactions on Programming languages and Systems, 4, 1982, 455\u2013495.","journal-title":"ACM transactions on Programming languages and Systems"},{"key":"13_CR18","unstructured":"C. A. Petri, Kommunikation mit Automaten, Bonn: Institut fur Instrumentelle Matematik, Schriften des IIM Nr. 2(1962)."},{"key":"13_CR19","unstructured":"A. Pnueli, Applications of temporal logic to the specification and verification of reactive systems, a survey of current trends."},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"W. Reisig, Partial order semantics versus interleaving semantics for CSP like languages and its impact on fairness, 11\n                  th\n                 ICALP, Antwerp, Belgium, 1984, Lecture notes in Computer Science, Springer-Verlag, 172, 403\u2013413.","DOI":"10.1007\/3-540-13345-3_37"}],"container-title":["Lecture Notes in Computer Science","Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0013032","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T23:23:41Z","timestamp":1578525821000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013032"}},"subtitle":["Preliminary version"],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540510802","9783540461470"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0013032","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}