Difference decision diagrams

Abstract This paper describes a new data structure, difference decision diagrams (DDDs), for representing a Boolean logic over inequalities of the form ¡£¢¥¤§¦©¨ 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.