Abstract
Several methods have been developed to validate the correctness and performance of hard- and software systems. One way to do this is to model the system and carry out a state space exploration in order to detect all possible states. In this paper, a survey of existing probabilistic state space exploration methods is given. The paper starts with a thorough review and analysis of bitstate hashing, as introduced by Holzmann. The main idea of this initial approach is the mapping of each state onto a specific bit within an array by employing a hash function. Thus a state is represented by a single bit, rather than by a full descriptor. Bitstate hashing is efficient concerning memory and runtime, but it is hampered by the non deterministic omission of states. The resulting positive probability of producing wrong results is due to the fact that the mapping of full state descriptors onto much smaller representatives is not injective. – The rest of the paper is devoted to the presentation, analysis, and comparison of improvements of bitstate hashing, which were introduced in order to lower the probability of producing a wrong result, but maintaining the memory and runtime efficiency. These improvements can be mainly grouped into two categories: The approaches of the first group, the so called multiple hashing schemes, employ multiple hash functions on either a single or on multiple arrays. The approaches of the remaining category follow the idea of hash compaction. I.e. the diverse schemes of this category store a hash value for each detected state, rather than associating a single or multiple bit positions with it, leading to persuasive reductions of the probability of error if compared to the original bitstate hashing scheme.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Buchholz, P.: Structured Analysis Approaches for Large Markov Chains. Applied Numerical Mathematics 31, 375–404 (1999)
Godefroid, P.: Using Partial Orders to Improve Automatic Verification Methods. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176–185. Springer, Heidelberg (1991)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. An Approach to the State-Explosion Problem. PhD thesis, Universitè de Liege (1995)
Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pp. 174–186 (1997)
Godefroid, P., Holzmann, G., Pirottin, D.: State Space Caching Revisited. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 178–191. Springer, Heidelberg (1992)
Godefroid, P., Wolper, P.: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Formal Methods in System Design 2(2), 149–164 (1993)
Graham, R., Knuth, D., Patashnik, O.: Concrete Mathematics, 2nd edn. Addison-Wesley, Reading (1994)
Haverkort, B.R., Bell, A., Bohnenkamp, H.: On the Efficient Sequential and Distributed Generation of very Large Markov Chains from Stochastic Petri Nets. In: Proc. of IEEE Petri Nets and Performance Models, pp. 12–21 (1999)
Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains. In: Plateau, et al. [23], Proc. of the 3rd Int.Workshop on the Numerical Solution of Markov Chains (NSMC 1999), pp. 188–207 (1999)
Holzmann, G.: On Limits and Possibilities of Automated Protocol Analysis. In: Proc. 7th IFIP WG6.1 Int. Workshop on Protocol Specification, Testing, and Verification,, pp. 339–344. North-Holland Publishers, Amsterdam (1987)
Holzmann, G.: An Improved Protocol Reachability Analysis Technique. Software, Practice and Experience 18(2), 137–161 (1988)
Holzmann, G.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Holzmann, G.: The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5), 1–17 (1997)
Holzmann, G.: An Analysis of Bitstate Hashing. Formal Methods in System Design 13(3), 289–307 (1998)
Knottenbelt, W.: Generalized Markovian Analysis of Timed Transition Systems, Master’s Thesis, University of Cape Town (1996)
Knottenbelt, W., Harrison, P.: Distributed Disk-based Solution Techniques for Large Markov Models. In: Plateau, et al. (eds.) Proc. of the 3rd Int. Workshop on the Numerical Solution of Markov Chains (NSMC 1999)., vol. 23, pp. 58–75 (1999)
Knottenbelt, W., Harrison, P., Mestern, M., Kritzinger, P.: Probability, parallelism and the state space exploration problem. In: Puigjaner, R., Savino, N., Serra, B. (eds.) TOOLS 1998. LNCS, vol. 1469, pp. 165–179. Springer, Heidelberg (1998)
Knottenbelt, W., Harrison, P., Mestern, M., Kritzinger, P.: A Probabilistic Dynamic Technique for the Distributed Generation of Very Large State Spaces. Performance Evaluation Journal 39(1–4), 127–148 (2000)
Knottenbelt, W.J.: Parallel Performance Analysis of Large Markov Models. PhD thesis, University of London, Imperial College, Dept. of Computing (1999)
Knuth, D.: The Art of Computer Programming: Vol 3: Sorting and Searching, 2nd edn. Addison-Wesley, Reading (1998)
Kuntz, M., Lampka, K.: Probabilistic Methods in State Space Analysis. Technical Report 7 07/02, Universität Erlangen-Nürnberg, Institut für Informatik 7 (2002)
Ottman, Th., Widmayer, P.: Algorithmen und Datenstrukturen, 3 revised edn. Spektrum Akademischer Verlag (1996)
Plateau, B., Stewart, W.J., Silva, M. (eds.) Proc. of the 3rd Int. Workshop on the Numerical Solution of Markov Chains NSMC 1999, Prensas Universitarias de Zaragoza (1999)
Siegle, M.: Behaviour analysis of communication systems: Compositional modelling, compact representation and analysis of performability properties, Habilitationsschrift, Institut für Informatik. Friederich-Alexander-Universität Erlangen- Nürnberg (2002)
Stern, U.: Algorithmic Techniques in Verification by Explicit State Enumeration. PhD thesis, Technische Universität München (1997)
Stern, U., Dill, D.L.: Improved Probabilistic Verification by Hash Compaction. In: Sloman, M., Lobo, J., Lupu, E.C. (eds.) POLICY 2001. LNCS, vol. 1995, pp. 206–224. Springer, Heidelberg (2001)
Stern, U., Dill, D.L.: A New Scheme for Memory-Efficient Probabilistic Verification. In: Gotzhein, R., Bredereke, J. (eds.) Formal Description Techniques IX: Theory, application and tools. IFIP Conference Proceedings, vol. 96, pp. 333–348. Kluwer, Dordrecht (1996); Proc. of IFIP TC6 WG6.1 International Conference on Formal Description Techniques IX / Protocol Specification, Testing and Verification XVI, Kaiserslautern Germany, October 8-11
Stern, U., Dill, D.L.: Combining State Space Caching and Hash Compaction. In: Methoden des Entwurfs und der Verifikation digitaler Systeme, 4. GI/ITG/GME Workshop, pp. 81–90 (1996)
Wolper, P., Leroy, D.: Reliable Hashing Without Collision Detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 59–70. Springer, Heidelberg (1993)
Wolper, P., Stern, U., Leroy, D., Dill, D.L.: Reliable probabilistic verification using hash compaction (submitted for publication), Downloaded from http://www.citeseer.nj.nec.com/32915.html on (August 23, 2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Kuntz, M., Lampka, K. (2004). Probabilistic Methods in State Space Analysis. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, JP., Siegle, M. (eds) Validation of Stochastic Systems. Lecture Notes in Computer Science, vol 2925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24611-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-24611-4_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22265-1
Online ISBN: 978-3-540-24611-4
eBook Packages: Springer Book Archive