Abstract
Symbolic model-checking usually includes two steps: the building of a compact representation of a state graph and the evaluation of the properties of the system upon this data structure. In case of properties expressed with a linear time logic, it appears that the second step is often more time consuming than the first one. In this work, we present a mixed solution which builds an observation graph represented in a non symbolic way but where the nodes are essentially symbolic set of states. Due to the small number of events to be observed in a typical formula, this graph has a very moderate size and thus the complexity time of verification is neglectible w.r.t. the time to build the observation graph. Thus we propose different symbolic implementations for the construction of the nodes of this graph. The evaluations we have done on standard examples show that our method outperforms the pure symbolic methods which makes it attractive.
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
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35, 677–691 (1986)
Wegener, I.: Branching Programs and Binary Decision Diagrams: Theory and Application. SIAM Monographs on Discrete Mathematics and Applications (2000)
Fisler, K., Fraer, R., Khami, G., Vardi, M., Yang, Z.: Is there a best symbolic cycledetection algorithm? In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 420–434. Springer, Heidelberg (2001)
Emerson, E., Lei, C.: Efficient model-checking in fragments of propositional model mu-calculus. In: Proceedings of LIC 1986, pp. 267–278 (1986)
Ravi, K., Bloem, R., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: International Conference on Formal Methods for Computer-Aided Verification, pp. 143–160. Springer, Heidelberg (2000)
Bloem, R., Gabow, H., Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps. In: International Conference on Formal Methods for Computer-Aided Verification, pp. 37–54. Springer, Heidelberg (2000)
Gentilini, R., Piazza, C., Policriti, A.: Computing strongly connected components in a linear number of symbolic steps. In: Proceedings of International Symposium on Discrete Algorithms (SODA 2003), pp. 573–582. ACM/SIAM (2003)
Xie, A., Beerel, P.: Implicit enumeration of strongly connected components and an application to formal verification. IEEETCAD: IEEE Transactions on Computer- Aided Design of Integrated Circuits and Systems 19 (2000)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems, vol. 1. Springer, New York (1992)
Kaivola, R., Valmari, A.: The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic. In: International Conference on Concurrency Theory, pp. 207–221 (1992)
Puhakka, A., Valmari, A.: Weakest-congruence results for livelock-preserving equivalences. In: Proceedings of the 10th International Conference on Concurrency Theory, pp. 510–524. Springer, Heidelberg (1999)
Valmari, A.: Failure-based equivalences are faster than many believe. In: Desel, J. (ed.) Structures in Concurrency Theory, Proceedings of the International Workshop on Structures in Concurrency Theory (STRICT), Berlin, May 11-13, pp. 326–340 (1995)
Valmari, A.: The state explosion problem. In: Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, pp. 429–528. Springer, Heidelberg (1998)
Miner, A., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: International Conference on Application and Theory of Petri Nets. LNCS, pp. 388–393. Springer, Heidelberg (1999)
Geldenhuys, J., Valmari, A.: Techniques for smaller intermediary bdds. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 233–247. Springer, Heidelberg (2001)
Lind-Nielsen, J.: Buddy, a binary decision diagram package. Technical Report ITTR 1999-028, Institute of Information Technology Technical University of Denmark (1999), http://cs.it.dtu.dk/buddy
Pastor, E., Roig, O., Cortadella, J., Badia, R.M.: Petri net analysis using boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 416–435. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haddad, S., Ilié, JM., Klai, K. (2004). Design and Evaluation of a Symbolic and Abstraction-Based Model Checker. In: Wang, F. (eds) Automated Technology for Verification and Analysis. ATVA 2004. Lecture Notes in Computer Science, vol 3299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30476-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-30476-0_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23610-8
Online ISBN: 978-3-540-30476-0
eBook Packages: Springer Book Archive