{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:28Z","timestamp":1776305308905,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_6","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:05:28Z","timestamp":1526616328000},"page":"173-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Partial-Order Reduction"],"prefix":"10.1007","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"6_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/3-540-63166-6_34","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Alur","year":"1997","unstructured":"Alur, R., Brayton, R., Henzinger, T., Qadeer, S., Rajamani, S.: Partial order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01254, pp.\u00a0340\u2013351. Springer, Heidelberg (1997)"},{"key":"6_CR2","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-540-73420-8_16","volume-title":"Intl. Colloquium on Automata, Languages and Programming (ICALP)","author":"D. Bosnacki","year":"2007","unstructured":"Bosnacki, D., Elkind, E., Genest, B., Peled, D.: On commutativity based edge lean search. In: Arge, L., Cachin, C., Jurdzinski, T., Tarlecki, A. (eds.) Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a04596, pp.\u00a0158\u2013170. Springer, Heidelberg (2007)"},{"issue":"1\u20132","key":"6_CR3","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M. Browne","year":"1988","unstructured":"Browne, M., Clarke, E., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1\u20132), 115\u2013131 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR4","series-title":"LNCS","first-page":"241","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"C. Chou","year":"1996","unstructured":"Chou, C., Peled, D.: Verifying a model-checking algorithm. In: Margaria, T., Steffen, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01055, pp.\u00a0241\u2013257. Springer, Heidelberg (1996)"},{"key":"6_CR5","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"issue":"2\u20133","key":"6_CR6","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des. 1(2\u20133), 275\u2013288 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"6_CR7","first-page":"118","volume-title":"Symp. on Logic in Computer Science","author":"R. Nicola De","year":"1990","unstructured":"De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. In: Symp. on Logic in Computer Science, vol.\u00a0LICS, pp.\u00a0118\u2013129. IEEE, Piscataway (1990)"},{"key":"6_CR8","series-title":"EATCS Monographs in Theoretical Computer Science","volume-title":"Unfoldings\u2014a partial-order approach to model checking","author":"J. Esparza","year":"2008","unstructured":"Esparza, J., Heljanko, K.: Unfoldings\u2014a partial-order approach to model checking. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (2008)"},{"key":"6_CR9","first-page":"130","volume-title":"Israel Symp. on the Theory of Computing and Systems (ISTCS)","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Kuiper, R., Penczek, W., Peled, D.: A partial order approach to branching time logic model checking. In: Israel Symp. on the Theory of Computing and Systems (ISTCS), pp.\u00a0130\u2013139. IEEE, Piscataway (1995). Full version in Information and Computation 150(2), 132\u2013152 (1999)"},{"key":"6_CR10","series-title":"IFIP Conference Proceedings","first-page":"3","volume-title":"Intl. Symp. on Protocol Specification, Testing and Verification (PSTV)","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) Intl. Symp. on Protocol Specification, Testing and Verification (PSTV). IFIP Conference Proceedings, vol.\u00a038, pp.\u00a03\u201318. Chapman & Hall, London (1995)"},{"key":"6_CR11","first-page":"613","volume-title":"Information Processing 89, Proc. of the IFIP World Computer Congress","author":"R. Glabbeek van","year":"1989","unstructured":"van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics. In: Ritter, G.X. (ed.) Information Processing 89, Proc. of the IFIP World Computer Congress, pp.\u00a0613\u2013618. North-Holland\/IFIP, Amsterdam (1989)"},{"key":"6_CR12","series-title":"Software Engineering Notes","first-page":"261","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P., Peled, D., Staskauskas, M.: Using partial order methods in the formal validation of industrial concurrent programs. In: Zeil, S.J. (ed.) Intl. Symp. on Software Testing and Analysis (ISSTA). Software Engineering Notes, vol.\u00a021, pp.\u00a0261\u2013269. ACM Press, New York (1996)"},{"key":"6_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-56922-7_36","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"P. Godefroid","year":"1993","unstructured":"Godefroid, P., Pirottin, D.: Refining dependencies improves partial order verification methods. In: Courcoubetis, C. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0697, pp.\u00a0438\u2013449. Springer, Heidelberg (1993)"},{"key":"6_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/3-540-55179-4_32","volume-title":"Intl. Workshop on Computer-Aided Verification (CAV)","author":"P. Godefroid","year":"1991","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Larsen, K.G., Skou, A. (eds.) Intl. Workshop on Computer-Aided Verification (CAV). LNCS, vol.\u00a0575, pp.\u00a0332\u2013342. Springer, Heidelberg (1991)"},{"issue":"2","key":"6_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01383879","volume":"2","author":"P. Godefroid","year":"1993","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. Form. Methods Syst. Des. 2(2), 149\u2013164 (1993)","journal-title":"Form. Methods Syst. Des."},{"key":"6_CR16","series-title":"IFIP Transactions","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/B978-0-444-89874-6.50028-3","volume-title":"Intl. Symp. on Protocol Specification, Testing and Verification (PSTV)","author":"G. Holzmann","year":"1992","unstructured":"Holzmann, G., Godefroid, P., Pirottin, D.: Coverage preserving reduction strategies for reachability analysis. In: Linn, R.J. Jr., Uyar, M.\u00dc. (eds.) Intl. Symp. on Protocol Specification, Testing and Verification (PSTV). IFIP Transactions, vol.\u00a0C-8, pp.\u00a0349\u2013363. North-Holland, Amsterdam (1992)"},{"key":"6_CR17","series-title":"IFIP Conference Proceedings","first-page":"197","volume-title":"Intl. Conf. on Formal Description Techniques (FORTE)","author":"G. Holzmann","year":"1994","unstructured":"Holzmann, G., Peled, D.: An improvement in formal verification. In: Hogrefe, D., Leue, S. (eds.) Intl. Conf. on Formal Description Techniques (FORTE). IFIP Conference Proceedings, vol.\u00a06, pp.\u00a0197\u2013211. Chapman & Hall, London (1994)"},{"key":"6_CR18","series-title":"DIMACS: Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1090\/dimacs\/032\/03","volume-title":"Workshop on the SPIN Verification System","author":"G.J. Holzmann","year":"1996","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Gr\u00e9goire, J.C., Holzmann, G.J., Peled, D.A. (eds.) Workshop on the SPIN Verification System. DIMACS: Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a032, pp.\u00a023\u201332. AMS\/DIMACS, Providence (1996)"},{"key":"6_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-02658-4_31","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"V. Kahlon","year":"2009","unstructured":"Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05643, pp.\u00a0398\u2013413. Springer, Heidelberg (2009)"},{"key":"6_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/BFb0013032","volume-title":"REX Workshop on Linear Time, Branching Time and Partial Order 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. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) REX Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol.\u00a0354, pp.\u00a0489\u2013507. Springer, Heidelberg (1988)"},{"issue":"2","key":"6_CR21","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(92)90054-J","volume":"101","author":"S. Katz","year":"1992","unstructured":"Katz, S., Peled, D.: Defining conditional independence using collapses. Theor. Comput. Sci. 101(2), 337\u2013359 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-63166-6_33","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"I. Kokkarinen","year":"1997","unstructured":"Kokkarinen, I., Peled, D., Valmari, A.: Relaxed visibility enhances partial order reduction. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01254, pp.\u00a0328\u2013339. Springer, Heidelberg (1997)"},{"key":"6_CR23","series-title":"LNCS","first-page":"345","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"R. Kurshan","year":"1998","unstructured":"Kurshan, R., Levin, V., Minea, M., Peled, D., Yenig\u00fcn, H.: Static partial order reduction. In: Steffen, B. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01384, pp.\u00a0345\u2013357. Springer, Heidelberg (1998)"},{"key":"6_CR24","first-page":"657","volume-title":"Information Processing 83, Proc. of the World Computer Congress","author":"L. Lamport","year":"1983","unstructured":"Lamport, L.: What good is temporal logic. In: Mason, R. (ed.) Information Processing 83, Proc. of the World Computer Congress, pp.\u00a0657\u2013668. North-Holland\/IFIP, Amsterdam (1983)"},{"key":"6_CR25","series-title":"LNCS","first-page":"279","volume-title":"Petri Nets: Central Models and Their Properties, Advances in Petri Nets (APN)","author":"A. Mazurkiewicz","year":"1986","unstructured":"Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Central Models and Their Properties, Advances in Petri Nets (APN). LNCS, vol.\u00a0255, pp.\u00a0279\u2013324. Springer, Heidelberg (1986)"},{"key":"6_CR26","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/3-540-56496-9_14","volume-title":"Intl. Workshop on Computer-Aided Verification (CAV)","author":"K.L. McMillan","year":"1992","unstructured":"McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Gregor von Bochmann, D.K.P. (ed.) Intl. Workshop on Computer-Aided Verification (CAV). LNCS, vol.\u00a0663, pp.\u00a0164\u2013177. Springer, Heidelberg (1992)"},{"key":"6_CR27","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"6_CR28","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1142\/9789814261456_0006","volume-title":"The Book of Traces","author":"E. Ochmanski","year":"1995","unstructured":"Ochmanski, E.: Languages and automata. In: Diekert, V., Rozenberg, G. (eds.) The Book of Traces, pp.\u00a0167\u2013204. World Scientific, Singapore (1995)"},{"key":"6_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all, on model-checking using representatives. In: Courcoubetis, C. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0697, pp.\u00a0409\u2013423. Springer, Heidelberg (1993)"},{"issue":"1","key":"6_CR30","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D. Peled","year":"1996","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. Form. Methods Syst. Des. 8(1), 39\u201364 (1996)","journal-title":"Form. Methods Syst. Des."},{"issue":"5","key":"6_CR31","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D. Peled","year":"1997","unstructured":"Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the nexttime operator. Inf. Process. Lett. 63(5), 243\u2013246 (1997)","journal-title":"Inf. Process. Lett."},{"key":"6_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/3-540-61604-7_78","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"D. Peled","year":"1996","unstructured":"Peled, D., Wilke, T., Wolper, P.: An algorithmic approach for checking closure properties of \u03c9$\\omega$-regular languages. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01119, pp.\u00a0596\u2013610. Springer, Heidelberg (1996)"},{"key":"6_CR33","series-title":"LNCS","first-page":"491","volume-title":"Intl. Conf. on Applications and Theory of Petri Nets (APN)","author":"A. Valmari","year":"1989","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Intl. Conf. on Applications and Theory of Petri Nets (APN). LNCS, vol.\u00a0483, pp.\u00a0491\u2013515. Springer, Heidelberg (1989)"},{"key":"6_CR34","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Valmari","year":"1993","unstructured":"Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0697, pp.\u00a0397\u2013408. Springer, Heidelberg (1993)"},{"key":"6_CR35","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1090\/dimacs\/029\/12","volume-title":"DIMACS Workshop on Partial Order Methods in Verification (POMIV)","author":"A. Valmari","year":"1996","unstructured":"Valmari, A.: Stubborn set methods for process algebras. In: Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.) DIMACS Workshop on Partial Order Methods in Verification (POMIV). DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a029, pp.\u00a0213\u2013231. AMS, Providence (1996)"},{"key":"6_CR36","first-page":"322","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"M. Vardi","year":"1986","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0322\u2013331. IEEE, Piscataway (1986)"},{"key":"6_CR37","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/BFb0013026","volume-title":"REX Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"G. Winskel","year":"1988","unstructured":"Winskel, G.: An introduction to event structures. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) REX Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol.\u00a0354, pp.\u00a0364\u2013397. Springer, Heidelberg (1988)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:07:14Z","timestamp":1526616434000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_6","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}