Difference Decision Diagrams
Jesper Møller
Jakob Lichtenberg
Henrik Reif Andersen
Henrik Hulgaard
February 1999
Abstract
This paper describes a new data structure, difference decision
diagrams (DDDs), for representing a Boolean logic over inequalities
of the form x-y < c and x-y <= c where the
variables are integer or real-valued.
We give algorithms for manipulating DDDs and for
determining functional properties (tautology, 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 can be
represented symbolically, similar to how ROBDDs represent
Boolean predicates.
