{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:52:10Z","timestamp":1742935930739,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540401179"},{"type":"electronic","value":"9783540448297"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44829-2_6","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:01:40Z","timestamp":1183478500000},"page":"89-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Light-Weight Algorithm for Model Checking with Symmetry Reduction and Weak Fairness"],"prefix":"10.1007","author":[{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"6_CR1","unstructured":"A. V. Aho, J. E. Hopcroft, J. D. Ulmann, The design and Analysis of Computer Algorithms, Addison Wesley, 1974."},{"key":"6_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-48234-2_4","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"D. Bo\u0161na\u010dki","year":"1999","unstructured":"D. Bo\u0161na\u010dki, Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness, Theoretical and Practical Aspects of SPIN Model Checking, 5th and 6th International SPIN Workshops, LNCS 1680, pp. 40\u201356, Springer, 1999."},{"key":"6_CR3","unstructured":"D. Bo\u0161na\u010dki, Enhancing State Space Reduction Techniques for Model Checking, p. 146, Ph.D. Thesis, Eindhoven University of Technology, ISBN 90-386-0951-5, 2001."},{"key":"6_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-46017-9","volume-title":"Proc. of FORTE\u201902","author":"D. Bo\u0161na\u010dki","year":"2002","unstructured":"D. Bo\u0161na\u010dki, A Nested Depth First Search Algorithm for Model Checking with Symmetry Reduction, Proc. of FORTE\u201902, LNCS, Springer, 2002."},{"key":"6_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10722468_1","volume-title":"7th Int. SPIN Workshop on Model Checking of Software SPIN 2000","author":"D. Bo\u0161na\u010dki","year":"2000","unstructured":"D. Bo\u0161na\u010dki, D. Dams, L. Holenderski, Symmetric Spin, 7th Int. SPIN Workshop on Model Checking of Software SPIN 2000, pp. 1\u201319, LNCS 1885, Springer, 2000."},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Y. Choueka, Theories of Automata on \u03c9-tapes: a Simplified Approach, Journal of Computer and System Science, Vol. 8, pp. 117\u2013141, 1974.","journal-title":"Journal of Computer and System Science"},{"key":"6_CR7","unstructured":"E. M. Clarke, Jr., O. Grumberg, D. A. Peled, Model Checking, The MIT Press, 2000."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis, Memory Efficient Algorithms for the Verification of Temporal Properties, Formal Methods in System Design I, pp. 275\u2013288, 1992.","DOI":"10.1007\/BF00121128"},{"key":"6_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"Proc. of FM\u201999","author":"J.-M. Couvreur","year":"1999","unstructured":"J.-M. Couvreur, On-the-fly Verification of Linear Temporal Logic, Proc. of FM\u201999, pp. 253\u2013271, LNCS 1708, 1999."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"E. A. Emerson, Temporal and Modal Logic, in J. van Leeuwen (ed.), Formal Models and Semantics, pp. 995\u20131072, Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"6_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-56922-7_38","volume-title":"Proc. of CAV\u201993 (Computer Aided Verification)","author":"E. A. Emerson","year":"1993","unstructured":"E. A. Emerson, A. P. Sistla, Symmetry and model checking, Proc. of CAV\u201993 (Computer Aided Verification), LNCS 697, pp. 463\u2013478, Springer, 1993."},{"key":"6_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/3-540-60045-0_59","volume-title":"Proc. of CAV\u201995 (Computer Aided Verification)","author":"E. A. Emerson","year":"1995","unstructured":"E. A. Emerson, A. P. Sistla, Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata Theoretic Approach, Proc. of CAV\u201995 (Computer Aided Verification), LNCS 697, pp. 309\u2013324, Springer, 1995."},{"key":"6_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/BFb0035378","volume-title":"Proc. of TACAS\u201997 (Tools and Algorithms for the Construction and Analysis of Systems)","author":"E. A. Emerson","year":"1997","unstructured":"E. A. Emerson, S. Jha, D. Peled, Combining partial order and symmetry reductions, in Ed Brinksma (ed.), Proc. of TACAS\u201997 (Tools and Algorithms for the Construction and Analysis of Systems), LNCS 1217, pp. 19\u201334, Springer, 1997."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"N. Francez, Fairness, Springer, 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"6_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-63166-6_24","volume-title":"Proc. of CAV\u201997 (Computer Aided Verification)","author":"V. Gyuris","year":"1997","unstructured":"V. Gyuris, A. P. Sistla, On-the fly model checking under fairness that exploits symmetry, in O. Grumberg (ed.), Proc. of CAV\u201997 (Computer Aided Verification), LNCS 1254, pp. 232\u2013243, Springer, 1997."},{"key":"6_CR16","unstructured":"G. J Holzmann, Design and Validation of Communication Protocols, Prentice Hall, 1991. Also: http:\/\/netlib.bell-labs.com\/netlib\/spin\/whatispin.html."},{"key":"6_CR17","unstructured":"G. Holzmann, D. Peled, An Improvement in Formal Verification, FORTE 1994, Bern, Switzerland, 1994."},{"key":"6_CR18","volume-title":"Proc. of the 2nd Spin Workshop","author":"G. Holzmann","year":"1996","unstructured":"G. Holzmann, D. Peled, M. Yannakakis, On Nested Depth First Search, Proc. of the 2nd Spin Workshop, Rutgers University, New Jersey, USA, 1996."},{"key":"6_CR19","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"C. N. Ip","year":"1996","unstructured":"C. N. Ip, D. L. Dill, Better verification through symmetry. Formal Methods in System Design, Vol. 9, pp. 41\u201375, 1996.","journal-title":"Formal Methods in System Design"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"W. Thomas, Automata on Infinite Objects, in J. van Leeuwen (ed.), Formal Models and Semantics, pp. 995\u20131072 Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"issue":"2","key":"6_CR21","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M. Vardi","year":"1986","unstructured":"M. Vardi, P. Wolper, Automata Theoretic Techniques for Modal Logics of Programs, Journal of Computer and System Science, 32(2), pp. 182\u2013221, 1986.","journal-title":"Journal of Computer and System Science"},{"key":"6_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/3-540-56922-7_6","volume-title":"Proc. of CAV\u201993 (Computer Aided Verification)","author":"P. Wolper","year":"1993","unstructured":"P. Wolper, D. Leroy, Reliable Hashing without Collision Detection, Proc. of CAV\u201993 (Computer Aided Verification), LNCS 697, pp. 59\u201370, Springer, 1993."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44829-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T21:59:44Z","timestamp":1675893584000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44829-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540401179","9783540448297"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44829-2_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"15 April 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}