Difference bound matrix
In model checking, a field of computer science, a difference bound matrix (DBM) is a data structure used to represent some convex polytopes called zones.
This structure can be used to efficiently implement some geometrical operations over zones, such as testing emptyness, inclusion, equality, and computing the intersection and the sum of two zones.
It is, for example, used in the Uppaal model checker; where it is also distributed as an independent library.
A difference bound matrix is used to represents some kind of convex polytopes.
Intuitively, a region can be considered as a minimal non-empty zones, in which the constants used in constraint are bounded.
constraints which uses a single variable and a lower bound, and for each of the
This is the reason why DBMs can not be extended from zones to convex polytopes.
As stated in the introduction, we consider a zone defined by a set of statements of the form
can be added to the zone definition without loss of generality.
This monoid is traditionally the set of integers, rationals, reals, or their subset of non-negative numbers.
In order to define the data structure difference bound matrix, it is first required to give a data structure to encode atomic constraints.
More generally, some convex polytopes can not be defined when the ordered monoid does not have the least-upper-bound property, even if each of the constraints in its definition uses at most two variables.
has the greatest-lower bound property then the intersection of an infinite number of constraints is also defined.
Here is a list of algebraic properties satisfied by the set of constraints.
Thus, the set of constraints does not even form a semiring, because the identity of the intersection is distinct from the zero of the sum.
Before introducing the definition of a canonical DBM, we need to define and discuss an order relation on those matrices.
Similarly to the case of constraints, considered in section "Operation on constraints" above, the greatest-lower-bound of an infinite number of matrices is correctly defined as soon as
We restate the definition of a canonical difference bound matrix.
In the remaining of the discussion, we will not explicitly describe constraints due to entries of the form
We now consider many matrices which all encodes the empty set.
We then explain why each of the DBM encodes the empty set.
The canonical DBM of the empty set, over one variable, is
More generally, this show that the entry in the diagonal line can not be smaller than
As mentioned in the Example section, both of those constraints implies that
As explained in the Example section, the constant 0 can be considered as any variable, which leads to the more general rule: in any DBM
It suffices to apply the Floyd–Warshall algorithm to the graph and associates to each entry
If this algorithm detects a cycle of negative length, this means that the constraints are not satisfiable, and thus that the zone is empty.
As stated in the introduction, the main interest of DBMs is that they allow to easily and efficiently implements operations on zones.
The Minkowski sum of two zones, defined by two DBMs
Similarly, the past of a zone can be computed by setting every entries
