Abstract: 
In his Master Project Thesis, Rami Marelly, under the supervision of Dr. Orna
Grumberg, presented a tool for automatic verification of distributed algorithms.
In the different phases of the algorithm, huge automata are created which caused a problem
of very large memory consumption, exceeding the capabilities of many computer systems. In order to reduce the memory consumption (at least in the average case), a realization using BDD was
suggested. A Binary Decision Diagram (BDD), presented by Bryant is a canonical data structure for the representation of boolean functions. A binary function is represented by a directed acyclic graph.
In the worst case this graph might be exponential in size, but in typical applications
it is much smaller. The time complexity of most manipulations on this structure is proportional to its size.
Our project is intended to check the feasibility of an implementation using BDD, on three
of the major bottlenecks of the algorithm:
 Given two automata, representing two processes, build an automaton which
represents their communication behavior.
 Convert nondeterministic automata which represent communication behaviors into deterministic ones. This step is a necessity for the next one.
 For a given pair of states, in two, possibly different communication behaviors,
check whether they are state equivalent.
The project is implemented in C using a BDD  library written by David Long.
