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.