difference bound matrix

A difference bound matrix is used to represents some kind of convex polytopes. Those polytopes are called zone. They are now defined. Formally, a zone is defined by equations of the form $x\backslash le\; c$, $x\backslash ge\; c$, $x\_1\backslash le\; x\_2+c$ and $x\_1\backslash ge\; x\_2+c$, with $x\_1$ and $x\_2$ some variables, and $c$ a constant.

Zones have originally be called region,{{cite book |last1=Dill |first1=David L|title=Automatic Verification Methods for Finite State Systems |chapter=Timing assumptions and verification of finite-state concurrent systems |series=Lecture Notes in Computer Science |date=1990|volume=407 |pages=197–212|isbn=978-3-540-52148-8| doi=10.1007/3-540-52148-8_17|doi-access=free}} but nowadays this name usually denote region, a special kind of zone. Intuitively, a region can be considered as a minimal non-empty zones, in which the constants used in constraint are bounded.

Given $n$ variables, there are exactly $n(n+1)$ different non-redundant constraints possible, $n$ constraints which use a single variable and an upper bound, $n$ constraints which uses a single variable and a lower bound, and for each of the $n^2$ ordered pairs of variable $(x,y)$, an upper bound on $x-y$. However, an arbitrary convex polytope in $\backslash mathbb\; R^n$ may require an arbitrarily great number of constraints. Even when $n=2$, there can be an arbitrary great number of non-redundant constraints

As stated in the introduction, we consider a zone defined by a set of statements of the form $x\_1\backslash le\; c$, $x\_1\backslash ge\; c$, $x\_1\backslash le\; x\_2+c$ and $x\_1\backslash ge\; x\_2+c$, with $x\_1$ and $x\_2$ some variables, and $c$ a constant. However some of those constraints are either contradictory or redundant. We now give such examples.

• the constraints $x\_1\backslash le3$ and $x\_1\backslash ge4$ are contradictory. Hence, when two such constraints are found, the zone defined is empty. File:X incompatible.png
• the constraints $x\_1\backslash le3$ and $x\_1\backslash le\; 4$ are redundant. The second constraint being implied by the first one. Hence, when two such constraints are found in the definition of the zone, the second constraint may be removed. File:Showing x 1 less than 3 and 4.png

We also give example showing how to generate new constraints from existing constraints. For each pair of clocks $x\_1$ and $x\_2$, the DBM has a constraint of the form $x\_1\backslash prec\; x\_2+c$, where $\backslash prec$ is either < or ≤. If no such constraint can be found, the constraint $x\_1\backslash prec\; x\_2+\backslash infty$ can be added to the zone definition without loss of generality. But in some case, a more precise constraint can be found. Such an example is now going to be given.

• the constraints $x\_1\backslash le\; 3$, $x\_2\backslash ge-3$ implies that $x\_1\backslash le\; x\_2+6$. Thus, assuming that no other constraint such as $x\_1\backslash le\; x\_2+5$ or
• the constraints $x\_2\backslash le\; 3$, $x\_1\backslash le\; x\_2+3$ implies that $x\_1\backslash le\; 6$. Thus, assuming that no other constraint such as $x\_1\backslash le\; 5$ or belongs to the definition, the constraint $x\_1\backslash le\; 6$ is added to the zone definition. File:X less than 3, x less than y+3.png
• the constraints $x\_1\backslash le\; x\_2+3$, $x\_2\backslash le\; x\_3+3$ implies that $x\_1\backslash le\; x\_3+6$. Thus, assuming that no other constraint such as $x\_1\backslash le\; x\_3+5$ or belongs to the definition, the constraint $x\_1\backslash le\; x\_3+6$ is added to the zone definition.

Actually, the two first cases above are particular cases of the third cases. Indeed, $x\_1\backslash le3$ and $x\_2\backslash ge-3$ can be rewritten as $x\_1\backslash le\; 0+3$ and $0\backslash le\; x\_2+3$ respectively. And thus, the constraint $x\_1\backslash le\; x\_2+6$ added in the first example is similar to the constraint added in the third example.

We now fix a monoid $(M,0,+)$ which is a subset of the real line. 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. Furthermore, we introduce an algebra for atomic constraints. This algebra is similar to the tropical semiring, with two modifications:

