Abstract
Symbolic model-checking using binary decision diagrams (BDD) can allow to represent very large state spaces. BDD give good results for synchronous systems, particularly for circuits that are well adapted to a binary encoding of a state. However both the operation definition mechanism (using more BDD) and the state representation (purely linear traversal from root to leaves) show their limits when trying to tackle globally asynchronous and typed specifications. Data Decision Diagrams (DDD) [7] are a directed acyclic graph structure that manipulates(a priori unbounded) integer domain variables, and which offers a flexible and compositional definition of operations through inductive homomorphisms.
We first introduce a new transitive closure unary operator for homomorphisms, that heavily reduces the intermediate peak size effect common to symbolic approaches. We then extend the DDD definition to introduce hierarchy in the data structure. We define Set Decision Diagrams, in which a variable’s domain is a set of values. Concretely, it means the arcs of an SDD may be labeled with an SDD (or a DDD), introducing the possibility of arbitrary depth nesting in the data structure. We show how this data structure and operation framework is particularly adapted to the computation and representation of structured state-spaces, and thus shows good potential for symbolic model-checking of software systems, a problem that is difficult for plain BDD representations.
Chapter PDF
Similar content being viewed by others
Keywords
- Parallel Composition
- Label Transition System
- Binary Decision Diagram
- Assignment Sequence
- Synchronization Transition
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Burch, J.R., Clarke, E.M., McMillan, K.L.: Symbolic model checking: 1020 states and beyond. Information and Computation (Special issue for best papers from LICS90) 98(2), 153–181 (1992)
Ciardo, G., Lüttgen, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 103–122. Springer, Heidelberg (2000)
Ciardo, G., Marmorstein, R., Siminiceanu, R.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379–393. Springer, Heidelberg (2003)
Ciardo, G.: Reachability set generation for petri nets: Can brute force be smart? In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 17–34. Springer, Heidelberg (2004)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV version 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 359. Springer, Heidelberg (2002)
Couvreur, J.-M., Encrenaz, E., Paviot-Adet, E., Poitrenaud, D., Wacrenier, P.-A.: Data decision diagrams for petri net analysis. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 101–120. Springer, Heidelberg (2002)
Garavel, H.: A net generated from lotos by cadp ( http://www.inrialpes.fr/vasy/cadp ). In: PetriNets@daimi.au.dk mailing list. Posted 28/07/03 and follow-up with performance of 4 tools on 26/09/03
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)
Gupta, A., Fisher, A.L.: Representation and symbolic manipulation of linearly inductive boolean functions. In: ICCAD 1993, pp. 111–116 (1993)
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: Halaas, A., Denyer, P.B. (eds.) International Conference on Very Large Scale Integration, Edinburgh, Scotland, pp. 49–58. North-Holland, Amsterdam (1991)
Kordon, F., Lemoine, M. (eds.): Formal Methods for Embedded Distributed Systems How to master the complexity. Kluwer Academic Publishers, Dordrecht (2004)
Miner, A.S., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 6–25. Springer, Heidelberg (1999)
Petrucci, L.: Design and validation of a controller. In: Proceedings of the 4th World Multiconference on Systemics, Cybernetics and Informatics (SCI 2000), Orlando, Florida, USA, pp. 684–688 (July 2000)
Thierry-Mieg, Y., Ilié, J.-M., Poitrenaud, D.: A symbolic symbolic state space representation. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 276–291. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 IFIP International Federation for Information Processing
About this paper
Cite this paper
Couvreur, JM., Thierry-Mieg, Y. (2005). Hierarchical Decision Diagrams to Exploit Model Structure. In: Wang, F. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2005. FORTE 2005. Lecture Notes in Computer Science, vol 3731. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562436_32
Download citation
DOI: https://doi.org/10.1007/11562436_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29189-3
Online ISBN: 978-3-540-32084-5
eBook Packages: Computer ScienceComputer Science (R0)