{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T15:54:33Z","timestamp":1781020473111,"version":"3.54.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"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":[[1996,1]]},"DOI":"10.1007\/bf00121262","type":"journal-article","created":{"date-parts":[[2004,11,1]],"date-time":"2004-11-01T08:07:59Z","timestamp":1099296479000},"page":"39-64","source":"Crossref","is-referenced-by-count":108,"title":["Combining partial order reductions with on-the-fly model-checking"],"prefix":"10.1007","volume":"8","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1145\/78942.78948","volume":"12","author":"S. Aggarwal","year":"1990","unstructured":"S. Aggarwal, C. Courcoubetis, and P. Wolper, ?Adding Liveness Properties to Coupled Finite State Machines,? ACM Transactions on Programming Languages and Systems, Vol. 12, pp. 303?339, 1990.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/BF01872848","volume":"2","author":"K. Apt","year":"1988","unstructured":"K. Apt, N. Francez, and S. Katz, ?Appraising fairness in languages for distributed programming,? Distributed Computing, Vol. 2, pp. 226?241, 1988.","journal-title":"Distributed Computing"},{"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, Vol. 8, pp. 244?263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR4","first-page":"1","volume-title":"On a decision method in restricted second order arithmetic","author":"J.R. B\u00fcchi","year":"1960","unstructured":"J.R. B\u00fcchi, ?On a decision method in restricted second order arithmetic,? in E. Nagel et al. (Eds.), Proceeding of the International Congress on Logic, Methodology and Philosophy of Science, Stanford, CA, Stanford University Press, pp. 1?11, 1960."},{"key":"CR5","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis, ?Memory-efficient algorithms for the verification of temporal properties,? Formal Methods in System Design, Vol. 1, pp. 275?288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"J.C. Fernandez, L. Mounier, C. Jard, and T. Jeron, ?On-the-fly verification of finite transition systems,? Formal Methods in System Design, Kluwer, Vol. 1, pp. 251?273, 1992.","DOI":"10.1007\/BF00121127"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"P. Godefroid, ?Using partial orders to improve automatic verification methods,? in E.M. Clarke and R.P. Kurshan (Eds.), Computer Aided Verification 1990, DIMACS, Vol. 3, pp. 321?339, 1991.","DOI":"10.1090\/dimacs\/003\/21"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"P. Godefroid and D. Pirottin, ?Refining Dependencies Improves Partial-Order Verification Methods,? 5th International Conference on Computer Aided Verification, Elounda, Greece. Lecture Notes in Computer Science 697, Springer-Verlag, 1993, pp. 438?449.","DOI":"10.1007\/3-540-56922-7_36"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"P. Godefroid and P. Wolper, ?A Partial Approach to Model Checking,? 6th LICS, Amsterdam, pp. 406?415. Also in Information and Computation, Vol. 110, No. 2, pp. 305?326, 1991.","DOI":"10.1006\/inco.1994.1035"},{"key":"CR10","unstructured":"G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall Software Series, 1992."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann, P. Godefroid, and D. Pirottin, ?Coverage preserving reduction strategies for reachability analysis,? Proc. IFIP, Symp. on Protocol Specification, Testing, and Verification, Orlando, U.S.A., June 1992, pp. 349?364.","DOI":"10.1016\/B978-0-444-89874-6.50028-3"},{"key":"CR12","unstructured":"G.J. Holzmann and D. Peled, ?An Improvement in Formal Verification,? 7th International Conference on Formal Description Techniques, Berne, Switzerland, 1994, pp. 177?194."},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"S. Katz and D. Peled, ?Verification of distributed programs using representative interleaving sequences,? Distributed Computing, Vol. 6, pp. 107?120, 1992. A preliminary version, titled An Efficient Verification Method for Parallel and Distributed Programs, appeared in: Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, The Netherlands, May\/June 1988, Lecture Notes in Computer Science, Springer, Vol. 354, pp. 489?507.","DOI":"10.1007\/BFb0013032"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/0304-3975(92)90054-J","volume":"101","author":"S. Katz","year":"1992","unstructured":"S. Katz and D. Peled, ?Defining conditional independence using collapses,? Theoretical Computer Science, Vol. 101, pp. 337?359, 1992. A preliminary version appeared in BCS-FACS Workshop on Semantics for Concurrency, Leicester, England, July 1990, Springer, pp. 262?280.","journal-title":"Theoretical Computer Science"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, ?Reducibility in analysis of coordination,? Lecture Notes in Communication and Information, Springer, Vol. 103, pp. 19?39, 1987.","DOI":"10.1007\/BFb0042302"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF01887206","volume":"1","author":"M.Z. Kwiatkowska","year":"1989","unstructured":"M.Z. Kwiatkowska, ?Event Fairness and Non-Interleaving Concurrency,? Formal Aspects of Computing, Vol. 1, pp. 213?228, 1989.","journal-title":"Formal Aspects of Computing"},{"key":"CR17","unstructured":"L. Lamport, ?What good is temporal logic,? IFIP Congress, North Holland, 1983, pp. 657?668, in Computer Science 115."},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli, ?Checking that finite-state concurrent programs satisfy their linear specification,? 11th ACM POPL, pp. 97?107, 1984.","DOI":"10.1145\/318593.318622"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, ?How to cook a temporal proof system for your pet language,? 9th ACM Symposium on Principles on Programming Languages, Austin, Texas, 1983, pp. 141?151.","DOI":"10.1145\/567067.567082"},{"key":"CR20","series-title":"Lecture Notes in Computer Science","first-page":"279","volume-title":"Advances in Petri Nets","author":"A. Mazurkiewicz","year":"1986","unstructured":"A. Mazurkiewicz, Trace Theory, in Advances in Petri Nets 1986, W. Brauer, W. Reisig, and G. Rozenberg (Eds.), Bad Honnef, Germany, Lecture Notes in Computer Science 255, Springer, 1987, pp. 279?324."},{"key":"CR21","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0304-3975(94)90009-4","volume":"126","author":"D. Peled","year":"1994","unstructured":"D. Peled and A. Pnueli, ?Proving partial order properties,? Theoretical Computer Science, Vol. 126, pp. 143?182, 1994.","journal-title":"Theoretical Computer Science"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"D. Peled, ?All from one, one for all, on model-checking using representatives,? 5th International Conference on Computer Aided Verification, Greece, 1993. Lecture Notes in Computer Science, Springer, pp. 409?423.","DOI":"10.1007\/3-540-56922-7_34"},{"key":"CR23","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R.S. Street","year":"1982","unstructured":"R.S. Street, ?Propositional Dynamic Logic of Looping and Converse,? Information and Control, Vol. 54, pp. 121?141, 1982.","journal-title":"Information and Control"},{"key":"CR24","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, Bonn, Vol. 2, pp. 1?22, 1989.","journal-title":"10th International Conference on Application and Theory of Petri Nets"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"A. Valmari, ?A Stubborn attack on state explosion,? in E.M. Clarke and R.P. Kurshan (Eds.), CAV'90, DIMACS. Vol. 3, pp. 25?42, 1991.","DOI":"10.1090\/dimacs\/003\/04"},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"A. Valmari, ?On-The-Fly Verification of Stubborn Sets,? 5th CAV, Greece, 1993. Lecture Notes in Computer Science, Springer, Vol. 697, pp. 397?408.","DOI":"10.1007\/3-540-56922-7_33"},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"P. Wolper, M.Y. Vardi, and A.P. Sistla, ?Reasoning about infinite computation paths,? Proceedings of 24th IEEE Symposium on Foundation of Computer Science, Tuscan, 1983, pp. 185?194.","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00121262.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00121262\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00121262","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,29]],"date-time":"2023-04-29T21:14:03Z","timestamp":1682802843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00121262"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,1]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1996,1]]}},"alternative-id":["BF00121262"],"URL":"https:\/\/doi.org\/10.1007\/bf00121262","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,1]]}}}