Abstract
To limit the explosion problem encountered during reachability analysis we suggest a variety of techniques for reducing the number of states to be stored during exploration, while maintaining the guarantee of termination and keeping the number of revisits small. The techniques include static analysis methods for component automata in order to determine small sets of covering transitions. We carry out extensive experimental investigation of the techniques within the real-time verification tool Uppaal. Our experimental results are extremely encouraging: a best combination is identified which for a variety of industrial case-studies reduces the space-consumption to less than 10% with only a moderate overhead in time-performance.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Dill, D.: Automata for Modelling Real-Time Systems. Theoretical Computer Science 126(2), 183–236 (1994)
Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–270. Springer, Heidelberg (2003)
Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)
Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 states and beyond. In: Proc. of IEEE Symp. on Logic in Computer Science (1990)
Godefroid, P., Holzmann, G.J., Pirottin, D.: State-space caching revisited. Formal Methods in System Design 7(3), 227–241 (1995)
Godefroid, P., Wolper, P.: A Partial Approach to Model Checking. In: Proc. Of IEEE Symp. on Logic in Computer Science, pp. 406–415 (1991)
Karp, R.M.: Redcibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W. (eds.) Complexity of Computer Computations, pp. 85–103. Plenum Press, New York (1972)
Kurshan, R., Levin, V., Minea, M., Peled, D., Yenigün, H.: Static partial order reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 345–357. Springer, Heidelberg (1998)
Laroussinie, F., Larsen, K.G.: Compositional Model Checking of Real Time Systems. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962. Springer, Heidelberg (1995)
Larsson, F., Larsen, K.G., Pettersson, P., Yi, W.: Efficient Verification of Real- Time Systems: Compact Data Structures and State-Space Reduction. In: Proc. of the 18th IEEE Real-Time Systems Symposium, pp. 14–24. IEEE Computer Society Press, Los Alamitos (1997)
Lind-Nielsen, J., Reif Andersen, H., Behrmann, G., Hulgaard, H., Kristoffersen, K., Larsen, K.G.: Verification of Large State/Event Systems Using Compositionality and Dependency Analysis. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 201–216. Springer, Heidelberg (1998)
Valmari, A.: A Stubborn Attack on State Explosion. Theoretical Computer Science 3 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Behrmann, G., Larsen, K.G., Pelánek, R. (2003). To Store or Not to Store. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_40
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive