Binary Decision Graphs

Abstract. Binary Decision Graphs are an extension of Binary Decision Diagrams that can represent some infinite boolean functions. Three refinements of BDGs corresponding to classes of infinite functions of increasing complexity are presented. The first one is closed by intersection and union, the second one by intersection, and the last one by all boolean operations. The first two classes give rise to a canonical representation, which, when restricted to finite functions, are the classical BDDs. The paper also gives new insights in to the notion of variable names and the possibility of sharing variable names that can be of interest in the case of finite functions.

• Type: Conference
• Year: 1999
• Where: SAS
• Authors: Laurent Mauborgne
• Keywords: Binary Decision, Binary Decision Graphs, Formal Methods, Infinite Boolean Functions, SAS 1999