• An arbitrary ordered monoid may be used instead of $\backslash mathbb\{R\}$.
• In order to distinguish between "" and "$\backslash le\; m$", the set of elements of the algebra must contain information stating whether the order is strict or not.

The set of satisfiable constraints is defined as the set of pairs of the form:

• $(\backslash le,m)$, with $m\backslash in\; M$, which represents a constraint of the form $\backslash le\; m$,
• , with $m\backslash in\; M$, where $m$ is not a minimal element of $M$, which represents a constraint of the form ,
• , which represents the absence of constraint.

The set of constraint contains all satisfiable constraints and contains also the following unsatisfiable constraint:

• .

The subset $\backslash \{q\backslash in\backslash mathbb\; Q\backslash mid\; q\backslash le\backslash sqrt2\backslash \}$ can not be defined using this kind of 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.

In order to generate a single constraint from a pair of constraints applied to the same (pair of) variable, we formalize the notion of intersection of constraints and of order over constraints. Similarly, in order to define a new constraints from existing constraints, a notion of sum of constraint must also be defined.

We now define an order relation over constraints. This order symbolize the inclusion relation.

First, the set is considered as an ordered set, with < being inferior to ≤. Intuitively, this order is chosen because the set defined by is strictly included in the set defined by $x\backslash le\; c$. We then state that the constraint $(\backslash prec\_1,m\_1)$ is smaller than $(\backslash prec\_2,m\_2)$ if either or ($m\_1=m\_2$ and $\backslash prec\_1$ is less than $\backslash prec\_2$). That is, the order on constraints is the lexicographical order applied from right to left. Note that this order is a total order. If $M$ has the least-upper-bound property (or greatest-lower-bound property) then the set of constraints also have it.

The intersection of two constraints, denoted as $(\backslash prec\_1,m\_1)\backslash sqcap(\backslash prec\_2,m\_2)$, is then simply defined as the minimum of those two constraints. If $M$ has the greatest-lower bound property then the intersection of an infinite number of constraints is also defined.

Given two variables $x\_1$ and $x\_2$ to which are applied constraints $(\backslash prec\_1,m\_1)$ and $(\backslash prec\_2,m\_2)$, we now explain how to generate the constraint satisfied by $x\_1+x\_2$. This constraint is called the sum of the two above-mentioned constraint, is denoted as $(\backslash prec\_1,m\_1)+(\backslash prec\_2,m\_2)$ and is defined as $(\backslash min(\backslash prec\_1,\backslash prec\_2),m\_1+m\_2)$.

Here is a list of algebraic properties satisfied by the set of constraints.

• Both operations are associative and commutative,
• Sum is distributive over intersection, that is, for any three constraints, $((\backslash prec\_1,m\_1)\backslash sqcap(\backslash prec\_2,m\_2))+(\backslash prec\_3,m\_3)$ equals $((\backslash prec\_1,m\_1)+(\backslash prec\_3,m\_3))\backslash sqcap((\backslash prec\_2,m\_2)+(\backslash prec\_3,m\_3))$,
• The intersection operation is idempotent,
• The constraint is an identity for the intersection operation,
• The constraint $(\backslash le,0)$ is an identity for the sum operation,

Furthermore, the following algebraic properties holds over satisfiable constraints:

• The constraint is a zero for the sum operation,
• It follows that the set of satisfiable constraints is an idempotent semiring, with as zero and $(\backslash le,0)$ as unity.
• If 0 is the minimum element of $M$, then $(\backslash le,0)$ is a zero for the intersection constraints over satisfiable constraints.

Over non-satisfiable constraints both operations have the same zero, which is . 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.

=== DBMs ===

