{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T16:40:18Z","timestamp":1738255218598,"version":"3.35.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2008,6,6]],"date-time":"2008-06-06T00:00:00Z","timestamp":1212710400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2008,10]]},"DOI":"10.1007\/s10009-008-0070-5","type":"journal-article","created":{"date-parts":[[2008,6,5]],"date-time":"2008-06-05T13:19:50Z","timestamp":1212671990000},"page":"443-454","source":"Crossref","is-referenced-by-count":17,"title":["Properties of state spaces and their applications"],"prefix":"10.1007","volume":"10","author":[{"given":"Radek","family":"Pel\u00e1nek","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,6,6]]},"reference":[{"issue":"1","key":"70_CR1","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1103\/RevModPhys.74.47","volume":"74","author":"R. Albert","year":"2002","unstructured":"Albert R., Barab\u00e1si A.L.: Statistical mechanics of complex networks. Rev. Modern Phys. 74(1), 47\u201397 (2002)","journal-title":"Rev. Modern Phys."},{"key":"70_CR2","doi-asserted-by":"crossref","unstructured":"Bao, T., Jones, M.: Time-efficient model checking with magnetic disk. In: Proceeding of Tools and Algorithms for the Construction and Analysis (TACAS\u201905), vol. 3440 of LNCS, pp. 526\u2013540. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-31980-1_34"},{"key":"70_CR3","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Cern\u00e1, I.: Cluster-based ltl model checking of large systems. In: Proceeding of Formal Methods for Components and Objects (FMCO\u201905), Revised Lectures, vol. 4111 of LNCS, pp. 259\u2013279. Springer, Heidelberg (2006)","DOI":"10.1007\/11804192_13"},{"key":"70_CR4","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL model-checking. In: Proceeding Automated Software Engineering (ASE 2003), pp. 106\u2013115. IEEE Computer Society, New York (2003)","DOI":"10.1109\/ASE.2003.1240299"},{"key":"70_CR5","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., Moravec, P., Rockai, P., \u0160ime\u010dek, P.: Divine\u2014a tool for distributed verification. In: Proceeding of Computer Aided Verification (CAV\u201906), vol. 4144 of LNCS, pp. 278\u2013281. Springer, Heidelberg 2006. The tool is available at http:\/\/anna.fi.muni.cz\/divine","DOI":"10.1007\/11817963_26"},{"key":"70_CR6","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Larsen, K.G., Pel\u00e1nek, R.: To store or not to store. In: Proceeding Computer Aided Verification (CAV 2003), vol. 2725 of LNCS, pp. 433\u2013445 (2003)","DOI":"10.1007\/978-3-540-45069-6_40"},{"key":"70_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y. Symbolic model checking without BDDs. In: Proceeding Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1999), vol. 1579 of LNCS, pp. 193\u2013207 (1999)","DOI":"10.21236\/ADA360973"},{"key":"70_CR8","volume-title":"Classification and Regression Trees","author":"L. Breiman","year":"1984","unstructured":"Breiman L.: Classification and Regression Trees. CRC Press, Boca Raton (1984)"},{"key":"70_CR9","doi-asserted-by":"crossref","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Distributed explicit fair cycle detection. In: Proceeding SPIN workshop, vol. 2648 of LNCS, pp. 49\u201373 (2003)","DOI":"10.1007\/3-540-44829-2_4"},{"key":"70_CR10","doi-asserted-by":"crossref","unstructured":"Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured petri nets exploiting strongly connected components. In: Proceeding International Workshop on Discrete Event Systems, pp. 169\u2013177 (1996)","DOI":"10.7146\/dpb.v26i519.7048"},{"key":"70_CR11","doi-asserted-by":"crossref","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A Sweep-Line Method for State Space Exploration. In: Proceeding Tools and Algorithms for Construction and Analysis of Systems (TACAS 2001), vol. 2031 of LNCS, pp. 450\u2013464 (2001)","DOI":"10.1007\/3-540-45319-9_31"},{"key":"70_CR12","doi-asserted-by":"crossref","unstructured":"David, A., Behrmann, G., Larsen, K.G., Yi, W.: Unification & sharing in timed automata verification. In: Proceeding SPIN Workshop, vol. 2648 of LNCS, pp. 225\u2013229 (2003)","DOI":"10.1007\/3-540-44829-2_15"},{"key":"70_CR13","first-page":"290","volume":"6","author":"P. Erd\u0151s","year":"1959","unstructured":"Erd\u0151s P., Renyi A.: On random graphs. Publ. Math. 6, 290\u2013297 (1959)","journal-title":"Publ. Math."},{"key":"70_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceeding of Principles of programming languages (POPL\u201905), pp. 110\u2013121. ACM Press, New York (2005)","DOI":"10.1145\/1040305.1040315"},{"issue":"4","key":"70_CR15","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. Int. J. Softw. Tools Technol. Transfer (STTT) 2(4), 317\u2013320 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transfer (STTT)"},{"key":"70_CR16","doi-asserted-by":"crossref","unstructured":"Geldenhuys, J.: State caching reconsidered. In: Proceeding of SPIN Workshop, vol. 2989 of LNCS, pp. 23\u201339. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24732-6_3"},{"key":"70_CR17","doi-asserted-by":"crossref","unstructured":"Groote, J.F., van Ham, F.: Large state space visualization. In: Proceeding of Tools and Algorithms for Construction and Analysis of Systems (TACAS 2003), vol. 2619 of LNCS, pp. 585\u2013590 (2003)","DOI":"10.1007\/3-540-36577-X_42"},{"issue":"2","key":"70_CR18","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 Tech. J. 69(2), 32\u201344 (1990)","journal-title":"AT&T Tech. J."},{"key":"70_CR19","unstructured":"Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proceeding SPIN Workshop. Twente Univ. (1997)"},{"key":"70_CR20","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The engineering of a model checker: the gnu i-protocol case study revisited. In: Proceeding SPIN Workshop, vol. 1680 of LNCS, pp. 232\u2013244 (1999)","DOI":"10.1007\/3-540-48234-2_18"},{"key":"70_CR21","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":"70_CR22","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proceeding SPIN Workshop, pp. 23\u201332. American Mathematical Society, New York (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"70_CR23","doi-asserted-by":"crossref","unstructured":"Kr\u010d \u00e1l, P.: Distributed explicit bounded ltl model checking. In: Proceeding of Parallel and Distributed Methods in verifiCation (PDMC\u201903), vol. 89 of ENTCS. Elsevier, Amsterdam (2003)","DOI":"10.1016\/S1571-0661(05)80095-7"},{"key":"70_CR24","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":"70_CR25","doi-asserted-by":"crossref","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Proceeding of SPIN Workshop, vol. 2057 of LNCS, pp. 80\u2013102. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45139-0_6"},{"key":"70_CR26","unstructured":"Maister, D.H.: The psychology of waiting lines. In: Czepiel J.A., Solomon M.R., Suprenant C. (eds.), The Service Encounter. Lexington Books (1985)"},{"issue":"5663","key":"70_CR27","doi-asserted-by":"crossref","first-page":"1538","DOI":"10.1126\/science.1089167","volume":"303","author":"R. Milo","year":"2004","unstructured":"Milo R., Itzkovitz S., Kashtan N., Levitt R., Shen-Orr S., Ayzenshtat I., Sheffer M., Alon U.: Superfamilies of evolved and designed networks. Science 303(5663), 1538\u20131542 (2004)","journal-title":"Science"},{"issue":"5594","key":"70_CR28","doi-asserted-by":"crossref","first-page":"824","DOI":"10.1126\/science.298.5594.824","volume":"298","author":"R. Milo","year":"2002","unstructured":"Milo R., Shen-Orr S., Itzkovitz S., Kashtan N., Chklovskii D., Alon U.: Network motifs: simple building blocks of complex networks. Science 298(5594), 824\u2013827 (2002)","journal-title":"Science"},{"key":"70_CR29","doi-asserted-by":"crossref","unstructured":"Pel\u00e1nek, R.: Typical structural properties of state spaces. In: Proceeding of SPIN Workshop, vol. 2989 of LNCS, pp. 5\u201322. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24732-6_2"},{"key":"70_CR30","unstructured":"Pel\u00e1nek, R.: Reduction and Abstraction Techniques for Model Checking. PhD thesis, Faculty of Informatics, Masaryk University, Brno (2006)"},{"key":"70_CR31","doi-asserted-by":"crossref","unstructured":"Pel\u00e1nek, R.: Beem: Benchmarks for explicit model checkers. In: Proceeding of SPIN Workshop, vol. 4595 of LNCS, pp. 263\u2013267. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73370-6_17"},{"key":"70_CR32","unstructured":"Pel\u00e1nek, R.: Model classifications and automated verification. In: Proceeding of Formal Methods for Industrial Critical Systems (FMICS\u201907) (2007). (To appear)"},{"key":"70_CR33","doi-asserted-by":"crossref","unstructured":"Pel\u00e1nek, R., Han\u017el, T., \u010cern\u00e1, I., Brim, L.: Enhancing random walk state space exploration. In: Proceeding of Formal Methods for Industrial Critical Systems (FMICS\u201905), pp. 98\u2013105. ACM Press, New York (2005)","DOI":"10.1145\/1081180.1081193"},{"key":"70_CR34","unstructured":"Pel\u00e1nek, R., \u0160ime\u010dek, P.: Estimating state space parameters. Technical Report FIMU-RS-2008-01, Masaryk University Brno (2008)"},{"key":"70_CR35","doi-asserted-by":"crossref","unstructured":"Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. In: Proceeding of Application of Concurrency to System Design (ACSD\u201904), p. 217. IEEE Computer Society, New York (2004)","DOI":"10.1109\/CSD.2004.1309134"},{"key":"70_CR36","doi-asserted-by":"crossref","unstructured":"Sivaraj, H., Gopalakrishnan, G.: Random walk based heuristic algorithms for distributed memory model checking. In: Proceeding of Parallel and Distributed Model Checking (PDMC\u201903), vol. 89 of ENTCS (2003)","DOI":"10.1016\/S1571-0661(05)80096-9"},{"key":"70_CR37","unstructured":"Stern, U.: Algorithmic Techniques in Verification by Explicit State Enumeration. PhD thesis, Technical University of Munich (1997)"},{"key":"70_CR38","doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.L.: Using magnatic disk instead of main memory in the Murphi verifier. In: Proceeding Computer Aided Verification (CAV 1998), vol. 1427 of LNCS, pp. 172\u2013183 (1998)","DOI":"10.1007\/BFb0028743"},{"key":"70_CR39","doi-asserted-by":"crossref","unstructured":"Tronci, E., Penna, G.D., Intrigila, B., Venturini, M.: A probabilistic approach to automatic verification of concurrent systems. In: Proceeding Asia-Pacific Software Engineering Conference (APSEC 2001), pp. 317\u2013324. IEEE Computer Society, New York (2001)","DOI":"10.1109\/APSEC.2001.991495"},{"key":"70_CR40","doi-asserted-by":"crossref","unstructured":"Tronci, E., Penna, G.D., Intrigila, B., Zilli, M.V.: Exploiting transition locality in automatic verification. In: Proceeding Correct Hardware Design and Verification Methods (CHARME 2001), vol. 2144 of LNCS, pp. 259\u2013274 (2001)","DOI":"10.1007\/3-540-44798-9_22"},{"key":"70_CR41","first-page":"332","volume-title":"Proceeding of Logic in Computer Science (LICS \u201986)","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi M.Y., Wolper P.: An automata-theoretic approach to automatic program verification. In: Kozen, D. (eds) Proceeding of Logic in Computer Science (LICS \u201986), pp. 332\u2013344. IEEE Computer Society Press, New York (1986)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0070-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-008-0070-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-008-0070-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T16:00:10Z","timestamp":1738252810000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-008-0070-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6,6]]},"references-count":41,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2008,10]]}},"alternative-id":["70"],"URL":"https:\/\/doi.org\/10.1007\/s10009-008-0070-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2008,6,6]]}}}