Tilbage til hovedside

Difference Decision Diagrams

A Difference Decision Diagram (DDD) is a data structure for representing a first-order Boolean logic over inequalities of the form x - y < d and x - y <= d, that is formulae of the form:

    F  ::=  false  |  true  |  x - y < d  |  x - y <= d  |  not F  |  F1 or F2  |  F1 and F2  |  exists x.F

where x and y are integer- or real-valued variables, d is a constant, and F is a formula.

DDDs enable a symbolic 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.  DDDs share many properties with binary decision diagrams (BDDs): (1) they are ordered, (2) they can be reduced making it possible to check for tautology and satisfiability in constant time, and (3) many of the algorithms and techniques for BDDs can be generalized to apply to DDDs.

Online DDD Demo

Check out the DDD Demo page.

Publications

Browse DDD publications.

Authors

The DDD data structure is developed by Henrik R. Andersen, Henrik Hulgaard, Jesper Møller, and Jakob Lichtenberg, from the IT University of Copenhagen. The development of the DDD data structure is part of the VERIS-project. The DDD data structure is currently being patented.