Difference Decision Diagrams

This paper describes a new data structure, difference decision diagrams (DDDs), for representing a Boolean logic over inequalities of the form ¡£¢¥¤§¦©¨ and ¡¢¥¤¨ where the variables are integer or real-valued. We give algorithms for manipulating DDDs and for determining functional properties (tautology, 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 can be represented symbolically, similar to how ROBDDs represent Boolean predicates.

• Type: Conference
• Year: 1999
• Where: CSL
• Authors: Jesper B. Møller, Jakob Lichtenberg, Henrik Reif Andersen, Henrik Hulgaard
• Keywords: Automated Reasoning, Boolean Logic, CSL 1999, Difference Decision Diagrams, Timed Systems