{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T04:36:06Z","timestamp":1778301366347,"version":"3.51.4"},"reference-count":46,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1994,4,1]],"date-time":"1994-04-01T00:00:00Z","timestamp":765158400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7047,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1994,4]]},"DOI":"10.1016\/0304-3975(94)90009-4","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:47:37Z","timestamp":1027655257000},"page":"143-182","source":"Crossref","is-referenced-by-count":32,"title":["Proving partial order properties"],"prefix":"10.1016","volume":"126","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(94)90009-4_BIB1","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/BF00289262","article-title":"Recursive assertions and parallel programs","volume":"15","author":"Apt","year":"1981","journal-title":"Acta Inform."},{"key":"10.1016\/0304-3975(94)90009-4_BIB2","series-title":"Mathematical Theory of Program Correctness","author":"de Bakker","year":"1980"},{"key":"10.1016\/0304-3975(94)90009-4_BIB3","series-title":"Concurrency Control and Recovery in Database Systems","author":"Bernstein","year":"1987"},{"key":"10.1016\/0304-3975(94)90009-4_BIB4","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0304-3975(87)90005-3","article-title":"Repeated snapshots in distributed systems with synchronous communications and their implementations in CSP","volume":"49","author":"Boug\u00e9","year":"1987","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)90009-4_BIB5","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/214451.214456","article-title":"Distributed snapshots: determining the global state of distributed systems","volume":"3","author":"Chandy","year":"1985","journal-title":"ACM Trans. Comput. Systems"},{"key":"10.1016\/0304-3975(94)90009-4_BIB6","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/BF00571463","article-title":"Program proving: coroutines","volume":"2","author":"Clint","year":"1973","journal-title":"Acta Inform."},{"key":"10.1016\/0304-3975(94)90009-4_BIB7","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","article-title":"Soundness and completeness of an axiom systems for program verification","volume":"7","author":"Cook","year":"1978","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0304-3975(94)90009-4_BIB8","series-title":"Technical Report EWD123","first-page":"43","article-title":"Cooperating Sequential Processes","author":"Dijkstra","year":"1965"},{"key":"10.1016\/0304-3975(94)90009-4_BIB9","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","article-title":"Guarded commands, nondeterminancy and formal derivation of programs","volume":"18","author":"Dijkstra","year":"1975","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(94)90009-4_BIB10","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","article-title":"Decomposition of distributed programs into communication-closed layers","volume":"2","author":"Elrad","year":"1982","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0304-3975(94)90009-4_BIB11","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","article-title":"Using branching time temporal logic to synthesize synchronization skeletons","volume":"2","author":"Emerson","year":"1982","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0304-3975(94)90009-4_BIB12","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"\u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic","volume":"33","author":"Emerson","year":"1986","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(94)90009-4_BIB13","series-title":"Fairness","author":"Francez","year":"1986"},{"key":"10.1016\/0304-3975(94)90009-4_BIB14","first-page":"46","article-title":"Generalized fair termination","author":"Francez","year":"1984","journal-title":"Proc. 11th Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(94)90009-4_BIB15","first-page":"72","article-title":"Partial order models of concurrency and computation of functions","author":"Gaifman","year":"1987","journal-title":"Symp. on Logic in Computer Science"},{"key":"10.1016\/0304-3975(94)90009-4_BIB16","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0019-9958(85)80014-0","article-title":"A proof rule for termination of guarded commands","volume":"66","author":"Gr\u00fcmberg","year":"1985","journal-title":"Inform. Control"},{"key":"10.1016\/0304-3975(94)90009-4_BIB17","article-title":"First-Order Dynamic Logic","volume":"Vol. 68","author":"Harel","year":"1979"},{"key":"10.1016\/0304-3975(94)90009-4_BIB18","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","article-title":"Communicating sequential processes","volume":"21","author":"Hoare","year":"1978","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(94)90009-4_BIB19","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0304-3975(86)90177-5","article-title":"Concurrent and maximally concurrent evolution of non-sequential system","volume":"43","author":"Janicki","year":"1986","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"10.1016\/0304-3975(94)90009-4_BIB20","first-page":"21","article-title":"Interleaving set temporal logic","volume":"75","author":"Katz","year":"1987","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)90009-4_BIB21","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/BF02252682","article-title":"Verification of distributed programs using representative interleaving sequences","volume":"6","author":"Katz","year":"1992","journal-title":"Distrib. Comput."},{"key":"10.1016\/0304-3975(94)90009-4_BIB22","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/0304-3975(92)90054-J","article-title":"Defining conditional independence using collapses","volume":"101","author":"Katz","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)90009-4_BIB23","series-title":"Ph.D. Thesis","article-title":"Fairness for non-interleaving concurrency","author":"Kwiatkowska","year":"1989"},{"key":"10.1016\/0304-3975(94)90009-4_BIB24","first-page":"454","article-title":"Paradigms for distributed programs: computing global states","volume":"Vol. 190","author":"Lamport","year":"1985"},{"key":"10.1016\/0304-3975(94)90009-4_BIB25","first-page":"264","article-title":"Impartiality, justice and fairness: The ethics of concurrent termination","volume":"Vol. 115","author":"Lehman","year":"1981"},{"key":"10.1016\/0304-3975(94)90009-4_BIB26","series-title":"The Correctness Problem in Computer Science","first-page":"215","article-title":"Verification of concurrent programs: the temporal framework","author":"Manna","year":"1981"},{"key":"10.1016\/0304-3975(94)90009-4_BIB27","first-page":"162","article-title":"Verification of concurrent programs, a temporal proof system","author":"Manna","year":"1982","journal-title":"Proc. 4th School on Advanced Programming"},{"key":"10.1016\/0304-3975(94)90009-4_BIB28","first-page":"141","article-title":"How to cook a temporal proof system for your pet language","author":"Manna","year":"1983","journal-title":"Proc. Symp. on Principles on Programming Languages"},{"key":"10.1016\/0304-3975(94)90009-4_BIB29","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","article-title":"Adequate proof principles for invariance and liveness properties of concurrent programs","volume":"4","author":"Manna","year":"1984","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0304-3975(94)90009-4_BIB30","first-page":"201","article-title":"The anchored version of the temporal framework","volume":"Vol. 354","author":"Manna","year":"1988"},{"key":"10.1016\/0304-3975(94)90009-4_BIB31","doi-asserted-by":"crossref","first-page":"534","DOI":"10.1007\/BFb0035782","article-title":"Completing the temporal picture","volume":"Vol. 372","author":"Manna","year":"1989","journal-title":"Proc. 16th Internat. Coll. on Automata, Languages and Programming"},{"key":"10.1016\/0304-3975(94)90009-4_BIB32","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","article-title":"Synthesis of communicating processes from temporal logic specifications","volume":"6","author":"Manna","year":"1984","journal-title":"ACM Trans. Programming Languages Systems"},{"key":"10.1016\/0304-3975(94)90009-4_BIB33","first-page":"279","article-title":"Trace semantics","volume":"Vol. 255","author":"Mazurkiewicz","year":"1987"},{"key":"10.1016\/0304-3975(94)90009-4_BIB34","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/0304-3975(89)90052-2","article-title":"Concurrent processes and inevitability","volume":"64","author":"Mazurkiewicz","year":"1989","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)90009-4_BIB35","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","article-title":"Petri nets, event structures and domains","volume":"13","author":"Nielsen","year":"1981","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)90009-4_BIB36","first-page":"73","article-title":"A consistent and complete deductive system for the verification of parallel programs","author":"Owicki","year":"1976","journal-title":"Proc. 8th Ann. Symp. on Theory of Computing"},{"key":"10.1016\/0304-3975(94)90009-4_BIB37","series-title":"6th IEEE Ann. Symp. on Logic in Computer Science","first-page":"232","article-title":"Specifying and proving serializability in temporal logic","author":"Peled","year":"1991"},{"key":"10.1016\/0304-3975(94)90009-4_BIB38","article-title":"Kommunikation mit Automaten","author":"Petri","year":"1962","journal-title":"Bonn: Institut f\u00fcr Instrumentelle Matematik, Schriften des IIm Nr. 2"},{"key":"10.1016\/0304-3975(94)90009-4_BIB39","first-page":"23","article-title":"A temporal logic for reasoning about partially ordered computations","author":"Pinter","year":"1984","journal-title":"Proc. 3rd ACM Symp. on Principles of Distributed Computing"},{"key":"10.1016\/0304-3975(94)90009-4_BIB40","first-page":"652","article-title":"On the synthesis of an asynchronous reactive module","volume":"Vol. 372","author":"Pnueli","year":"1989"},{"key":"10.1016\/0304-3975(94)90009-4_BIB41","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF01379149","article-title":"Modeling concurrency with partial orders","volume":"15","author":"Pratt","year":"1986","journal-title":"Internat. J. Parallel Programming"},{"key":"10.1016\/0304-3975(94)90009-4_BIB42","first-page":"121","article-title":"Temporal logic and causality in concurrent systems","volume":"Vol. 335","author":"Reisig","year":"1988"},{"key":"10.1016\/0304-3975(94)90009-4_BIB43","series-title":"Theory of Recursive Functions and Effective Computability","author":"Rogers","year":"1967"},{"key":"10.1016\/0304-3975(94)90009-4_BIB44","series-title":"Mathematical Logic","author":"Shoenfield","year":"1976"},{"key":"10.1016\/0304-3975(94)90009-4_BIB45","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1016\/0890-5401(89)90004-7","article-title":"The \u03bc-calculus as an assertion-language for fairness arguments","volume":"82","author":"Stomp","year":"1989","journal-title":"Inform. Comput."},{"key":"10.1016\/0304-3975(94)90009-4_BIB46","first-page":"26","article-title":"Elementary net systems","volume":"Vol. 254","author":"Thiagarajan","year":"1987"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397594900094?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397594900094?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T04:27:00Z","timestamp":1555129620000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397594900094"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,4]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994,4]]}},"alternative-id":["0304397594900094"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(94)90009-4","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1994,4]]}}}