Technical Report CS729

Authors: O. Grumberg, T. Djerassi-Shintel, N. Shintel, E. Aharonson
PDF - RevisedCS0729.revised.pdf

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 bottle-necks of the algorithm:

  • Given two automata, representing two processes, build an automaton which represents their communication behavior.
  • Convert non-deterministic 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.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 1992
To the main CS technical reports page

Computer science department, Technion