Nacer Tabib¹, Jean Michel Ilie² and Djamel Eddine Saidouni¹, ¹ Constantine 2 University, Algeria
and ²UPMC, France

This paper proposes a new framework based on Binary Decision Diagrams (BDD) for the graph distribution problem in the context of explicit model checking. The BDD are yet used to represent the state space for a symbolic verification model checking. Thus, we took advantage of high compression ratio of BDD to encode not only the state space, but also the place where each state will be put. So, a fitness function that allows a good balance load of states over the nodes of an homogeneous network is used. Furthermore, a detailed explanation of how to calculate the inter-site edges between different nodes based on the adapted data structure is presented.

Graph distribution, Binary Decision Diagram, State space generation, Formal verification, Model Checking.