Abstract
Explicit model checking algorithms explore the full state space of a system. State spaces are usually treated as directed graphs without any specific features. We gather a large collection of state spaces and extensively study their structural properties. Our results show that state spaces have several typical properties, i.e., they are not arbitrary graphs. We also demonstrate that state spaces differ significantly from random graphs and that different classes of models (application domains, academic vs. industrial) have different properties. We discuss consequences of these results for model checking experiments and we point out how to exploit typical properties of state spaces in practical model checking algorithms.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Albert R., Barabási A.L.: Statistical mechanics of complex networks. Rev. Modern Phys. 74(1), 47–97 (2002)
Bao, T., Jones, M.: Time-efficient model checking with magnetic disk. In: Proceeding of Tools and Algorithms for the Construction and Analysis (TACAS’05), vol. 3440 of LNCS, pp. 526–540. Springer, Heidelberg (2005)
Barnat, J., Brim, L., Cerná, I.: Cluster-based ltl model checking of large systems. In: Proceeding of Formal Methods for Components and Objects (FMCO’05), Revised Lectures, vol. 4111 of LNCS, pp. 259–279. Springer, Heidelberg (2006)
Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL model-checking. In: Proceeding Automated Software Engineering (ASE 2003), pp. 106–115. IEEE Computer Society, New York (2003)
Barnat, J., Brim, L., Černá, I., Moravec, P., Rockai, P., Šimeček, P.: Divine—a tool for distributed verification. In: Proceeding of Computer Aided Verification (CAV’06), vol. 4144 of LNCS, pp. 278–281. Springer, Heidelberg 2006. The tool is available at http://anna.fi.muni.cz/divine
Behrmann, G., Larsen, K.G., Pelánek, R.: To store or not to store. In: Proceeding Computer Aided Verification (CAV 2003), vol. 2725 of LNCS, pp. 433–445 (2003)
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–207 (1999)
Breiman L.: Classification and Regression Trees. CRC Press, Boca Raton (1984)
Černá, I., Pelánek, R.: Distributed explicit fair cycle detection. In: Proceeding SPIN workshop, vol. 2648 of LNCS, pp. 49–73 (2003)
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–177 (1996)
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–464 (2001)
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–229 (2003)
Erdős P., Renyi A.: On random graphs. Publ. Math. 6, 290–297 (1959)
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceeding of Principles of programming languages (POPL’05), pp. 110–121. ACM Press, New York (2005)
Dwyer M.B., Avrunin G.S., Corbett J.C.: Benchmarking finite-state verifiers. Int. J. Softw. Tools Technol. Transfer (STTT) 2(4), 317–320 (2000)
Geldenhuys, J.: State caching reconsidered. In: Proceeding of SPIN Workshop, vol. 2989 of LNCS, pp. 23–39. Springer, Heidelberg (2004)
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–590 (2003)
Holzmann G.J.: Algorithms for automated protocol verification. AT&T Tech. J. 69(2), 32–44 (1990)
Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proceeding SPIN Workshop. Twente Univ. (1997)
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–244 (1999)
Holzmann G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)
Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proceeding SPIN Workshop, pp. 23–32. American Mathematical Society, New York (1996)
Krč ál, P.: Distributed explicit bounded ltl model checking. In: Proceeding of Parallel and Distributed Methods in verifiCation (PDMC’03), vol. 89 of ENTCS. Elsevier, Amsterdam (2003)
Lafuente, A.L.: Simplified distributed LTL model checking by localizing cycles. Technical Report 176, Institut für Informatik, Universität Freiburg, July (2002)
Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Proceeding of SPIN Workshop, vol. 2057 of LNCS, pp. 80–102. Springer, Heidelberg (2001)
Maister, D.H.: The psychology of waiting lines. In: Czepiel J.A., Solomon M.R., Suprenant C. (eds.), The Service Encounter. Lexington Books (1985)
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–1542 (2004)
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–827 (2002)
Pelánek, R.: Typical structural properties of state spaces. In: Proceeding of SPIN Workshop, vol. 2989 of LNCS, pp. 5–22. Springer, Heidelberg (2004)
Pelánek, R.: Reduction and Abstraction Techniques for Model Checking. PhD thesis, Faculty of Informatics, Masaryk University, Brno (2006)
Pelánek, R.: Beem: Benchmarks for explicit model checkers. In: Proceeding of SPIN Workshop, vol. 4595 of LNCS, pp. 263–267. Springer, Heidelberg (2007)
Pelánek, R.: Model classifications and automated verification. In: Proceeding of Formal Methods for Industrial Critical Systems (FMICS’07) (2007). (To appear)
Pelánek, R., Hanžl, T., Černá, I., Brim, L.: Enhancing random walk state space exploration. In: Proceeding of Formal Methods for Industrial Critical Systems (FMICS’05), pp. 98–105. ACM Press, New York (2005)
Pelánek, R., Šimeček, P.: Estimating state space parameters. Technical Report FIMU-RS-2008-01, Masaryk University Brno (2008)
Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. In: Proceeding of Application of Concurrency to System Design (ACSD’04), p. 217. IEEE Computer Society, New York (2004)
Sivaraj, H., Gopalakrishnan, G.: Random walk based heuristic algorithms for distributed memory model checking. In: Proceeding of Parallel and Distributed Model Checking (PDMC’03), vol. 89 of ENTCS (2003)
Stern, U.: Algorithmic Techniques in Verification by Explicit State Enumeration. PhD thesis, Technical University of Munich (1997)
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–183 (1998)
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–324. IEEE Computer Society, New York (2001)
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–274 (2001)
Vardi M.Y., Wolper P.: An automata-theoretic approach to automatic program verification. In: Kozen, D. (eds) Proceeding of Logic in Computer Science (LICS ’86), pp. 332–344. IEEE Computer Society Press, New York (1986)
Author information
Authors and Affiliations
Corresponding author
Additional information
R. Pelánek was partially supported by GA ČR grant no. 201/07/P035.
Rights and permissions
About this article
Cite this article
Pelánek, R. Properties of state spaces and their applications. Int J Softw Tools Technol Transfer 10, 443–454 (2008). https://doi.org/10.1007/s10009-008-0070-5
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-008-0070-5