{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T05:23:28Z","timestamp":1736659408069,"version":"3.32.0"},"reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540558224"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0084792","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T13:12:14Z","timestamp":1164373934000},"page":"192-206","source":"Crossref","is-referenced-by-count":1,"title":["Sometimes \u2018some\u2019 is as good as \u2018all\u2019"],"prefix":"10.1007","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern, F.B. Schneider, Defining Liveness, Information Processing Letters 21, 1985, 181\u2013185.","journal-title":"Information Processing Letters"},{"key":"15_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 Transactions on Programming Languages and Systems, Vol 2, 1980, 359\u2013385.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR3","volume-title":"Mathematical Theory of Program Correctness","author":"J. W. deBakker","year":"1980","unstructured":"J. W. deBakker, Mathematical Theory of Program Correctness, Prentice-Hall, Englewood Cliffs, N. J., 1980."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, A. Pnueli, Now You May Compose Temporal Logic Specification, Proceedings of 16th ACM Symposium on Theory of Computing, 1984, 51\u201363.","DOI":"10.1145\/800057.808665"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/214451.214456","volume":"3","author":"K. M. Chandy","year":"1985","unstructured":"K. M. Chandy, L. Lamport, Distributed Snapshots: determining the global state of distributed systems, ACM Transactions on Computer Systems 3, 1985, 63\u201375.","journal-title":"ACM Transactions on Computer Systems"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"E. Chang, Z. Manna, A. Pnueli, The Safety-Progress Classification, Manuscript 1992.","DOI":"10.1007\/978-3-642-58041-3_5"},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/BF00571463","volume":"2","author":"M. Clint","year":"1973","unstructured":"M. Clint, Program proving: Coroutines, Acta Informatica 2, 1973, 50\u201363.","journal-title":"Acta Informatica"},{"key":"15_CR8","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":"15_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, \u201cSometimes\u201d and \u201cNot Never\u201d Revisited: On Branching versus Linear Time Temporal Logic, Journal of the ACM 33 (1986), 151\u2013178.","journal-title":"Journal of the ACM"},{"key":"15_CR10","unstructured":"D. Gabbay, The declarative past and imperative future, in: B. Banieqbal, H. Barringer, A. Pnueli (editors), Temporal Logic in Specification, LNCS 398, Springer-Verlag, 1987, 407\u2013448."},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"P. Godefroid, P. Wolper, Using partial orders for the efficient verification of deadlock freedom and safety properties, Proceedings of Computer-Aided Verification, Aalborg, Denmark, 1991.","DOI":"10.1007\/3-540-55179-4_32"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"D. Harel, First order Dynamic Logic, Lecture Notes in Computer Science 68, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09237-4"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"15_CR14","first-page":"307","volume-title":"LNCS 571","author":"W. Janssen","year":"1992","unstructured":"W. Janssen, J. Zwiers, Protocol Design by Layered Decomposition, A compositional Approach, 2nd Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Nijmegen, The Netherlands, 1992, LNCS 571, Springer-Verlag, 307\u2013326."},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/0304-3975(90)90096-Z","volume":"75","author":"S. Katz","year":"1990","unstructured":"S. Katz, D. Peled, Interleaving Set Temporal Logic, Theoretical Computer Science 75 (1990), 21\u201343.","journal-title":"Theoretical Computer Science"},{"key":"15_CR16","unstructured":"S. Katz, D. Peled, Verification of Distributed Programs using Representative Interleaving Sequences, to appear in Distributed Computing."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"M. Z. Kwiatkowska, Fairness for Non-interleaving Concurrency, Phd. Thesis, Faculty of Science, University of Leicester, 1989.","DOI":"10.1007\/BF01887206"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"\u201cSometime\u201d is Sometimes \u201cNot Never\u201d \u2014 On the Temporal Logic of Programs, Proceedings of the 7th ACM symposium on Principles of Programming Languages, 1980, 174\u2013185.","DOI":"10.1145\/567446.567463"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, How to Cook a Temporal Proof System for Your Pet Language. Proceedings of the Symposium on Principles on Programming Languages, Austin, Texas, 1983, 141\u2013151.","DOI":"10.1145\/567067.567082"},{"key":"15_CR20","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Z. Manna, A. Pnueli, Completing the temporal picture, Theoretical Computer Science 83 (1991), 97\u2013130.","journal-title":"Theoretical Computer Science"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"A. Mazurkiewicz, Traces, Histories, Graphs: Instances of a process monoid, in M. Chytil (Ed.), Mathematical Foundation of Computer Science, LNCS 176, Springer-Verlag, 1984, 115\u2013133.","DOI":"10.1007\/BFb0030293"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"D. Park, On the Semantics of Fair Parallelism, in D. Biorner (ed.), Proceedings on Abstract Software Specification, LNCS 86, Springer-Verlag, 1979, 504\u2013526.","DOI":"10.1007\/3-540-10007-5_47"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"D. Peled, S. Katz, and A. Pnueli, Specifying and Proving Serializability in Temporal Logic, LICS 91', Amsterdam, The Netherlands, July 1991, 232\u2013245.","DOI":"10.1109\/LICS.1991.151648"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"D. Peled, M. Joseph, A Compositional Approach to Fault Tolerance Using Specification Transformation, Manuscript, 1992.","DOI":"10.1007\/3-540-56891-3_14"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"D. Peled, A. Pnueli, Proving partial order liveness properties, in M.S. Paterson (ed.), Proceedings of the 17th ICALP, LNCS 443, Springer-Verlag, 1990, 553\u2013571.","DOI":"10.1007\/BFb0032058"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"W. Penczek, A Concurrent Branching Time Temporal Logic, Conference on Computer Science Logic, LNCS 440, Springer-Verlag, 1989, 337\u2013354.","DOI":"10.1007\/3-540-52753-2_49"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"S. Pinter, P. Wolper, A Temporal Logic for Reasoning about Partially Ordered Computations, Proceedings of the 3rd ACM Symposium on Principles of Distributed Computing, Vancouver, B. C., August 1984, 23\u201327.","DOI":"10.1145\/800222.806733"},{"key":"15_CR28","first-page":"46","volume-title":"The Temporal Logic of Programs","author":"A. Pnueli","year":"1977","unstructured":"A. Pnueli, The Temporal Logic of Programs, Proceedings of the 18th Symposium on Foundation of Computer Science, IEEE, Providence, 1977, 46\u201357."},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"F. A. Stomp, W. P. deRoever, Designing Distributed Algorithms by Means of Formal Sequentially Phased Reasoning, Proceedings of the 3rd International Workshop on Distributed Algorithms, LNCS 392, Springer-Verlag, 1989, 242\u2013253.","DOI":"10.1007\/3-540-51687-5_47"},{"key":"15_CR30","first-page":"1","volume":"2","author":"A. Valmari","year":"1989","unstructured":"A. Valmari, Stubborn Sets for Reduced State Space Generation, 10th International Conference on Application and Theory of Petri Nets, Germany, 1989, Vol 2, 1\u201322.","journal-title":"10th International Conference on Application and Theory of Petri Nets, Germany"},{"key":"15_CR31","unstructured":"J. Zwiers, Compositionality, Concurrency and Partial Correctness, LNCS 321, Springer-Verlag, 1987."},{"key":"15_CR32","unstructured":"L. Zhiming, M. Joseph, Transformations of programs for fault-tolerance, to appear in Formal Aspects of Computing."}],"container-title":["Lecture Notes in Computer Science","CONCUR '92"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0084792.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T03:55:25Z","timestamp":1736654125000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0084792"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540558224"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/bfb0084792","relation":{},"subject":[]}}