{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T02:34:56Z","timestamp":1780626896709,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540646082","type":"print"},{"value":"9783540693390","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028727","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"17-28","source":"Crossref","is-referenced-by-count":59,"title":["Ten years of partial order reduction"],"prefix":"10.1007","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani, Partial order reduction in symbolic state space exploration. In Proceedings of the Conference on Computer Aided Verification (CAV'97), Haifa, Israel, June 1997.","DOI":"10.1007\/3-540-63166-6_34"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, O. Gr\u00fcmberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science 59 (1988), Elsevier, 115\u2013131.","journal-title":"Theoretical Computer Science"},{"issue":"8","key":"2_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, Graph-based algorithms for boolean function manipulation, IEEE Transactions on Computers, C-35(8), 1986, 677\u2013691.","journal-title":"IEEE Transactions on Computers"},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic model checking: 102\u00b0 states and beyond, Information and Computation, 98 (1992), 142\u2013170.","journal-title":"Information and Computation"},{"key":"2_CR5","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/3-540-61042-1_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C.T. Chou","year":"1996","unstructured":"C.T. Chou, D. Peled, Verifying a model-checking algorithm, Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1055, Springer, 1996, Passau, Germany. 241\u2013257."},{"key":"2_CR6","series-title":"LNCS","first-page":"52","volume-title":"Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke, E.A. Emerson, Design and synthesis of synchronous skeletons using branching time temporal logic, Logic of Programs, Yorktown Heights, NY, LNCS 131, Springer, 1981, 52\u201371."},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M.Y. Vardi, P. Wolper, M, Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal methods in system design 1 (1992) 275\u2013288.","journal-title":"Formal methods in system design"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, E.M. Clarke, Characterizing correctness properties of parallel programs using fixpoints, Automata, Languages and Programming, LNCS 85, Springer, 1980, 169\u2013181.","DOI":"10.1007\/3-540-10003-2_69"},{"key":"2_CR9","series-title":"ISTCS'95","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1109\/ISTCS.1995.377038","volume-title":"3rd Israel Symposium on Theory on Computing and Systems","author":"R. Gerth","year":"1995","unstructured":"R. Gerth, R. Kuiper, W. Penczek, D. Peled, A partial order approach to branching time logic model checking, ISTCS'95, 3rd Israel Symposium on Theory on Computing and Systems, IEEE press, 1995, Tel Aviv, Israel, 130\u2013139. A full version was accepted to Information and Computation."},{"key":"2_CR10","first-page":"3","volume-title":"PSTV95, Protocol Specification Testing and Verification","author":"R. Gerth","year":"1995","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, PSTV95, Protocol Specification Testing and Verification, Chapman & Hall, 1995, Warsaw, Poland, 3\u201318."},{"key":"2_CR11","first-page":"613","volume":"89","author":"R.J. Glabbeek van","year":"1989","unstructured":"R.J. van Glabbeek, W.P. Weijland, Branching time and abstraction in bisimulation semantics, Information Processing 89. Elsevier Science Publishers, 1989, 613\u2013618.","journal-title":"Information Processing"},{"key":"2_CR12","series-title":"LNCS","first-page":"176","volume-title":"Proc. 2nd Workshop on Computer Aided Verification","author":"P. Godefroid","year":"1990","unstructured":"P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. 2nd Workshop on Computer Aided Verification, LNCS 531, Springer, New Brunswick, NJ, 1990, 176\u2013185."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"P. Godefroid, D. Pirottin, Refining dependencies improves partial order verification methods, 5th Conference on Computer Aided Verification, LNCS 697, Elounda, Greece, 1993, 438\u2013449.","DOI":"10.1007\/3-540-56922-7_36"},{"key":"2_CR14","series-title":"ISSTA'96","first-page":"261","volume-title":"International Symposium on Software Testing and Analysis","author":"P. Godefroid","year":"1996","unstructured":"P. Godefroid, D. Peled, M. Staskauskas, Using partial order methods in the formal validation of industrial concurrent programs, 1996, ISSTA'96, International Symposium on Software Testing and Analysis, ACM Press, San Diego, California, USA, 261\u2013269."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"P. Godefroid, P. Wolper, A Partial approach to model checking, 6th Annual IEEE Symposium on Logic in Computer Science, 1991, Amsterdam, 406\u2013415.","DOI":"10.1109\/LICS.1991.151664"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann, P. Godefroid, D. Pirottin, Coverage preserving reduction strategies for reachability analysis, Proc. 12th Int. Conf on Protocol Specification, Testing, and Verification, INWG\/IFIP, Orlando, Florida, 1992, 349\u2013363.","DOI":"10.1016\/B978-0-444-89874-6.50028-3"},{"key":"2_CR17","unstructured":"G.J. Holzmann, D. Peled, An improvement in formal verification, 7th International Conference on Formal Description Techniques, Berne, Switzerland, 1994, 177\u2013194."},{"key":"2_CR18","unstructured":"S. Jha, D. Peled, Generalized stuttering equivalence for linear temporal logic specification, Submitted for publication."},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/BF02252682","volume":"6","author":"S. Katz","year":"1992","unstructured":"S. Katz, D. Peled, Verification of distributed programs using representative interleaving sequences, Distributed Computing 6 (1992), 107\u2013120. A preliminary version appeared in Temporal Logic in Specification, UK, 1987, LNCS 398, 21\u201343.","journal-title":"Distributed Computing"},{"key":"2_CR20","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(92)90054-J","volume":"101","author":"S. Katz","year":"1992","unstructured":"S. Katz, D. Peled, Defining conditional independence using collapses, Theoretical Computer Science 101 (1992), 337\u2013359, a preliminary version appeared in BCS-FACS Workshop on Semantics for Concurrency, Leicester, England, July 1990, Springer, 262\u2013280.","journal-title":"Theoretical Computer Science"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"I. Kokkarinen, A. Valmari, D. Peled, Relaxed visibility enhances partial order reduction, CAV'97, June 1997, Israel, LNCS 1254, 328\u2013339.","DOI":"10.1007\/3-540-63166-6_33"},{"key":"2_CR22","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"R.P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton, New Jersey, 1994."},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, V. Levin, M. Minea, D. Peled, H. Yenig\u00fcn, Static partial order reduction, 345\u2013357, 1997.","DOI":"10.1007\/BFb0054182"},{"key":"2_CR24","first-page":"657","volume-title":"Information Processing '83: Proc. of the IFIP 9th World Computer Congress,, Paris, France","author":"L. Lamport","year":"1983","unstructured":"L. Lamport, What good is temporal logic, in R.E.A. Mason (ed.), Information Processing '83: Proc. of the IFIP 9th World Computer Congress,, Paris, France, North-Holland, Amsterdam, 1983, 657\u2013668."},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, Checking that finite-state concurrent programs satisfy their linear specification, Proceedings of the 11th Annual Symposium on Principles of Programming Languages, ACM Press, 1984, 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnuefi, 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":"2_CR27","series-title":"LNCS","first-page":"279","volume-title":"Advances in Petri Nets 1986","author":"A. Mazurkiewicz","year":"1987","unstructured":"A. Mazurkiewicz, Trace theory, Advances in Petri Nets 1986, Bad Honnef, Germany, LNCS 255, Springer, 1987, 279\u2013324."},{"key":"2_CR28","unstructured":"R. Milner, A calculus of communicating system, LNCS, Springer, 92."},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"R. de Nicola, F. Vaandrager, Three logics for branching bisimulation, Logic in Computer Science '90, IEEE, 1990, 118\u2013129.","DOI":"10.1109\/LICS.1990.113739"},{"issue":"1-2","key":"2_CR30","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(96)00225-3","volume":"186","author":"D. Peled","year":"1997","unstructured":"D. Peled, On projective and separable properties, Theoretical Computer Science, 186(1-2), 1997, 135\u2013155.","journal-title":"Theoretical Computer Science"},{"key":"2_CR31","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(94)90009-4","volume":"126","author":"D. Peled","year":"1994","unstructured":"D. Peled, A. Pnueli, Proving partial order properties, Theoretical Computer Science, 126 (1994), 143\u2013182.","journal-title":"Theoretical Computer Science"},{"key":"2_CR32","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"5th Conference on Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"D. Peled, All from one, one for all, on model-checking using representatives, 5th Conference on Computer Aided Verification, Greece, 1993, LNCS, Springer, 409\u2013423."},{"key":"2_CR33","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D. Peled","year":"1996","unstructured":"D. Peled, Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design 8 (1996), 39\u201364. A preliminary version appeared in Computer Aided Verification 94, LNCS 818, Springer, Stanford, USA, 377\u2013390.","journal-title":"Formal Methods in System Design"},{"key":"2_CR34","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D. Peled","year":"1997","unstructured":"D. Peled, Th. Wilke, Stutter-invariant temporal properties are expressible without the nexttime operator, Information Processing Letters 63 (1997), 243\u2013246.","journal-title":"Information Processing Letters"},{"key":"2_CR35","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1007\/3-540-61604-7_78","volume-title":"7th International Conference on Concurrency Theory","author":"D. Peled","year":"1996","unstructured":"D. Peled, Th. Wilke, P. Wolper, An algorithmic approach for checking closure properties of w-Regular Languages, CONCUR'96, 7th International Conference on Concurrency Theory, Piza, Italy, LNCS 1119, Springer, August 1996, 596\u2013610. A full version accepted to Theoretical Computer Science."},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"J.P. Quielle, J. Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th International Symposium on Programming, 1981, 337\u2013350.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"2_CR37","series-title":"LNCS","first-page":"491","volume-title":"10th International Conference on Application and Theory of Petri Nets","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, Germany, 1989, LNCS 483, Springer, 491\u2013515."},{"key":"2_CR38","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"A. Valmari, A stubborn attack on state explosion. Formal Methods in System Design, 1 (1992), 297\u2013322.","journal-title":"Formal Methods in System Design"},{"key":"2_CR39","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Proceedings of CAV '93, 5th International Conference on Computer-Aided Verification","author":"A. Valmari","year":"1993","unstructured":"A. Valmari, On-the-fly verification with stubborn sets, Proceedings of CAV '93, 5th International Conference on Computer-Aided Verification, Elounda, Greece, LNCS 697, Springer 1993, pp. 397\u2013408."},{"key":"2_CR40","first-page":"213","volume-title":"POMIV'96, Partial Orders Methods in Verification","author":"A. Valmari","year":"1996","unstructured":"A. Valmari, Stubborn set methods for process algebras, POMIV'96, Partial Orders Methods in Verification, American Mathematical Society, DIMACS, Princeton, NJ, USA, 1996, 213\u2013232."},{"key":"2_CR41","first-page":"322","volume-title":"1st Annual IEEE Symposium on Logic in Computer Science","author":"M.Y. Vardi","year":"1986","unstructured":"M.Y. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, 1st Annual IEEE Symposium on Logic in Computer Science, 1986, Cambridge, England, 322\u2013331."},{"key":"2_CR42","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1109\/LICS.1996.561357","volume-title":"11th Annual IEEE Symposium on Logic in Computer Science","author":"B. Willems","year":"1996","unstructured":"B. Willems, P. Wolper, Partial-order methods for model-checking: from linear time to branching time, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, NJ, USA, 1996, 294\u2013303."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028727","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T01:44:45Z","timestamp":1736127885000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028727"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/bfb0028727","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}