{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:30:54Z","timestamp":1759638654127,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615507"},{"type":"electronic","value":"9783540705970"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61550-4_141","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:55:17Z","timestamp":1330293317000},"page":"93-112","source":"Crossref","is-referenced-by-count":15,"title":["Partial order reduction: Model-checking using representatives"],"prefix":"10.1007","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"6_CR1","first-page":"90","volume-title":"Model-Checking of Causality Properties","author":"R. Alur","year":"1995","unstructured":"R. Alur, D. Peled, W. Penczek, Model-Checking of Causality Properties, 10th Symposium on Logic in Computer Science, IEEE, 1995, San Diego, California, USA, 90\u2013100."},{"key":"6_CR2","doi-asserted-by":"crossref","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.","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, J. Hwang, Symbolic model checking: 1020 states and beyond, 5th Annual IEEE Symposium on Logic in Computer Science, 1990, 428\u2013439.","DOI":"10.1109\/LICS.1990.113767"},{"key":"6_CR4","series-title":"LNCS 1055","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-Verlag, 1996, Passau, Germany, to appear March 1996, 241\u2013257."},{"key":"6_CR5","doi-asserted-by":"publisher","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(1986), 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, A.P. Sistla, Symmetry and model checking, 5th International Conference on Computer-Aided Verification, 1993.","DOI":"10.1007\/3-540-56922-7_37"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. 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":"6_CR8","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1006\/inco.1995.1010","volume":"116","author":"V. Diekert","year":"1995","unstructured":"V. Diekert, P. Gastin, A. Petit, Rational and Recognizable Trace Languages, Information and Computation, 116(1995), 134\u2013153.","journal-title":"Information and Computation"},{"key":"6_CR9","first-page":"130","volume-title":"A Partial Order Approach to Branching Time Logic Model Checking","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."},{"key":"6_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, 3\u201318, Chapman & Hall, 1995, Warsaw, Poland."},{"key":"6_CR11","first-page":"176","volume-title":"LNCS 531","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-Verlag, New Brunswick, NJ, 1990, 176\u2013185."},{"key":"6_CR12","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":"6_CR13","first-page":"261","volume-title":"Using Partial Order Methods in the Formal Validation of Industrial Concurrent Programs","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":"6_CR14","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":"6_CR15","unstructured":"M.J.C. Gordon, T.F. Melham, Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic, Cambridge University Press, 1993."},{"key":"6_CR16","unstructured":"G. J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall Software Series, 1992."},{"key":"6_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":"6_CR18","unstructured":"G.J. Holzmann, D. Peled, M. Yannakakis, On Nested Depth First Search, in preparation."},{"key":"6_CR19","doi-asserted-by":"crossref","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":"6_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":"6_CR21","doi-asserted-by":"publisher","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 1 (1989), 213\u2013228.","journal-title":"Formal Aspects of Computing"},{"key":"6_CR22","unstructured":"L. Lamport, What good is temporal logic, Information Processing 83, Elsevier Science Publishers, 1983, 657\u2013668."},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, Checking that finite-state concurrent programs satisfy their linear specification, 11th Annual ACM Symposium on Principles of Programming Languages, 1984, 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"6_CR24","series-title":"LNCS 255","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":"6_CR25","unstructured":"R. Milner, A Calculus of Communicating System, LNCS, Springer-Verlag, 92."},{"key":"6_CR26","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":"6_CR27","first-page":"409","volume-title":"LNCS","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":"6_CR28","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.","journal-title":"Formal Methods in System Design"},{"key":"6_CR29","unstructured":"D. Peled, Th. Wilke, P. Wolper, An Algorithmic Approach for Checking Closure Properties of \u03c9-Regular Languages, submitted."},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, 18th FOCS, IEEE Symposium on Foundation of Computer Science, 1977, 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"6_CR31","first-page":"1","volume":"2","author":"A. Valmari","year":"1989","unstructured":"A. Valmari, Stubborn sets for reduced state space generation, 10 th International Conference on Application and Theory of Petri Nets, Vol. 2, Bonn, Germany, 1989, 1\u201322.","journal-title":"10 th International Conference on Application and Theory of Petri Nets"},{"key":"6_CR32","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":"6_CR33","doi-asserted-by":"publisher","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, P. Wolper, The Complementation Problem for B\u00fcchi Automata with Applications to Temporal Logic, Theoretical Computer Science, 49 (1987), 217\u2013237.","journal-title":"Theoretical Computer Science"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"P.S. Thiagarajan, A Trace Based Extension of Linear Time Temporal Logic. Proc. 10th IEEE Conference on Logic In Computer Science, 1994, 438\u2013447.","DOI":"10.1109\/LICS.1994.316047"},{"key":"6_CR35","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."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1996"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61550-4_141.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:21:35Z","timestamp":1742599295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61550-4_141"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615507","9783540705970"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-61550-4_141","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}