{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T15:19:32Z","timestamp":1772205572662,"version":"3.50.1"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1993,4,1]],"date-time":"1993-04-01T00:00:00Z","timestamp":733622400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1993,4]]},"DOI":"10.1007\/bf01383879","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T03:29:35Z","timestamp":1112412575000},"page":"149-164","source":"Crossref","is-referenced-by-count":87,"title":["Using partial orders for the efficient verification of deadlock freedom and safety properties"],"prefix":"10.1007","volume":"2","author":[{"given":"Patrice","family":"Godefroid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Wolper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"4","author":"Z. Manna","year":"1984","unstructured":"Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs.Science of Computer Programming, 4:257?289 (1984).","journal-title":"Science of Computer Programming"},{"issue":"3","key":"CR2","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki and L. Lamport. Proving liveness properties of concurrent programs.ACM Transactions on Programming Languages and Systems, 4(3):455?495 (July 1982).","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"CR3","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems, 8(2):244?263 (January 1986).","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. InProceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pp. 97?107, New Orleans, January 1985.","DOI":"10.1145\/318593.318622"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. InProceedings of the 5th International Symposium on Programming. Lecture Notes in Computer Science, 137:337?351 (1981).","DOI":"10.1007\/3-540-11494-7_22"},{"key":"CR6","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. InProceedings of the symposium on Logic in Computer Science, pp. 322?331, Cambridge, June 1986."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J.-C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for branching semantics. InProceedings of the 12th International Colloquium on Automata, Language and Programming. Lecture Notes in Computer Science, (1991).","DOI":"10.1007\/3-540-54233-7_126"},{"key":"CR8","series-title":"Technical Report SPECTRE L12","volume-title":"On the verification of safety properties","author":"A. Bouajjani","year":"1990","unstructured":"A. Bouajjani, J.C. Fernandez, and N. Halbwachs. On the verification of safety properties. Technical Report SPECTRE L12, IMAG, Grenoble, March 1990."},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"C. Jard and T. Jeron. On-line model-checking for finite linear temporal logic specifications. InAutomatic Verification Methods for Finite State Systems, Proceedings of an International Workshop, Grenoble. Lecture Notes in Computer Science, 407:189?196 (1989).","DOI":"10.1007\/3-540-52148-8_16"},{"key":"CR10","first-page":"1","volume-title":"Proceedings of the International Congress on Logic, Method and Philosophy of Science 1960","author":"J.R. B\u00fcchi","year":"1962","unstructured":"J.R. B\u00fcchi. On a decision method in restricted second order arithmetic. InProceedings of the International Congress on Logic, Method and Philosophy of Science 1960. Stanford: Stanford University Press, 1962, pp. 1?12."},{"key":"CR11","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"M.O. Rabin. Decidability of second order theories and automata on infinite trees.Transactions of the AMS, 141:1?35 (1969).","journal-title":"Transactions of the AMS"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Shmuel Safra. On the complexity of omega-automata. InProceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains (October 1988).","DOI":"10.1109\/SFCS.1988.21948"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for B\u00fcchi automata with applications to temporal logic.Theoretical Computer Science, 49:217?237 (1987).","journal-title":"Theoretical Computer Science"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"P. Godefroid and P. Wolper. A partial approach to model checking. InProceedings of the 6th Symposium on Logic in Computer Science, pp. 406?415, Amsterdam, July 1991.","DOI":"10.1109\/LICS.1991.151664"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"A. Valmari. A stubborn attack on state explosion. InProceedings of the 2nd Workshop on Computer Aided Verification. Lecture Notes in Computer Science, 531:156?165 (1990).","DOI":"10.1007\/BFb0023729"},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"P. Godefroid. Using partial orders to improve automatic verification methods. InProceedings of the 2nd Workshop on Computer Aided Verification. Lecture Notes in Computer Science, 531:176?185 (1990).","DOI":"10.1007\/BFb0023731"},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"D.K. Probst and H.F. Li. Using partial-order semantics to avoid the state explosion problem in asynchronous systems. InProceedings of the 2nd Workshop on Computer Aided Verification. Lecture Notes in Computer Science, 531:146?155 (1990).","DOI":"10.1007\/BFb0023728"},{"key":"CR18","unstructured":"A. Valmari. Stubborn sets for reduced state space generation. InProceedings of the 10th International Conference on Application and Theory of Petri Nets, vol. 2, pp. 1?22, Bonn, 1989."},{"key":"CR19","unstructured":"A. Mazurkiewcz. Trace theory. InPetri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course. Lecture Notes in Computer Science, 255:279?324 (1986)."},{"key":"CR20","unstructured":"A. Valmari. Error detection by reduced reachability graph detection. InProceedings of the 9th European Workshop on Application and Theory of Petri Nets, pp. 95?112, Venice, 1988."},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. InProceedings of the 2nd Workshop on Computer Aided Verification. Lecture Notes in Computer Science, 531:233?242 (1990).","DOI":"10.1007\/BFb0023737"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, D. Pilaud, F. Ouabdesselam, and A.C. Glory. Specifying, programming and verifying real-time systems, using a synchronous declarative language. InWorkshop on Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science, 407:213?231 (1989).","DOI":"10.1007\/3-540-52148-8_18"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"J.C. Fernandez and L. Mounier. On the fly verification of behavioural equivalences and preorders. InProceedings of the 3rd Workshop on Computer Aided Verification. Lecture Notes in Computer Science, 575:181?191, (1991).","DOI":"10.1007\/3-540-55179-4_18"},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"C. Jard and T. Jeron. Bounded-memory algorithms for verification on the fly. InProceedings of the 3rd Workshop on Computer Aided Verification. Lecture Notes in Computer Science, 575:192?202 (1991).","DOI":"10.1007\/3-540-55179-4_19"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"H. Gaifman. Modeling concurrency by partial orders and nonlinear transition systems. InLinear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Lecture Notes in Computer Science, 354:467?488 (1988).","DOI":"10.1007\/BFb0013031"},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"W. Reisig.Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-69968-9"},{"key":"CR27","unstructured":"S. Graf and B. Steffen. Using interface specifications for compositional reduction. InProceedings of the 2nd Workshop on Computer Aided Verification. Lecture Notes in Computer Science, 531:186?196 (1990)."},{"key":"CR28","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"B. Alpern and F.B. Schneider. Recognizing safety and liveness.Distributed Computing, 2:117?126 (1987).","journal-title":"Distributed Computing"},{"issue":"2","key":"CR29","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1002\/spe.4380180203","volume":"18","author":"G. Holzmann","year":"1988","unstructured":"G. Holzmann. An improved protocol reachability analysis technique.Software Practice and Experience, 18(2):137?161 (February 1988).","journal-title":"Software Practice and Experience"},{"key":"CR30","volume-title":"Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"G. Holzmann.Design and Validation of Computer Protocols. Englewood Cliffs, NJ: Prentice-Hall International Editions, 1991."},{"key":"CR31","volume-title":"Proceedings of the 12th International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida","author":"G.J. Holzmann","year":"1992","unstructured":"G.J. Holzmann, P. Godefroid, and D. Pirottin. Coverage preserving reduction strategies for reachability analysis. InProceedings of the 12th International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida. North-Holland, Amsterdam, 1992."},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"P. Godefroid, G.J. Holzmann, and D. Pirottin. State space caching revisited. InProceedings of the 4th Workshop on Computer Aided Verification, Montreal, June 1992.","DOI":"10.1007\/3-540-56496-9_15"},{"key":"CR33","unstructured":"P. Godefroid and F. Kabanza. An efficient reactive planner for synthesizing reactive plans. InProceedings of AAAI-91, Vol. 2, pp. 640?645, Anaheim, July 1991."},{"key":"CR34","doi-asserted-by":"crossref","unstructured":"P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. InProceedings of the 3rd Workshop on Computer Aided Verification. Lecture Notes in Computer Science, 575:332?342 (1991).","DOI":"10.1007\/3-540-55179-4_32"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383879.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383879\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383879","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:25:18Z","timestamp":1586190318000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383879"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,4]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,4]]}},"alternative-id":["BF01383879"],"URL":"https:\/\/doi.org\/10.1007\/bf01383879","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,4]]}}}