F ::= false | true | x - y < d | x - y <= d | not F | F1 or F2 | F1 and F2 | exists x.F
where x and y are integer- or real-valued variables, d is a constant, and F is a formula.
DDDs enable a symbolic 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. DDDs share many properties with binary decision diagrams (BDDs): (1) they are ordered, (2) they can be reduced making it possible to check for tautology and satisfiability in constant time, and (3) many of the algorithms and techniques for BDDs can be generalized to apply to DDDs.
Check out the DDD Demo page.
Browse DDD publications.