Difference Bound Matrices

Difference Bound Matrices (DBMs) [2] are a data structure used to represent a type of convex polytope, often referred to as zones. DBMs find applications in various fields, such as timed automata model checking and static program analysis. This entry formalizes DBMs and the operations for inclusion checking, intersection, variable reset, upper-bound relaxation, and extrapolation (as used in timed automata model checking). With the help of the Imperative Refinement Framework, efficient imperative implementations of these operations are also provided. For each zone, there exists a canonical DBM. The characteristic properties of canonical forms are proved, including the fact that DBMs can be transformed into canonical form using the Floyd-Warshall algorithm. This entry is part of the work described in a paper by the authors of this entry [4] and a PhD thesis [3].