Difference Decision Diagrams

Jesper Møller
Jakob Lichtenberg

August 1998

Summary

This report is a Master's Thesis on a new data structure called difference decision diagrams and consists of four parts:

A presentation of a first-order logic for difference constraint expressions. Difference constraint expressions are Boolean combinations of difference constraints, x-y<c and x-y<=c, over integer or real-valued variables. We prove that determining satisfiability of quantifier-free difference constraint expressions is NP-complete. For quantified difference constraint expressions the problem is PSPACE-hard.
A specification of difference decision diagrams (DDDs). DDDs are a data structure to represent difference constraint expressions, and combine symbolic representation of states known from BDDs with timing constraint information. We use a built-in feasibility check to make DDDs semi-canonical. Semi-canonical DDDs make testing of functional properties (such as satisfiability and validity) constant time operations. This part furthermore contains a thorough description of the core algorithms to construct DDDs.
A number of applications of difference decision diagrams. We show how to model timing constraints of combinational circuits, and we present a DDD-based algorithm to compute the reachable state space of a timed Petri net. Furthermore, we show how to verify non-Boolean properties of an imperative programming language.
An implementation of difference decision diagrams. This part contains a C library with a Moscow ML interface, and a number of example programs.