Difference Decision Diagrams
Jesper Møller
Jakob Lichtenberg
Henrik Reif Andersen
Henrik Hulgaard
September 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 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 UPPAAL.
