Clock difference diagrams
Kim G. Larsen, Justin Pearson, Carsten Weise, Wang Yi · 1999
In this paper, we present Clock Difference Diagrams, a new BDD- like data-structure for effective representation and manipulation of certain non-convex subsets of the Euclidean space, notably those encountered in verification of timed automata. It is shown that all set-theoretic operations including inclusion checking may be carried out efficiently on Clock Difference Diagrams. Other central operations needed for analysing timed automata (e.g. future- and reset-operations), are readily defined using an effectively obtained, relative normal form. A version of the real-time verification tool Uppaal using Clock Difference Diagrams as the main data-structure has been implemented. Experimental results demonstrate significant space-savings: between 46% and 99% for a number of industrial examples.