Difference Decision Diagrams

12 years 4 months ago
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.
Jesper B. Møller, Jakob Lichtenberg, Henrik
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where CSL
Authors Jesper B. Møller, Jakob Lichtenberg, Henrik Reif Andersen, Henrik Hulgaard
Comments (0)