In: Proceedings of Formal Techniques for Networked and Distributed Systems -- FORTE 2004: 24th IFIP WG 6.1 International Conference, Madrid Spain, September 27-30, 2004, pages 276-291. Volume 3235 of Lecture Notes in Computer Science / David de Frutos-Escrig, Manuel Nunez (Eds.) --- Springer-Verlag, September 2004.
Abstract: Symmetry based approaches are known to attack the state space explosion problem encountered during the analysis of distributed systems. In another way, BDD-like encodings enable the management of huge data sets. In this paper, we show how to benefit from both approaches automatically. Hence, a quotient set is built from a coloured Petri net description modeling the system. The reachability set is managed under some explicit symbolic operations. Also, data representations are managed symbolically based on a recently introduced data structure, called Data Decisions Diagrams, that allow flexible definition of application specific operators. Performances yielded by our prototype are reported in the paper.
Keywords: Decision Diagrams; Symbolic Model-checking; Symbolic Reachability Graph; Well-Formed Petri Nets; Symmetry Detection.