No label defined (Q4934627)

Binary decision diagrams allow the representation and manipulation of propositional formulas or, equivalently, of boolean functions. Their use is meanwhile classical in several fields of computer science: the verification of hardware, the testing and optimization of sequential (i.e. finite state) circuits, model checking, the optimization of logical circuits, graph algorithms. The paper presents a detailed introduction into the topic. After a precise definition of binary decision diagrams the paper proves their canonicity. Next, algorithms for manipulating these diagrams are described in some detail and their time complexity is discussed. A further section is devoted to the impact of the ordering of the variables on the size of the diagram. Finally, the use of binary decision diagrams is illustrated by an extensive discussion of the verification of sequential circuits. The paper is precise and includes, for instance, proofs of the theorems. Thanks to the numerous comments and the large number of simple examples the paper is quite easy to read. It does not require particular background knowledge. It is unfortunate that a few minor deficiencies -- such as the use of not yet defined notation -- unnecessarily harm a fluent reading. The paper may be recommended to all those who look for a clear, authorative and easy-to-read introduction into binary decision diagrams. For the entire collection see [Zbl 0919.00073].