Given a set of $n$ variables, $x\_1,\backslash dots,x\_n$, a DBM is a matrix with column and rows indexed by $0,x\_1,\backslash dots,x\_n$ and the entries are constraints. Intuitively, for a column $C$ and a row $R$, the value $m$ at position $(C,R)$ represents $C\backslash prec\; R+m$. Thus, the zone defined by a matrix $D((\backslash prec\_\{C,R\},m\_\{C,R\}))\_\{C,R\backslash in\backslash \{0,x\_1,\backslash dots,x\_n\}\backslash \}$, denoted by $\backslash mathcal\; R(D)$, is $\backslash \{(x\_1,\backslash dots,x\_n)\backslash in\backslash mathbb\; R\backslash mid\; \backslash bigwedge\_\{C,R\backslash in\backslash \{0,x\_1,\backslash dots,x\_n\backslash \}\}C\backslash prec\_\{C,R\}R+m\_\{C,R\}\backslash \}$.

Note that $C\backslash prec\; R+m$ is equivalent to $C-R\backslash prec\; m$, thus the entry $(\backslash prec,m)$ is still essentially an upper bound. Note however that, since we consider a monoid $M$, for some values of $C$ and $R$ the real $C-R$ does not actually belong to the monoid.

Before introducing the definition of a canonical DBM, we need to define and discuss an order relation on those matrices.

A matrix $D$ is considered to be smaller than a matrix $D\text{'}$ if each of its entries are smaller. Note that this order is not total. Given two DBMs $D$ and $D\text{'}$, if $D$ is smaller than or equal to $D\text{'}$, then $\backslash mathcal\; R(D)\backslash subseteq\backslash mathcal\; R(D\text{'})$.

The greatest-lower-bound of two matrices $D$ and $D\text{'}$, denoted by $D\backslash sqcap\; D\text{'}$, has as its $(a,b)$ entry the value $(\backslash prec\_\{a,b\},m\_\{a,b\})\backslash sqcap(\backslash prec\text{'}\_\{a,b\},m\text{'}\_\{a,b\})$. Note that since $\backslash sqcap$ is the «sum» operation of the semiring of constraints, the operation $\backslash sqcap$ is the «sum» of two DBMs where the set of DBMs is considered as a module.

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 $M$ satisfies the greatest-lower-bound property.

The intersection of matrices/zones is defined. The union operation is not defined, and indeed, a union of zone is not a zone in general.

For an arbitrary set $\backslash mathcal\; D$ of matrices which all defines the same zone $Z$, $\backslash sqcap\_\{D\backslash in\backslash mathcal\; D\}D$ also defines $Z$. It thus follow that, as long as $M$ has the greatest-lower-bound property, each zone which is defined by at least a matrix has a unique minimal matrix defining it. This matrix is called the canonical DBM of $Z$.

We restate the definition of a canonical difference bound matrix. It is a DBM such that no smaller matrix defines the same set. It is explained below how to check whether a matrix is a DBM, and otherwise how to compute a DBM from an arbitrary matrix such that both matrices represents the same set. But first, we give some examples.

We first consider the case where there is a single clock $x\_1$.

We first give the canonical DBM for $\backslash mathbb\; R$. We then introduce another DBM which encode the set $\backslash mathbb\; R$. This allow to find constraints which must be satisfied by any DBM.

The canonical DBM of the set of real is . It represents the constraints $0\backslash le\; 0+0$, $x\_1\backslash le\; 0+\backslash infty$, $0\backslash le\; x\_1+\backslash infty$ and $0\backslash le0+0$. All of those constraints are satisfied independently of the value assigned to $x\_1$. In the remaining of the discussion, we will not explicitly describe constraints due to entries of the form , since those constraints are systematically satisfied.

The DBM also encodes the set of real. It contains the constraints and which are satisfied independently on the value of $x\_1$. This show that in a canonical DBM $D$, a diagonal entry is never greater than $(\backslash le,0)$, because the matrix obtained from $D$ by replacing the diagonal entry by $(\backslash le,0)$ defines the same set and is smaller than $D$.

We now consider many matrices which all encodes the empty set. We first give the canonical DBM for the empty set. We then explain why each of the DBM encodes the empty set. This allow to find constraints which must be satisfied by any DBM.

The canonical DBM of the empty set, over one variable, is . Indeed, it represents the set satisfying the constraint , , and . Those constraints are unsatisfiable.

The DBM also encodes the empty set. Indeed, it contains the constraint which is unsatisfiable. More generally, this show that no entry can be unless all entries are .

