Technical Report CS729
||CHECKING FOR EQUIVALENCE OF COMMUNICATION BEHAVIORS USING BDD.
||O. Grumberg, T. Djerassi-Shintel, N. Shintel, E. Aharonson
|PDF - Revised||CS0729.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:
The project is implemented in C using a BDD - library written by David Long.
- 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.
|Copyright||The 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 (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/1992/CS/CS0729), 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