{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:29Z","timestamp":1776305309640,"version":"3.50.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1992,9,1]],"date-time":"1992-09-01T00:00:00Z","timestamp":715305600000},"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":[[1992,9]]},"DOI":"10.1007\/bf02252682","type":"journal-article","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T14:56:36Z","timestamp":1132671396000},"page":"107-120","source":"Crossref","is-referenced-by-count":55,"title":["Verification of distributed programs using representative interleaving sequences"],"prefix":"10.1007","volume":"6","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","reference":[{"key":"BF02252682_CR1","volume-title":"Decidability and expressiveness of logics of programs","author":"K Abrahamson","year":"1980","unstructured":"Abrahamson K: Decidability and expressiveness of logics of programs. Ph.D. Thesis. University of Washington, Seattle 1980"},{"issue":"4","key":"BF02252682_CR2","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/BF01872848","volume":"2","author":"K Apt","year":"1988","unstructured":"Apt K, Francez N, Katz S: Appraising fairness in languages for distributed programming. Distribut. Comput. 2(4):226\u2013241 (1988).","journal-title":"Distribut. Comput."},{"key":"BF02252682_CR3","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"KR Apt","year":"1980","unstructured":"Apt, KR, Francez N, de Roever WP: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. 2:359\u2013385 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"BF02252682_CR4","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: Defining liveness. Inf. Process. Lett. 21:181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"BF02252682_CR5","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/214451.214456","volume":"3","author":"KM Chandy","year":"1985","unstructured":"Chandy KM, Lamport L: Distributed snapshots: determining global states of distributed systems. ACM Trans. Comp. Syst. (3):63\u201375 (1985)","journal-title":"ACM Trans. Comp. Syst."},{"key":"BF02252682_CR6","doi-asserted-by":"crossref","unstructured":"Chou CT, Gafni E: Understanding and verifying distributed algorithms using stratified decomposition. 7th Annual ACM Symposium on Principles of Distributed Computing 44\u201365 (1988)","DOI":"10.1145\/62546.62556"},{"key":"BF02252682_CR7","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"520","DOI":"10.1007\/BFb0028836","volume-title":"Proceedings FCT 85","author":"P Degano","year":"1985","unstructured":"Degano P, De Nicola R, Montanari U: Partial ordering for CCS. In: Budach L (ed.) Proceedings FCT 85. Lect. Notes Comput. Sci. Vol. 199. Springer, Berlin Heidelberg New York 1985, 520\u2013533"},{"key":"BF02252682_CR8","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra EW: Guarded commands, nondeterminancy and formal derivation of programs. Commun. ACM 18:453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"BF02252682_CR9","unstructured":"Dijkstra EW: The distributed snapshot algorithm of K.M. Chandy and L. Lamport. EWD864a"},{"key":"BF02252682_CR10","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","volume":"2","author":"T Elrad","year":"1982","unstructured":"Elrad T, Francez N: Decomposition of distributed programs into communication-closed layers. Sci. Comput Programm 2:155\u2013173 (1982)","journal-title":"Sci. Comput Programm"},{"key":"BF02252682_CR11","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"EA Emerson","year":"1983","unstructured":"Emerson EA: Alternative semantics for temporal logic. Theor. Comput. Sci. 26:121\u2013130 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"BF02252682_CR12","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson EA, Halpern JY: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. J. ACM 33:151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"BF02252682_CR13","volume-title":"Texts and monographs in computer science","author":"N Francez","year":"1986","unstructured":"Francez N:Fairness. In: Gries D (ed.), Texts and monographs in computer science. Springer, Berlin Heidelberg New York 1986"},{"key":"BF02252682_CR14","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0019-9958(85)80014-0","volume":"66","author":"O Gr\u00fcmberg","year":"1985","unstructured":"Gr\u00fcmberg O, Francez N, Makowski JA, de Roever WP: A proof rule for termination of guarded commands. Inf. Contr. 66:83\u2013102 (1985)","journal-title":"Inf. Contr."},{"key":"BF02252682_CR15","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare CAR: Communicating sequential processes. Commun. ACM 21:666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"BF02252682_CR16","doi-asserted-by":"crossref","unstructured":"Janicki R, Koutny M: Towards a theory of simulations for verification of concurrent systems. In: Odijk EM, Rem M, Syre JC (eds), PARLE '89, Lect Notes Comput Sci 366:73\u201388 (1989)","DOI":"10.1007\/3-540-51285-3_34"},{"issue":"3","key":"BF02252682_CR17","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0304-3975(90)90096-Z","volume":"75","author":"S Katz","year":"1990","unstructured":"Katz S, Peled D: Interleaving set temporal logic. Theor. Comput. Sci. 75(3):263\u2013287 (1990). Preliminary version in Proceedings of the 6th Annual ACM Symposium on Prinicples of Distributed Computing, Vancouver, Canada 1987, pp. 178\u2013190","journal-title":"Theor. Comput. Sci."},{"key":"BF02252682_CR18","doi-asserted-by":"crossref","unstructured":"Katz S, Peled D: Defining conditional independence using collapses, to appear in Theor. Comput. Sci. Preliminary version in Workshop on Semantics for Concurrency Leicester England 1990","DOI":"10.1007\/978-1-4471-3860-0_16"},{"key":"BF02252682_CR19","series-title":"Lect. Notes Comput. Sci.","first-page":"489","volume-title":"Proceedings of Workshop on Linear Time, Branching Time and Partial Orders, in Logics and Models for Concurrency","author":"S Katz","year":"1988","unstructured":"Katz S, Peled D: An efficient verification method for parallel and distributed programs. Proceedings of Workshop on Linear Time, Branching Time and Partial Orders, in Logics and Models for Concurrency. Lect. Notes Comput. Sci. vol. 354. Springer, Berlin Heidelberg New York 1988, 489\u2013507"},{"key":"BF02252682_CR20","doi-asserted-by":"crossref","unstructured":"Kwiatkowska MZ: Fairness for Non-Interleaving Concurrency. Phd Thesis, Department of Computing Studies Leicester 1989","DOI":"10.1007\/BF01887206"},{"key":"BF02252682_CR21","series-title":"Lect Notes Comput Sci","first-page":"454","volume-title":"Distributed systems \u2014 Methods and tools for specification. An advanced course. Munich","author":"L Lamport","year":"1985","unstructured":"Lamport L: Paradigms for distributed programs: computing global states. In: Paul M, Siegart H (eds) Distributed systems \u2014 Methods and tools for specification. An advanced course. Munich. Lect Notes Comput Sci vol. 190. Springer, Berlin Heidelberg New York 1985, pp 454\u2013468"},{"key":"BF02252682_CR22","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/3-540-10843-2_22","volume":"115","author":"D Lehman","year":"1981","unstructured":"Lehman D, Pnueli A, Stavi J: Impartiality, justice and fairness: the ethics of concurrent termination. Proc. of 8th International colloquium on Automata, Languages and Programming. Lect Notes Comput Sci 115:264\u2013277 (1981)","journal-title":"Lect Notes Comput Sci"},{"key":"BF02252682_CR23","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A: Verification of concurrent programs: the temporal framework. In: Boyer RS, Moore JS (eds) The correctness problem in computer science. Academic Press 1981, pp 215\u2013273","DOI":"10.21236\/ADA106750"},{"key":"BF02252682_CR24","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A: How to cook a temporal proof system for your pet language. 10th Symposium on Principles of Programming Languages. Austin Texas 1983, pp 141\u2013154","DOI":"10.1145\/567067.567082"},{"key":"BF02252682_CR25","doi-asserted-by":"crossref","first-page":"534","DOI":"10.1007\/BFb0035782","volume":"372","author":"Z Manna","year":"1989","unstructured":"Manna Z, Pnueli A: Completing the temporal picture. Proceedings 16th International Colloqium on Automata, Languages and Programming. Lect Notes Comput Sci 372:534\u2013558 (1989)","journal-title":"Lect Notes Comput Sci"},{"key":"BF02252682_CR26","first-page":"279","volume":"255","author":"A Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz A: Trace semantics, Proceedings of advances in Petri nets 1986. Bad Honnel. Lect Notes Comput Sci 255:279\u2013324 (1987)","journal-title":"Lect Notes Comput Sci"},{"key":"BF02252682_CR27","doi-asserted-by":"crossref","unstructured":"Owicki S, Lamport L: Proving liveness properties of concurrent programs. ACM Trans Program Lang Syst 4:455\u2013495","DOI":"10.1145\/357172.357178"},{"key":"BF02252682_CR28","doi-asserted-by":"crossref","unstructured":"Peled D, Katz S, Pnueli A: Specifying and Proving Serializability in Temporal Logic. Proceedings of 6th annual IEEE symposium on Logic in Computer Science. Amsterdam 1991, pp 232\u2013245","DOI":"10.1109\/LICS.1991.151648"},{"key":"BF02252682_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/BFb0032058","volume-title":"17th International Colloquium on Automata, Languages and Programming. Warwick University England July 1990","author":"D Peled","year":"1990","unstructured":"Peled D, Pnueli A: Proving partial order liveness properties. 17th International Colloquium on Automata, Languages and Programming. Warwick University England July 1990. Lect Notes Comput Sci, vol. 443. Springer, Berlin Heidelberg New York 1990, pp 553\u2013571"},{"issue":"3","key":"BF02252682_CR30","doi-asserted-by":"crossref","first-page":"297","DOI":"10.3233\/FI-1988-11307","volume":"11","author":"W Penczek","year":"1988","unstructured":"Penczek W: A temporal logic for event structures, Fundamenta Informaticae, Vol. 11 (3), 297\u2013326 (1988)","journal-title":"Fundamenta Informaticae"},{"key":"BF02252682_CR31","series-title":"Schriften des IIM","volume-title":"Kommunikation mit Automaten","author":"CA Petri","year":"1962","unstructured":"Petri CA: Kommunikation mit Automaten. Bonn: Institut f\u00fcr Instrumentelle Mathematik, Schriften des IIM Nr. 2 1962"},{"key":"BF02252682_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1007\/BFb0027047","volume-title":"Current Trends in Concurrency","author":"A Pnueli","year":"1986","unstructured":"Pnueli A: Applications of temporal logic to the specification and verification of reactive systems, a survey of current trends, in Current Trends in Concurrency. Lect Notes Comput Sci, vol. 224. Springer, Berlin Heidelberg New York 1986, pp 510\u2013584"},{"key":"BF02252682_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/3-540-13345-3_37","volume-title":"11th ICALP, Antwerp Belgium","author":"W Reisig","year":"1984","unstructured":"Reisig W: Partial order semantics versus interleaving semantics for CSP like languages and its impact on fairness, 11th ICALP, Antwerp Belgium. Lect Notes Comput Sci 172. Springer, Berlin Heidelberg New York 1984, pp 403\u2013413"},{"key":"BF02252682_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/3-540-50403-6_37","volume-title":"CONCURRENCY 88","author":"W Reisig","year":"1988","unstructured":"Reisig W: Temporal logic and causality in concurrent systems. In: Vogt FH (ed) CONCURRENCY 88. Lect Notes Comput Sci, vol 335. Springer, Berlin Heidelberg New York 1988, pp 121\u2013139"},{"key":"BF02252682_CR35","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 3rd International Workshop on Distributed Algorithms","author":"FA Stomp","year":"1989","unstructured":"Stomp FA, deRoever WP: Designing distributed algorithms by means of formal sequentially phased reasoning, Proceedings of the 3rd International Workshop on Distributed Algorithms. Lect Notes Comput Sci, vol 392. Springer, Berlin Heidelberg New York 1989"},{"key":"BF02252682_CR36","unstructured":"Valmari A: Stubborn sets for reduced state space generation, 10th International Conference on Application and Theory of Petri Nets. Bonn 1989 (2), pp 1\u201322"},{"key":"BF02252682_CR37","series-title":"Discrete Math","first-page":"25","volume-title":"Computer-aided Verification '90","author":"A Valmari","year":"1990","unstructured":"Valmari A: A stubborn attack on state explosion. In: Clarke E, Kurshan R (eds) Computer-aided Verification '90. Discrete Math, vol. 3. North-Holland, Amsterdam 1990, pp 25\u201342"}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02252682.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02252682\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02252682","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,20]],"date-time":"2021-07-20T04:56:03Z","timestamp":1626756963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02252682"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,9]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1992,9]]}},"alternative-id":["BF02252682"],"URL":"https:\/\/doi.org\/10.1007\/bf02252682","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"value":"0178-2770","type":"print"},{"value":"1432-0452","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,9]]}}}