{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T15:29:51Z","timestamp":1742398191528},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213147"},{"type":"electronic","value":"9783540247326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_2","type":"book-chapter","created":{"date-parts":[[2010,7,27]],"date-time":"2010-07-27T20:14:47Z","timestamp":1280261687000},"page":"5-22","source":"Crossref","is-referenced-by-count":21,"title":["Typical Structural Properties of State Spaces"],"prefix":"10.1007","author":[{"given":"Radek","family":"Pel\u00e1nek","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"http:\/\/www.fi.muni.cz\/~xpelanek\/state_spaces"},{"key":"2_CR2","unstructured":"Barabasi, A.L.: Linked: How Everything Is Connected to Everything Else and What It Means, Plume (2003)"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1109\/ASE.2003.1240299","volume-title":"Proc. Automated Software Engineering (ASE 2003)","author":"J. Barnat","year":"2003","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL modelchecking. In: Proc. Automated Software Engineering (ASE 2003), pp. 106\u2013115. IEEE Computer Society, Los Alamitos (2003)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-540-45069-6_40","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2003","unstructured":"Behrmann, G., Larsen, K.G., Pel\u00e1nek, R.: To store or not to store. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 433\u2013445. Springer, Heidelberg (2003)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-44829-2_4","volume-title":"Model Checking Software","author":"I. \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Distributed explicit fair cycle detection. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured petri nets exploiting strongly connected components. In: Proc. International Workshop on Discrete Event Systems, pp. 169\u2013177 (1996)","DOI":"10.7146\/dpb.v26i519.7048"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-45319-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Christensen","year":"2001","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A Sweep-Line Method for State Space Exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 450\u2013464. Springer, Heidelberg (2001)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-44829-2_15","volume-title":"Model Checking Software","author":"A. David","year":"2003","unstructured":"David, A., Behrmann, G., Larsen, K.G., Yi, W.: Unification & sharing in timed automata verification. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 225\u2013229. Springer, Heidelberg (2003)"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1109\/ICCD.1992.276232","volume-title":"Proc. Computer Design: VLSI in Computers and Processors","author":"D.L. Dill","year":"1992","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Han Yang, C.: Protocol verification as a hardware design aid. In: Proc. Computer Design: VLSI in Computers and Processors, pp. 522\u2013525. IEEE Computer Society, Los Alamitos (1992)"},{"key":"2_CR11","first-page":"290","volume":"6","author":"P. Erd\u0151s","year":"1959","unstructured":"Erd\u0151s, P., Renyi, A.: On random graphs. Publ. Math.\u00a06, 290\u2013297 (1959)","journal-title":"Publ. Math."},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-45319-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Fisler","year":"2001","unstructured":"Fisler, K., Fraer, R., Kamhi, G., Vardi, Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"issue":"4","key":"2_CR13","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/s100090050038","volume":"2","author":"M.B. Dwyer","year":"2000","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Benchmarking finite-state verifiers. International Journal on Software Tools for Technology Transfer (STTT)\u00a02(4), 317\u2013320 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"2_CR14","first-page":"13","volume":"4","author":"H. Garavel","year":"2002","unstructured":"Garavel, H., Lang, F., Mateescu, R.: An overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter\u00a04, 13\u201324 (2002)","journal-title":"European Association for Software Science and Technology (EASST) Newsletter"},{"issue":"3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/BF01384077","volume":"7","author":"P. Godefroid","year":"1995","unstructured":"Godefroid, P., Holzmann, G.J., Pirottin, D.: State space caching revisited. Formal Methods in System Design\u00a07(3), 227\u2013241 (1995)","journal-title":"Formal Methods in System Design"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Ponse, A.: The syntax and semantics of \u03bcCRL. In: Algebra of Communicating Processes 1994. Workshops in Computing Series, pp. 26\u201362 (1995)","DOI":"10.1007\/978-1-4471-2120-6_2"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/3-540-36577-X_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.F. Groote","year":"2003","unstructured":"Groote, J.F., van Ham, F.: Large state space visualization. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 585\u2013590. Springer, Heidelberg (2003)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: An analysis of bitstate hashing. In: Proc. Protocol Specification, Testing, and Verification, INWG\/IFIP, pp. 301\u2013314 (1995)","DOI":"10.1007\/978-0-387-34892-6_19"},{"key":"2_CR19","unstructured":"Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proc. SPIN Workshop, Twente Univ. (1997)"},{"issue":"2","key":"2_CR20","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1002\/j.1538-7305.1990.tb00101.x","volume":"69","author":"G.J. Holzmann","year":"1990","unstructured":"Holzmann, G.J.: Algorithms for automated protocol verification. AT&T Technical Journal\u00a069(2), 32\u201344 (1990)","journal-title":"AT&T Technical Journal"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-48234-2_18","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"G.J. Holzmann","year":"1999","unstructured":"Holzmann, G.J.: The engineering of a model checker: the gnu i-protocol case study revisited. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 232\u2013244. Springer, Heidelberg (1999)"},{"key":"2_CR22","volume-title":"The Spin Model Checker, Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"2_CR23","unstructured":"Lafuente, A.L.: Simplified distributed LTL model checking by localizing cycles. Technical Report 176, Institut f\u00fcr Informatik, Universit\u00e4t Freiburg (July 2002)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-36126-X_13","volume-title":"Formal Methods in Computer-Aided Design","author":"G.D. Penna","year":"2002","unstructured":"Penna, G.D., Intrigila, B., Tronci, E., Zilli, M.V.: Exploiting transition locality in the disk based Murphi verifier. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 202\u2013219. Springer, Heidelberg (2002)"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-40922-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Ravi","year":"2000","unstructured":"Ravi, K., Bloem, R., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 143\u2013160. Springer, Heidelberg (2000)"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/10722468_17","volume-title":"SPIN Model Checking and Software Verification","author":"T.C. Ruys","year":"2000","unstructured":"Ruys, T.C.: Low-fat recipes for SPIN. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 287\u2013321. Springer, Heidelberg (2000)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/3-540-36126-X_6","volume-title":"Formal Methods in Computer-Aided Design","author":"F. Somenzi","year":"2002","unstructured":"Somenzi, F., Ravi, K., Bloem, R.: Analysis of symbolic SCC hull algorithms. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 88\u2013105. Springer, Heidelberg (2002)"},{"key":"2_CR28","unstructured":"Stern, U.: Algorithmic Techniques in Verification by Explicit State Enumeration. PhD thesis, Technical University of Munich (1997)"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0028743","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1998","unstructured":"Stern, U., Dill, D.L.: Using magnatic disk instead of main memory in the Murphi verifier. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"2_CR30","first-page":"317","volume-title":"Proc. Asia-Pacific Software Engineering Conference (APSEC 2001)","author":"E. Tronci","year":"2001","unstructured":"Tronci, E., Penna, G.D., Intrigila, B., Venturini, M.: A probabilistic approach to automatic verification of concurrent systems. In: Proc. Asia-Pacific Software Engineering Conference (APSEC 2001), pp. 317\u2013324. IEEE Computer Society, Los Alamitos (2001)"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/3-540-44798-9_22","volume-title":"Correct Hardware Design and Verification Methods","author":"E. Tronci","year":"2001","unstructured":"Tronci, E., Penna, G.D., Intrigila, B., Zilli, M.V.: Exploiting transition locality in automatic verification. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 259\u2013274. Springer, Heidelberg (2001)"},{"key":"2_CR32","volume-title":"Six Degrees: The Science of a Connected Age","author":"D.J. Watts","year":"2003","unstructured":"Watts, D.J.: Six Degrees: The Science of a Connected Age. W.W. Norton & Company, New York (2003)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:29:58Z","timestamp":1559316598000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}