The DBM also encodes the empty set. Indeed, it contains the constraint which is unsatisfiable. More generally, this show that the entry in the diagonal line can not be smaller than $(\backslash le,0)$ unless it is .

The DBM also encodes the empty set. Indeed, it contains the constraints and $x\_1\backslash le\; -1$ which are contradictory. More generally, this show that, for each $C,R\backslash in\backslash \{0,x\_1,\backslash dots,x\_n\backslash \}$, if $m\_\{C,R\}=-m\_\{R,C\}$, then $\backslash prec\_\{R,C\}$ and $\backslash prec\_\{C,R\}$ are both equal to ≤.

The DBM also encodes the empty set. Indeed, it contains the constraints $0\backslash le\; x\_1+1$ and $x\_1\backslash le\; -2$ which are contradictory. More generally, this show that for each $C,R\backslash in\backslash \{0,x\_1,\backslash dots,x\_n\backslash \}$, $-m\_\{C,R\}\backslash le\; m\_\{R,C\}$, unless $m\_\{C,R\}$ is $-\backslash infty$.

The examples given in this section are similar to the examples given in the Example section above. This time, they are given as DBM.

The DBM represents the set satisfying the constraints $x\_2\backslash le\; 3$ and $x\_1\backslash le\; x\_2+3$. As mentioned in the Example section, both of those constraints implies that $x\_1\backslash le\; 6$. It means that the DBM encodes the same zone. Actually, it is the DBM of this zone. This shows that in any DBM $((\backslash prec\_\{C,R\},m\_\{C,R\}))\_\{c,r\backslash in\backslash \{0,x\_1,\backslash dots,x\_n\backslash \}\}$, for each $1\backslash le\; i,j\backslash le\; n$, the constraint $(\backslash prec\_\{x\_i,0\},m\_\{x\_i,0\})$ is smaller than the constraint $(\backslash prec\_\{x\_j,0\},m\_\{x\_j,0\})+(\backslash prec\_\{x\_i,x\_j\},m\_\{x\_i,x\_j\})$.

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 $((\backslash prec\_\{C,R\},m\_\{C,R\}))\_\{c,r\backslash in\backslash \{0,x\_1,\backslash dots,x\_n\backslash \}\}$, for each $a,b,c\backslash in\backslash \{0,x\_1,\backslash dots,x\_n\backslash \}$, the constraint $(\backslash prec\_\{a,b\},m\_\{a,b\})$ is smaller than the constraint $(\backslash prec\_\{c,b\},m\_\{c,b\})+(\backslash prec\_\{a,c\},m\_\{a,c\})$.

As explained in the introduction of the section Difference Bound Matrix, a canonical DBM is a DBM whose rows and columns are indexed by $(0,x\_1,\backslash dots,x\_n)$, whose entries are constraints. Furthermore, it follows one of the following equivalent properties.

• there are no smaller DBM defining the same zone,
• for each $a,b,c\backslash in\backslash \{0,x\_1,\backslash dots,x\_n\backslash \}$, the constraint $(\backslash prec\_\{a,b\},m\_\{a,b\})$ is smaller than the constraint $(\backslash prec\_\{c,b\},m\_\{c,b\})+(\backslash prec\_\{a,c\},m\_\{a,c\})$
• given the directed graph $G$ with edges $\backslash \{0,x\_1,\backslash dots,x\_n\backslash \}$ and arrows $(a,b)$ labelled by $(\backslash prec\_\{a,b\},m\_\{a,b\})$, the shortest path from any edge $a$ to any edge $b$ is the arrow $(a,b)$. This graph is called the potential graph of the DBM.

The last definition can be directly used to compute the canonical DBM associated to a DBM. It suffices to apply the Floyd–Warshall algorithm to the graph and associates to each entry $(a,b)$ the shortest path from $a$ to $b$ in the graph. 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.

We first recall operations which were considered above:

• testing for the inclusion of a zone $Z\_1$ in a zone $Z\_2$ is done by testing whether the canonical DBM of $Z\_1$ is smaller than or equal to the DBM of $Z\_2$,
• A DBM for the intersection of a set of zones is the greatest-lower-bound of the DBM of those zones,
• testing for zone emptiness consists in checking whether the canonical DBM of the zone consists only of ,
• testing whether a zone is the entire space consists in checking whether the DBM of the zone consists only of .

