Author name cluster

Henrik Hulgaard

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

2 author rows

I&C Journal 2002 Journal Article

Boolean Expression Diagrams

Henrik Reif Andersen
Henrik Hulgaard

This paper presents a new data structure called boolean expression diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of binary decision diagrams (BDDs) which can represent any Boolean circuit in linear space. Two algorithms are described for transforming a BED into a reduced ordered BDD. One is a generalized version of the BDD apply-operator while the other can exploit the structural information of the Boolean expression. This ability is demonstrated by verifying that two different circuit implementations of a 16-bit multiplier implement the same Boolean function. Using BEDs, this verification problem is solved efficiently, while using standard BDD techniques this problem is infeasible. Generally, BEDs are useful in applications, for example tautology checking, where the end-result as a reduced ordered BDD is small. Moreover, using operators for substitution and existential quantification they allow for the verification of large hierarchical circuits.

Details DOI

CSL Conference 1999 Conference Paper

Difference Decision Diagrams

Jesper B. Møller
Jakob Lichtenberg
Henrik Reif Andersen
Henrik Hulgaard

Abstract This paper describes a newdata structure, difference decision diagrams (DDDs), for representing a Boolean logic over inequalities of the form x-y ≤ c where the variables are integer or real-valued. We give algorithms for manipulating DDDs and for determining validity, satisfiability, and equivalence. DDDs enable an efficient verification of timed systems modeled as, for example, timed automata or timed Petri nets, since both the states and their associated timing information are represented symbolically, similar to how BDDs represent Boolean predicates. We demonstrate the efficiency of DDDs by analyzing a timed system and compare the results with the tools Kronos and U ppaal.

Details