We now describe operations which were not considered above. The first operations described below have clear geometrical meaning. The last ones become corresponds to operations which are more natural for clock valuations.

The Minkowski sum of two zones, defined by two DBMs $D$ and $D\text{'}$, is defined by the DBM $D+D\text{'}$ whose $(a,b)$ entry is $D\_\{a,b\}+D\text{'}\_\{a,b\}$. Note that since $+$ is the «product» operation of the semiring of constraints, the operation $+$ over DBMs is not actually an operation of the module of DBM.

In particular, it follows that, in order to translate a zone $Z$ by a direction $v$, it suffices to add the DBM of $\backslash \{v\backslash \}$ to the DBM of $Z$.

Let $d\backslash in\; M$ a constant.

Given a vector $\backslash vec\; x=(x\_1,\backslash dots,x\_n)$, and an index $1\backslash le\; i\backslash le\; n$, the projection of the $i$-th component of $\backslash vec\; x$ to $d$ is the vector $(x\_1,\backslash dots,x\_\{i-1\},d,x\_\{i+1\},\backslash dots,x\_n)$. In the language of clock, for $d=0$, this corresponds to resetting the $i$-th clock.

Projecting the $i$-th component of a zone $Z$ to $d$ consists simply in the set of vectors of $Z$ with their $i$-th component to $d$. This is implemented on DBM by setting the components $(x\_\{i\},a)$ to $(\backslash le,d)+D(0,a)$ and the components $(a,x\_\{i\})$ to $(\backslash le,-d)+D(0,a)$

Let us call the future the zone $F=\backslash \{(t,\backslash dots,t)\backslash mid\; t\backslash in\backslash mathbb\; R\_\{\backslash ge0\}\backslash \}$ and the past the zone $P=\backslash \{(-t,\backslash dots,-t)\backslash mid\; t\backslash in\backslash mathbb\; R\_\{\backslash ge0\}\backslash \}$. Given a point $\backslash vec\; x=(x\_1,\backslash dots,x\_n)\backslash in\backslash mathbb\; R^n$, the future of $\backslash vec\; x$ is defined as $\backslash \{(x\_1+t,\backslash dots,x\_n+t)\backslash mid\; t\backslash in\backslash mathbb\; R\_\{\backslash ge0\}\backslash \}=F+\backslash \{\backslash vec\; x\backslash \}$, and the past of $\backslash vec\; x$ is defined as $P+\backslash \{\backslash vec\; x\backslash \}$.

The names future and past comes from the notion of clock. If a set of $n$ clocks are assigned to the values $x\_1$, $x\_2$, etc. then in their future, the set of assignment they'll have is the future of $\backslash vec\; x$.

Given a zone $Z$, the future of $Z$ are the union of the future of each points of the zone. The definition of the past of a zone is similar. The future of a zone can thus be defined as $F+Z$, and hence can easily be implemented as a sum of DBMs. However, there is even a simpler algorithm to apply to DBM. It suffices to change every entries $(x\_i,0)$ to . Similarly, the past of a zone can be computed by setting every entries $(0,x\_i)$ to .

• Region (model checking) – a zone, minimal under inclusion, satisfying some properties

• [https://moves.rwth-aachen.de/wp-content/uploads/WS1617/amc/amc16_lec20_reduced.pdf Difference Bound Matrices Lecture #20 of Advanced Model Checking Joost-Pieter Katoen]
• {{cite book |last1=Péron |first1=Mathias|last2=Halbwachs|first2=Nicolas|title=Verification, Model Checking, and Abstract Interpretation |chapter=An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints |series=Lecture Notes in Computer Science |date=2008|volume=4349 |pages=268–282|isbn=978-3-540-69735-0| doi=10.1007/978-3-540-69738-1_20|chapter-url=http://hal.archives-ouvertes.fr/docs/00/26/24/22/PDF/PeronHalbwachsVMCAI07.pdf|doi-access=free}}

{{Data structures}}

{{DEFAULTSORT:Data Structure}}

Category:Polytopes

Polytope

Category:Geometric data structures