Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions^{}

Roberto Bagnara^{a}, Patricia M. Hill^{b}, Enea Zaffanella^{a}

aDepartment of Mathematics, University of Parma, Italy bSchool of Computing, University of Leeds, UK

Abstract

Deciding whether the union of two convex polyhedra is a convex polyhedron is a basic problem in polyhedral computation having important applications in the field of constrained control and in the synthesis, analysis, verification and optimization of hardware and software systems. In these application fields, though, general convex polyhedra are only one among many so-called numerical abstractions: these range from restricted families of (not necessarily closed) convex polyhedra to non-convex geometrical objects. We thus tackle the problem from an abstract point of view: for a wide range of numerical abstractions that can be modeled as bounded join-semilattices —that is, partial orders where any finite set of elements has a least upper bound—, we show necessary and sufficient conditions for the equivalence between the lattice-theoretic join and the set-theoretic union. For the case of closed convex polyhedra —which, as far as we know, is the only one already studied in the literature— we improve upon the state-of-the-art by providing a new algorithm with a better worst-case complexity. The results and algorithms presented for the other numerical abstractions are new to this paper. All the algorithms have been implemented, experimentally validated, and made available in the Parma Polyhedra Library.

Key words: polyhedron, union, convexity, abstract interpretation, numerical abstraction, powerset domain.

1. Introduction

For n ∈ ℕ, let 𝔻_{n} ⊂ ℘(ℝ^{n}) be a set of finitely-representable sets such that (𝔻_{n}, ⊆) is a bounded join-semilattice, that is, a minimum element exists as well as the least upper bound for all D_{1}, D_{2} ∈ 𝔻_{n}. Such least upper bound —let us denote it by D_{1} ⊎ D_{2} and call it the join of D_{1} and D_{2}— is, of course, not guaranteed to be equal to D_{1} ∪ D_{2}. More generally, we refer to the problem of deciding, for each finite set {D_{1}, …, D_{k}} ⊆ 𝔻_{n}, whether ⨄_{i=1}^{k} D_{i} = ⋃_{i=1}^{k} D_{i} as the exact join detection problem.

This work has been partly supported by PRIN project “AIDA2007 — Abstract Interpretation Design and Applications.”

Email addresses: bagnara@cs.unipr.it (Roberto Bagnara), hill@comp.leeds.ac.uk (Patricia M. Hill), zaffanella@cs.unipr.it (Enea Zaffanella)

Preprint submitted to Elsevier

Examples of 𝔻_{n} include n-dimensional convex polyhedra, either topologically closed or not necessarily so, restricted families of polyhedra characterized by interesting algorithmic complexities —such as bounded-difference and octagonal shapes—, Cartesian products of some families of intervals, and other “box-like” geometric objects where the intervals can have “holes” (for instance, Cartesian products of modulo intervals [33, 34] fall in this category). All these numerical abstractions allow to conveniently represent or approximate the constraints arising in constrained control (see, e.g., [26]) and, more generally, in the synthesis, analysis, verification and optimization of hardware and software systems (see, e.g., [8]).

The restrictions implied by convexity and/or by the “shapes” of the geometric objects in 𝔻_{n} are sometimes inappropriate for the application at hand. In these cases, one possibility is to consider finite sets of elements of 𝔻_{n}. For instance, many applications in the field of hardware/software verification use constructions like the finite powerset domain of [1]: this is a special case of disjunctive completion [22], where disjunctions are implemented by maintaining an explicit (hence finite) and non-redundant collection of elements of 𝔻_{n}. Non-redundancy means that a collection is made of maximal elements with respect to subset inclusion, so that no element is contained in another element in the collection. The finite powerset and similar constructions are such that Q_{1} = {D_{1}, …, D_{h−1}, D_{h}, …, D_{k}} and Q_{2} = {D_{1}, …, D_{h−1}, D} are two different representations for the same set, if ⋃_{i=h}^{k} D_{i} = ⨄_{i=h}^{k} D_{i} = D. The latter representation is clearly more desirable, and not only because —being more compact— it results in a better efficiency of all the involved algorithms. In the field of control engineering, the ability of efficiently simplifying Q_{1} into Q_{2} can be used to reduce the complexity of the solution to optimal control problems, thus allowing for the synthesis of cheaper control hardware [14, 37]. Similarly, the simplification of Q_{1} into Q_{2} can lead to improvements in loop optimizations obtained by automatic code generators such as CLooG [11]. In the same application area, this simplification allows for a reduction in the complexity of array data-flow analysis and for a simplification of quasi-affine selection trees (QUASTs). In loop optimization, dependences between program statements are modeled by parametric linear systems, whose solutions can be represented by QUASTs and computed by tools like PIP [23], which, however, can generate non-simplified QUASTs. These can be efficiently simplified provided there is an efficient procedure for deciding the exact join property. The exact join detection procedure can also be used as a preprocessing step for the extended convex hull problem [25].

Another important application of exact join detection comes from the field of static analysis via abstract interpretation [21, 22]. In abstract interpretation, static analysis is usually conducted by performing a fixpoint computation. Suppose we use the finite powerset domain (℘_{fn}(𝔻_{n}), ⊑, ∅, ⊔): this is the bounded join-semilattice of the finite and non-redundant subsets of 𝔻_{n} ordered by the relation given, for each Q_{1}, Q_{2} ∈ ℘_{fn}(𝔻_{n}), by

Q_{1} ⊑ Q_{2} ⟺ ∀D_{1} ∈ Q_{1} : ∃D_{2} ∈ Q_{2} . D_{1} ⊆ D_{2},

and ‘⊔’ is the least upper bound (join) operator induced by ‘⊑’ [4]. The system under analysis is approximated by a monotonic (so called) abstract semantic function A: ℘_{fn}(𝔻_{n}) → ℘_{fn}(𝔻_{n}), and the limit of the ascending chain given by A’s iterates,

A^{0}(∅), A^{1}(∅), A^{2}(∅), …,  (1)

is, by construction, a sound approximation of the analyzed system’s behavior. Since ℘_{fn}(𝔻_{n}) has infinite ascending chains, the standard abstract iteration sequence (1) may converge very slowly or fail to converge altogether. For this reason, a widening operator ∇: ℘_{fn}(𝔻_{n})^{2} → ℘_{fn}(𝔻_{n}) is introduced. This ensures that the sequence

B^{0}(∅), B^{1}(∅), B^{2}(∅), ….  (2)

where, for each Q ∈ ℘_{fn}(𝔻_{n}), B(Q) := Q ∇ (Q ⊔ A(Q)), is ultimately stationary and that the (finitely computable) fixpoint of B is a post-fixpoint of A, i.e., a sound approximation of the behavior of the system under consideration. In [4] three generic widening methodologies are presented for finite powerset abstract domains. A common trait of these methodologies is given by the fact that the precision/efficiency trade-off of the resulting widening can be greatly improved if domain elements are “pairwise merged” or even “fully merged.” Let the cardinality of a finite set S be denoted by # S. An element Q = {D_{1}, …, D_{h}} of ℘_{fn}(𝔻_{n}) is said to be pairwise merged if, for each R ⊆ Q, # R = 2 implies ⋃ R ≠ ⨄ R; the notion of being fully merged is obtained by replacing # R = 2 with # R ≥ 2 in the above.

In this paper, we tackle the problem of exact join detection for all the numerical abstractions that are in widespread use at the time of writing.^{1} This problem has been studied for convex polyhedra in [13]. We are not aware of any work that addresses the problem for other numerical abstractions.

In [13] the authors provide theoretical results and algorithms for the exact join detection problem applied to a pair of topologically closed convex polyhedra. Three different specializations of the problem are considered, depending on the chosen representation for the input polyhedra: H-polyhedra, described by constraints (halfspaces); V-polyhedra, described by generators (vertices); and VH-polyhedra, described by both constraints and generators.^{2} The algorithms for the H and V representations, which are based on Linear Programming techniques, enjoy a polynomial worst-case complexity bound; the algorithm for VHpolyhedra achieves a better, strongly polynomial bound. For the H-polyhedra case only, it is also shown how the algorithm can be generalized to more than two input polyhedra. An improved theoretical result for the case of more than two V-polytopes is stated in [10].

1Since numerical abstractions are so critical in the field of hardware and software analysis and verification, new ones are proposed on a regular basis.

2The algorithms in [13] for the V and VH representations only consider the case of bounded polyhedra, i.e., polytopes; the extension to the unbounded case can be found in [12].

The first contribution of the present paper is a theoretical result for the VHpolyhedra case, leading to the specification of a new algorithm improving upon the worst-case complexity bound of [12].

The second contribution is constituted by original results and algorithms concerning the exact join detection problem for the other numerical abstractions. For those that are restricted classes of topologically closed convex polyhedra, one could of course use the same algorithms used for the general case, but the efficiency would be poor. Consider that the applications of finite powersets of numerical abstractions range between two extremes:

• those using small-cardinality powersets of complex abstractions such as general polyhedra (see, for instance [16]);

• those using large-cardinality powersets of simple abstractions (for instance, verification tasks like the one described in [24], can be tackled this way).

So, in general, the simplicity of the abstractions is countered by their average number in the powersets. It is thus clear that specialized, efficient algorithms are needed for all numerical abstractions. In this paper we present algorithms, each backed with the corresponding correctness result, for the following numerical abstractions: not necessarily closed convex polyhedra, “box-like” geometric objects; rational (resp., integer) bounded difference shapes; and rational (resp., integer) octagonal shapes.

The plan of the paper is as follows. In Section 2 we introduce the required technical notation and terminology. In Section 3 we discuss the results and algorithms for convex polyhedra. The specialized results for boxes, bounded difference shapes and octagonal shapes are provided in Sections 4, 5 and 6, respectively. Section 7 concludes.

2. Preliminaries

The set of non-negative reals is denoted by ℝ_{+}. In the present paper, all topological arguments refer to the Euclidean topological space ℝ^{n}, for any positive integer n. If S ⊆ ℝ^{n}, then the topological closure of S is defined as ℂ(S) := ⋂{ C ⊆ ℝ^{n} | S ⊆ C and C is closed }.

For each i ∈ {1, …, n}, v_{i} denotes the i-th component of the (column) vector v ∈ ℝ^{n}; the projection on space dimension i for a set S ⊆ ℝ^{n} is denoted by π_{i}(S) := { v_{i} ∈ ℝ | v ∈ S }. We denote by 0 the vector of ℝ^{n} having all components equal to zero. A vector v ∈ ℝ^{n} can also be interpreted as a matrix in ℝ^{n×1} and manipulated accordingly with the usual definitions for addition, multiplication (both by a scalar and by another matrix), and transposition, which is denoted by v^{T}. The scalar product of v, w ∈ ℝ^{n}, denoted ⟨v, w⟩, is the real number v^{T}w = ∑_{i=1}^{n} v_{i}w_{i}.

For any relational operator ▷◁ ∈ {=, ≤, ≥, <, >}, we write v ▷◁ w to denote the conjunctive proposition ⋀_{i=1}^{n}(v_{i} ▷◁ w_{i}). Moreover, v ≠ w denotes the proposition ¬(v = w). We occasionally use the convenient notation a ▷◁_{1} b ▷◁_{2} c to denote the conjunction a ▷◁_{1} b ∧ b ▷◁_{2} c and do not distinguish conjunctions of propositions from sets of propositions.

2.1. Topologically Closed Convex Polyhedra

For each vector a ∈ ℝ^{n} and scalar b ∈ ℝ, where a ≠ 0, the linear non-strict inequality constraint β = (⟨a, x⟩ ≤ b) defines a topologically closed affine halfspace of ℝ^{n}. The linear equality constraint ⟨a, x⟩ = b defines an affine hyperplane. A topologically closed convex polyhedron is usually described as a finite system of linear equality and non-strict inequality constraints. Theoretically speaking, it is simpler to express each equality constraint as the intersection of the two half-spaces ⟨a, x⟩ ≤ b and ⟨−a, x⟩ ≤ −b. We do not distinguish between syntactically different constraints defining the same affine half-space so that, e.g., x ≤ 2 and 2x ≤ 4 are considered to be the same constraint.

We write con(C) to denote the polyhedron P ⊆ ℝ^{n} described by the finite constraint system C. Formally, we define

con(C) := { p ∈ ℝ^{n} | ∀β = (⟨a, x⟩ ≤ b) ∈ C : ⟨a, p⟩ ≤ b }.

The function ‘con’ enjoys an anti-monotonicity property, meaning that C_{1} ⊆ C_{2} implies con(C_{1}) ⊇ con(C_{2}).

Alternatively, the definition of a topologically closed convex polyhedron can be based on some of its geometric features. A vector r ∈ ℝ^{n} such that r ≠ 0 is a ray (or direction of infinity) of a non-empty polyhedron P ⊆ ℝ^{n} if, for every point p ∈ P and every non-negative scalar ρ ∈ ℝ_{+}, we have p + ρr ∈ P; the set of all the rays of a polyhedron P is denoted by rays(P). A vector l ∈ ℝ^{n} is a line of P if both l and −l are rays of P. The empty polyhedron has no rays and no lines. As was the case for equality constraints, the theory can dispense with the use of lines by using the corresponding pair of rays. Moreover, when vectors are used to denote rays, no distinction is made between different vectors having the same direction so that, e.g., r_{1} = (1, 3)^{T} and r_{2} = (2, 6)^{T} are considered to be the same ray in ℝ^{2}. The following theorem is a simple consequence of well-known theorems by Minkowski and Weyl [36].

Theorem 2.1. The set P ⊆ ℝ^{n} is a closed polyhedron if and only if there exist finite sets R, P ⊆ ℝ^{n} of cardinality r and p, respectively, such that 0 ∉ R and

P = gen((R, P)) := { Rρ + P σ ∈ ℝ^{n} | ρ ∈ ℝr_{+}, σ ∈ ℝp_{+}, ∑_{i=1}^{p} σ_{i} = 1 }.

When P ≠ ∅, we say that P is described by the generator system G = (R, P). In particular, the vectors of R and P are rays and points of P, respectively. Thus, each point of the generated polyhedron is obtained by adding a nonnegative combination of the rays in R and a convex combination of the points in P. Informally speaking, if no “supporting point” is provided then an empty polyhedron is obtained; formally, P = ∅ if and only if P = ∅. By convention, the empty system (i.e., the system with R = ∅ and P = ∅) is the only generator system for the empty polyhedron. We define a partial order relation ‘⊑’ on generator systems, which is the component-wise extension of set inclusion. Namely, for any generator systems G_{1} = (R_{1}, P_{1}) and G_{2} = (R_{2}, P_{2}), we have G_{1} ⊑ G_{2} if and only if R_{1} ⊆ R_{2} and P_{1} ⊆ P_{2}; if, in addition, G_{1} ≠ G_{2}, we write G_{1} ⊏ G_{2}. The function ‘gen’ enjoys a monotonicity property, as G_{1} ⊑ G_{2} implies gen(G_{1}) ⊆ gen(G_{2}).

The vector v ∈ P is an extreme point (or vertex) of the polyhedron P if it cannot be expressed as a convex combination of some other points of P. Similarly, r ∈ rays(P) is an extreme ray of P if it cannot be expressed as a non-negative combination of some other rays of P. It is worth stressing that, in general, the vectors in R and P are not the extreme rays and the vertices of the polyhedron: for instance, any half-space of ℝ^{2} has two extreme rays and no vertices, but any generator system describing it will contain at least three rays and one point.

The combination of the two approaches outlined above is the basis of the double description method due to Motzkin et al. [32], which exploits the duality principle to compute each representation starting from the other one, possibly minimizing both descriptions. Clever implementations of this conversion procedure, such as those based on the extension by Le Verge [29] of Chernikova’s algorithms [17, 18, 19], are the starting point for the development of software libraries based on the double description method. While being characterized by a worst-case computational cost that is exponential in the size of the input, these algorithms turn out to be practically useful for the purposes of many applications in the context of static analysis.

We denote by ℂℙ_{n} the set of all topologically closed polyhedra in ℝ^{n}, which is partially ordered by subset inclusion to form a non-complete lattice; the finitary greatest lower bound operator corresponds to intersection; the finitary least upper bound operator, denoted by ‘⊎’, corresponds to the convex polyhedral hull.

2.2. Not Necessarily Closed Convex Polyhedra

The linear strict inequality constraint β = (⟨a, x⟩ > b) defines a topologically open affine half-space of ℝ^{n}. A not necessarily closed (NNC) convex polyhedron is defined by a finite system of strict and non-strict inequality constraints. Since by using lines, rays and points we can only represent topologically closed polyhedra, the key step for a parametric description of NNC polyhedra is the introduction of a new kind of generator called a closure point [3].

Definition 2.2. (Closure point.) A vector c ∈ ℝ^{n} is a closure point of S ⊆ ℝ^{n} if and only if c ∈ ℂ(S).

For a non-empty NNC polyhedron P ⊆ ℝ^{n}, a vector c ∈ ℝ^{n} is a closure point of P if and only if σp + (1 − σ)c ∈ P for every point p ∈ P and every σ ∈ ℝ such that 0 < σ < 1. By excluding the case when σ = 0, c is not forced to be in P.

The following theorem taken from [3] is a generalisation of Theorem 2.1 to NNC polyhedra.

Theorem 2.3. The set P ⊆ ℝ^{n} is an NNC polyhedron if and only if there exist finite sets R, P, C ⊆ ℝ^{n} of cardinality r, p and c, respectively, such that 0 ∉ R and

P = gen((R, P, C)) := \{ Rρ + P σ + Cτ ∈ ℝ^{n} | \begin{matrix}ρ ∈ ℝr_{+}, σ ∈ ℝp_{+}, σ ≠ 0, \\ τ ∈ ℝc_{+}, \\ ∑_{i=1}^{p} σ_{i} + ∑_{i=1}^{c} τ_{i} = 1 \end{matrix} \}.

When P ≠ ∅, we say that P is described by the extended generator system G = (R, P, C). As was the case for closed polyhedra, the vectors in R and P are rays and points of P, respectively. The condition σ ≠ 0 ensures that at least one of the points of P plays an active role in any convex combination of the vectors of P and C. The vectors of C are closure points of P. Since both rays and closure points need a supporting point, we have P = ∅ if and only if P = ∅. The partial order relation ‘⊑’ on generator systems is easily extended to also take into account the closure points component, so that the overloading of the function ‘gen’ still satisfies the monotonicity property.

The set of all NNC polyhedra in ℝ^{n}, denoted ℙ_{n}, is again a non-complete lattice partially ordered by subset inclusion, having ℂℙ_{n} as a sublattice.

3. Exact Join Detection for Convex Polyhedra

In this section, we provide results for the exact join detection problem for convex polyhedra. Here we just consider the case when a double description representation is available; that is, in the proposed methods, we exploit both the constraint and the generator descriptions of the polyhedra.

3.1. Topologically Closed Polyhedra

First we consider the exact join detection problem for closed polyhedra since, in this case, given any two closed polyhedra P_{1}, P_{2} ∈ ℂℙ_{n}, we have that P_{1} ∪P_{2} is convex if and only if P_{1} ⊎ P_{2} = P_{1} ∪ P_{2}. Before stating and proving the main result for this section, we present the following lemma that establishes some simple conditions that will ensure the union of two closed polyhedra is not convex.

Lemma 3.1. Let P_{1}, P_{2} ∈ ℂℙ_{n} be topologically closed non-empty polyhedra. Suppose there exist a constraint β and a vector p such that (1) p saturates β,

(2) β is satisfied by P_{1} but violated by P_{2}, and (3) p ∈ P_{1} \ P_{2}. Then, P_{1} ∪ P_{2} is not convex.

Proof. By (2), there exists a point p_{2} ∈ P_{2} that violates β. Consider the closed line segment s := [p, p_{2}]; by (1), the one and only point on this segment that satisfies β is p; by (3), p ∈ P_{1} so that s ⊆ P_{1} ⊎ P_{2}. Also by (3), p ∉ P_{2}, so that there exists a non-strict constraint β_{2} that is satisfied by P_{2} but violated by p. Since p_{2} ∈ P_{2}, there exists a vector q ∈ s that saturates β_{2} and q ≠ p. It follows that the open line segment s_{1} := (p, q) is non-empty and every point in s_{1} violates both β and β_{2}; hence s_{1} ∩ P_{1} = s_{1} ∩ P_{2} = ∅. However, by construction,

(p, q) ⊂ [p, p_{2}] ⊆ P_{1} ⊎ P_{2},

so that P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}. Therefore P_{1} ∪ P_{2} is not convex. □

Theorem 3.2. Let P_{1}, P_{2} ∈ ℂℙ_{n} be topologically closed non-empty polyhedra, where P_{1} = con(C_{1}) = gen(G_{1}). Then P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2} if and only if there exist a constraint β_{1} ∈ C_{1} and a generator g_{1} in G_{1} such that (1) g_{1} saturates β_{1}, (2) P_{2} violates β_{1}, and (3) P_{2} does not subsume g_{1}.

Proof. Suppose first that P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}. Then P_{1} ∪ P_{2} is not convex and there exist points p_{1} ∈ P_{1} \P_{2} and p_{2} ∈ P_{2} \P_{1} such that [p_{1}, p_{2}] ⊈ P_{1} ∪P_{2}. As p_{2} ∉ P_{1}, there exists a constraint β_{1} ∈ C_{1} such that p_{2} violates β_{1}; also, there exists a point p′ ∈ [p_{1}, p_{2}] that saturates β_{1}; moreover p′ ∉ P_{2} since if this held, we would have [p_{1}, p′] ⊆ P_{1} and [p′, p_{2}] ⊆ P_{2}, contradicting [p_{1}, p_{2}] ⊈ P_{1} ∪ P_{2}. Let G′_{1} be the generator system containing all the points and rays in G_{1} that saturate β_{1}. Then p′ ∈ gen(G′_{1}). Hence, as p′ ∉ P_{2}, there is a point or ray g_{1} in G′_{1} that is not subsumed by P_{2}. Hence conditions (1), (2) and (3) are all satisfied.

Suppose now that there exist a constraint β_{1} ∈ C_{1} and a generator g_{1} in G_{1} such that conditions (1), (2) and (3) hold. Then, as P_{1} = gen(g_{1}), β_{1} is satisfied by P_{1}. If g_{1} := p_{1} is a point, then, by letting β := β_{1} and p := p_{1} in Lemma 3.1, the required three conditions hold so that P_{1} ∪ P_{2} is not convex. Now suppose that g_{1} := r_{1} is a ray for P_{1}. Suppose there exists a point p′_{1} ∈ P_{1} that saturates the constraint β_{1}. By condition (3), r_{1} is not a ray for P_{2}; hence for some ρ ∈ ℝ_{+} there exists a point p_{1} := p′_{1} + ρr_{1} ∈ P_{1} \ P_{2} that also saturates β_{1}. Hence, letting β := β_{1} and p := p_{1} in Lemma 3.1, the required three conditions hold so that P_{1} ∪ P_{2} is not convex. Otherwise, no point in P_{1} saturates β_{1}.^{3} Suppose, for some a ∈ ℝ^{n} and b ∈ ℝ, β = (⟨a, x⟩ ▷◁ b); then, since P_{1} ≠ ∅, there exist a point p′_{1} ∈ P_{1} and a constraint β′_{1} := (⟨a, x⟩ ▷◁ b′) such that P_{1} satisfies β′_{1} and p′_{1} saturates β′_{1}; note that β′_{1} is also saturated by ray r_{1}. Thus we can construct, as done above, a point p_{1} := p′_{1} + ρr_{1} ∈ P_{1} \ P_{2} that saturates β′_{1}. Hence, letting β := β_{1} and p := p_{1} in Lemma 3.1, the required three conditions hold so that P_{1} ∪ P_{2} is not convex. Therefore, in all cases, P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}. □

3This may happen because we made no minimality assumption on the constraint system C_{1}, so that β_{1} may be redundant.

(a) P, Q ∈ ℙ_{2}^{O  x_{1} x_{2}  A  B C D  E P  Q}  (b) P, Q′ ∈ ℙ_{2}^{O  x_{1} x_{2}  A  B C D  P  Q′}  (c) P ⊎ Q = P ⊎ Q′^{O  x_{1} x_{2}  A  B C D}

Figure 1: The convex polyhedral hull of NNC polyhedra

Example 3.3. Consider the closed polyhedra

P_{1} = con(C_{1}) = con({x_{1} ≥ 0, x_{2} ≥ 0, x_{1} + x_{2} ≤ 2})
= gen(G_{1}) = gen((∅, P)),
P_{2} = con(C_{2}) = con({x_{1} ≤ 2, x_{2} ≥ 0, x_{1} − x_{2} ≥ 0}),

where P = {(0, 0)^{T}, (2, 0)^{T}, (0, 2)^{T}}. Then

P_{1} ⊎ P_{2} = con({x_{1} ≥ 0, x_{2} ≥ 0, x_{1} ≤ 2, x_{2} ≤ 2})

so that (1, 1)^{T} ∈ (P_{1} ⊎ P_{2}) \ (P_{1} ∪ P_{2}) and, hence, P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}. In Theorem 3.2, let β_{1} = (x_{1} + x_{2} ≤ 2) and g_{1} = (0, 2)^{T}. Then conditions (1), (2) and (3) are all satisfied.

For each i ∈ {1, 2}, let l_{i} and m_{i} denote the number of constraints in C_{i} and generators in G_{i}, respectively. Then, the worst-case complexity of an algorithm based on Theorem 3.2, computed by summing the complexities for checking each of the conditions (1), (2) and (3), is in O(n(l_{1}m_{1} + l_{1}m_{2} + l_{2}m_{1})). Notice that the complexity bound is not symmetric so that, if l_{1}m_{1} ≫ l_{2}m_{2} holds, then an efficiency improvement can be obtained by exchanging the roles of P_{1} and P_{2} in the theorem. In all cases, an improvement is obtained with respect to the O(n(l_{1} + l_{2})m_{1}m_{2})) complexity bound of Algorithm 7.1 in [13].

3.2. Not Necessarily Closed Polyhedra

We now consider the exact join detection problem for two NNC polyhedra P_{1}, P_{2} ∈ ℙ_{n}; in this case, it can happen that P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2} although the union P_{1} ∪ P_{2} is convex.

Example 3.4. Consider the NNC polyhedra P and Q in Figure 1(a), where P is the open rectangle ABCD and Q is the single point E. The union P ∪ Q is convex but it is not an NNC polyhedron: the convex polyhedral hull P ⊎ Q (see Figure 1(c)) also contains the line segment (B, C) and hence P ⊎Q ≠ P ∪Q. On the other hand, if we now consider P and Q′, as shown in Figure 1(b), where Q′ is the line segment (B, C), then the convex polyhedral hull P ⊎ Q′ is such that P ⊎ Q′ = P ⊎ Q = P ∪ Q′.

Before stating and proving the main result for this section, we present a lemma similar to Lemma 3.1 but generalized so as to apply to NNC polyhedra.

Lemma 3.5. Let P_{1}, P_{2} ∈ ℙ_{n} be non-empty polyhedra. Suppose that there exist a constraint β and a vector p such that (1) p saturates β, (2) β is satisfied by P_{1} but violated by P_{2}, and (3) p ∈ ℂ(P_{1}) \ ℂ(P_{2}). Then P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}.

Proof. By (2), there exists a point p_{2} ∈ P_{2} that violates β. Consider the line segment s := (p, p_{2}]; by (1), no point on s satisfies β; by (3), p ∈ ℂ(P_{1}) so that s ⊆ P_{1} ⊎ P_{2}. Also, by (3), p ∉ ℂ(P_{2}), so that, there exists a constraint β_{2} that is satisfied by ℂ(P_{2}) but violated by p. Since p ∉ P_{2} and p_{2} ∈ P_{2}, there exists a vector q ∈ s that saturates β_{2} and q ≠ p. It follows that the open line segment s_{1} := (p, q) is non-empty and every point in s_{1} violates both β and β_{2}; hence s_{1} ∩ P_{1} = s_{1} ∩ P_{2} = ∅. However, by construction,

(p, q) ⊂ (p, p_{2}] ⊆ (P_{1} ⊎ P_{2}),

so that P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}. □

Theorem 3.6. For i ∈ {1, 2}, let P_{i} = con(C_{i}) = gen(G_{i}) ∈ ℙ_{n} be non-empty polyhedra. Then P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2} if and only if, for some i, j ∈ {1, 2}, i ≠ j, there exists a generator g_{i} in G_{i} that saturates a constraint β_{i} ∈ C_{i} violated by P_{j} and at least one of the following hold:

(1) g_{i} is a ray or closure point in G_{i} that is not subsumed by P_{j};

(2) g_{i} is a point in G_{i}, β_{i} is non-strict and g_{i} ∉ ℂ(P_{j});

(3) g_{i} is a closure point in G_{i}, β_{i} is strict and g_{i} ∈ (P_{1} ⊎ P_{2}) \ P_{j}.

Proof. Suppose first that P_{1}⊎P_{2} ≠ P_{1}∪P_{2}. Then, for some i, j ∈ {1, 2}, i ≠ j, there exist points p_{i} ∈ ℂ(P_{i}) \ P_{j} and p_{j} ∈ P_{j} \ P_{i} such that (p_{i}, p_{j}] ⊈ P_{1} ∪ P_{2}. By construction, (p_{i}, p_{j}] ⊆ P_{1} ⊎ P_{2}. For ease of notation, we will assume that i = 1 and j = 2; the other case follows by a symmetrical argument. As p_{2} ∉ P_{1}, there exists a constraint β_{1} ∈ C_{1} and a point p ∈ [p_{1}, p_{2}] such that p_{2} violates β_{1}, p saturates β_{1} and p ∈ ℂ(P_{1}); moreover, if p ∉ P_{1}, then we can and will assume that β_{1} is a strict constraint. Note that p ∉ P_{2} since, if this held, we would have (p_{1}, p) ⊆ P_{1} and [p, p_{2}] ⊆ P_{2}, contradicting (p_{1}, p_{2}] ⊈ P_{1} ∪ P_{2}. Moreover, if p ∈ P_{1}, p ∉ ℂ(P_{2}) since, if this held, we would have (p_{1}, p) ⊆ P_{1} and [p, p_{2}] ⊆ P_{2}, again contradicting (p_{1}, p_{2}] ⊈ P_{1} ∪ P_{2}. Let G′_{1} = (R′_{1}, P′_{1}, C′_{1}) be the system of all the generators in G_{1} that saturate β_{1} so that p ∈ gen((R′_{1}, P′_{1} ∪ C′_{1}, ∅)). Suppose condition (1) does not hold; that is, suppose that all the rays in R′_{1} are subsumed by P_{2} and C′_{1} ⊆ ℂ(P_{2}). If β_{1} is non-strict, p ∈ P_{1} so that p ∉ ℂ(P_{2}); hence P′_{1} ⊈ ℂ(P_{2}) and condition (2) holds. Suppose now that β_{1} is strict; then P′_{1} = ∅, C′_{1} ≠ ∅ and C′_{1} ∩ P_{1} = ∅. Hence, as p ∉ P_{2}, there exists C′′_{1} ⊆ C′_{1} such that p ∈ gen((R′_{1}, C′′_{1}, ∅)) and C′′_{1} ∩ P_{2} = ∅. As p ∈ P_{1} ⊎ P_{2}, there exists g_{1} ∈ C′′_{1} such that g_{1} ∈ P_{1} ⊎ P_{2}; hence condition (3) holds.

Suppose now that, for some i, j ∈ {1, 2} i ≠ j, there exists a generator g_{i} in G_{i} that saturates a constraint β_{i} ∈ C_{i} that is violated by P_{j} and at least one of conditions (1), (2) or (3) holds. As before, we will assume that i = 1 and j = 2, since the other case follows by a symmetrical argument. Let β_{1} := (⟨a, x⟩ ▷◁ b), where ▷◁ ∈ {<, ≤}. If condition (1) holds, then g_{1} is a closure point or ray that is not subsumed by P_{2}. Thus, if g_{1} is a closure point in G_{1}, g_{1} ∉ ℂ(P_{2}); so that, by letting β := β_{1} and p := g_{1} in Lemma 3.5, P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}. Suppose now that g_{1} := r_{1} is a ray. Since P_{1} ≠ ∅, there exist a point p′_{1} ∈ ℂ(P_{1}) and a constraint β′_{1} := (⟨a, x⟩ ≤ ⟨a, p′_{1}⟩) such that P_{1} satisfies β′_{1}; note that, by definition, β′_{1} is saturated by the point p′_{1} and the ray r_{1}.^{4} Thus there exists ρ ∈ ℝ_{+} such that the point p_{1} := p′_{1} + ρr_{1} ∈ ℂ(P_{1}) does not belong to ℂ(P_{2}); hence, as p_{1} saturates β′_{1}, by letting β := β′_{1} and p := p_{1} in Lemma 3.5, P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}. If condition (2) holds, then g_{1} is a point in G_{1} (so that g_{1} ∈ P_{1}) and g_{1} ∉ ℂ(P_{2}). Then, by letting β := β_{1} and p := g_{1} in Lemma 3.5, P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}. Finally, if condition (3) holds, then g_{1} is a closure point in G_{1} and β_{1} is a strict constraint, so that g_{1} ∉ P_{1}; as condition (3) also states that g_{1} ∈ (P_{1} ⊎ P_{2}) \ P_{2}, it follows that P_{1} ⊎ P_{2} ≠ P_{1} ∪ P_{2}. □

Observe that the conditions stated for the NNC case in Theorem 3.6 are more involved than the conditions stated for the topologically closed case in Theorem 3.2. In particular, a direct correspondence can only be found for condition (2) of Theorem 3.6. The added complexity is justified by the need to properly capture special cases where, as said above, convexity alone is not sufficient. Hence, we provide examples showing cases when conditions (1) and (3) of Theorem 3.6 come into play.

Example 3.7 (Condition (1) of Theorem 3.6). We first show how condition (1) of Theorem 3.6 where g_{1} is a closure point can properly discriminate between the two cases illustrated in Figures 1(a) and 1(b).

Consider the polyhedra P and Q in Figure 1(a) and assume that the line segment (B, C) satisfies the constraint x_{1} = 4. In the statement of Theorem 3.6, let P_{1} = P, P_{2} = Q, i = 1, j = 2, β_{1} = (x_{1} < 4) ∈ C_{1} and g_{1} = B be a closure point in G_{1}. Then β_{1} is violated by P_{2} and saturated by g_{1}, but g_{1} is not subsumed by P_{2}. Hence condition (1) of Theorem 3.6 holds and we correctly conclude that P ⊎ Q ≠ P ∪ Q.

On the other hand, if we consider polyhedra P and Q′ in Figure 1(b) and let P_{1} = P and P_{2} = Q′, then the closure point g_{1} = B is subsumed by P_{2} so that condition (1) of Theorem 3.6 does not hold.

Note that such a discrimination could not be obtained by checking only condition (2) of Theorem 3.6. If we swap the indices i and j so that i = 2, j = 1; letting β_{2} = (x_{1} ≥ 4) ∈ C_{2} and g_{2} = E be a point in G_{2}, then g_{2} ∈ ℂ(P) and β_{2} is a non-strict constraint of both Q and Q′ violated by P and saturated by point g_{2}; hence condition (2) does not hold for both P_{2} = Q and for P_{2} = Q′.

4Note that ⟨a, p′_{1}⟩ may differ from b because we made no minimality assumption on the constraint system C_{1}, so that β_{1} may be redundant.

(a) Q_{1}, Q_{2} ∈ ℙ_{2}^{O  x_{1} x_{2}  A Q_{1}  Q_{2}}  (b) Q_{3}, Q_{4} ∈ ℙ_{2}^{O  x_{1} x_{2} A  B C D  E F Q_{3}  Q_{4}}  (c) Q_{5}, Q_{6} ∈ ℙ_{2}^{O  x_{1} x_{2} A  B E C D  F G Q_{5} Q_{6}}

(d) Q_{1} ⊎ Q_{2}^{O  x_{1} x_{2}  A B Q_{1} ⊎ Q_{2}}  (e) Q_{3} ⊎ Q_{4}^{O  x_{1} x_{2} A D  E F B Q_{3} ⊎ Q_{4}}  (f) Q_{5} ⊎ Q_{6}^{O  x_{1} x_{2} A  C D  F G Q_{5} ⊎ Q_{6}}

Figure 2: More examples for the convex polyhedral hull of NNC polyhedra

For an example of application of condition (1) of Theorem 3.6 when g_{1} is a ray, consider Q_{1} and Q_{2} in Figure 2(a), where Q_{1} = con({2 ≤ x_{1} < 4}) is an unbounded strip and Q_{2} = {A} is a singleton, with A = (4, 2)^{T}. It can be seen that Q_{1} ⊎ Q_{2}, the polyhedron in Figure 2(d), contains the point B = (4, 0)^{T} which is not a point in Q_{1} or Q_{2}, so that Q_{1} ⊎ Q_{2} ≠ Q_{1} ∪ Q_{2}. In the statement of Theorem 3.6, let P_{1} = Q_{1}, P_{2} = Q_{2}, i = 1, j = 2, β_{1} = (x_{1} < 4) ∈ C_{1} and g_{1} = (0, 1)^{T} be a ray in G_{1}. Then β_{1} is violated by P_{2} and saturated by the ray g_{1}; but g_{1} is not subsumed by P_{2} so that condition (1) of Theorem 3.6 holds.

Example 3.8 (Condition (3) of Theorem 3.6). This example shows how condition (3) of Theorem 3.6 can properly discriminate between the two cases illustrated in Figures 2(b) and 2(c).

Consider the polyhedra Q_{3} and Q_{4} in Figure 2(b), where Q_{3} is the rectangle ABCD with the open bound (B, C) defined by the strict constraint x_{1} < 3, whereas Q_{4} is the rectangle BEF C with the open bound (B, C) defined by the strict constraint x_{1} > 3. Thus B = (3, 1)^{T} and C = (3, 5)^{T} are closure points for both Q_{3} and Q_{4}. It can be seen that Q_{3} ⊎ Q_{4}, the polyhedron in Figure 2(e), contains the whole line segment [B, C] so that Q_{3} ⊎ Q_{4} ≠ Q_{3} ∪ Q_{4}. In the statement of Theorem 3.6, let P_{1} = Q_{3}, P_{2} = Q_{4}, i = 1, j = 2, β_{1} = (x_{1} < 3) ∈ C_{1} and g_{1} = B be a closure point in G_{1}. Then β_{1} is violated by P_{2} and saturated by the closure point g_{1}. Although condition (1) does not hold because g_{1} is subsumed by P_{2}, condition (3) does hold since β_{1} is strict and g_{1} ∈ (P_{1} ⊎ P_{2}) \ P_{2}.

Consider the polyhedra Q_{5} and Q_{6} in Figure 2(c), where Q_{5} is the quadrilateral ABCD and Q_{6} is the quadrilateral EF GC. Then the convex polyhedral hull Q_{5} ⊎ Q_{6} shown in Figure 2(f) is equal to their union Q_{5} ∪ Q_{6}. In the statement of Theorem 3.6, let P_{1} = Q_{5}, P_{2} = Q_{6}, i = 1, j = 2, β_{1} ∈ C_{1} be the strict constraint defining the dashed line boundary (B, C) and g_{1} be the closure point C in both P_{1} and P_{2}. Then none of the conditions in Theorem 3.6 hold.

4. Exact Join Detection for Boxes and Other Cartesian Products

A rational interval constraint for a dimension i ∈ {1, …, n} has the form x_{i} ▷◁ b, where ▷◁ ∈ {<, ≤, =, ≥, >} and b ∈ ℚ. A finite system of rational interval constraints defines an NNC polyhedron in ℙ_{n} that we call a rational box; the set of all rational boxes in the n-dimensional vector space is denoted 𝔹_{n} and is a meet-sublattice of ℙ_{n}. The domain 𝔹_{n} so defined can be seen as the Cartesian product of n possibly infinite intervals with rational, possibly open boundaries. If we denote by 𝕀 the set of such intervals and by ‘⊕’ the binary join operator over the bounded join-semilattice (𝕀, ⊆), we have, for each B_{1}, B_{2} ∈ 𝔹,

B_{1} ⊎ B_{2} = (π_{1}(B_{1}) ⊕ π_{1}(B_{2})) × ⋯ × (π_{n}(B_{1}) ⊕ π_{n}(B_{2})).

The following theorem defines a necessary and sufficient condition that is only based on ‘⊕’ and on the subset ordering over 𝕀. Notice, in particular, that convexity does not play any role, neither in the statement, nor in the proof.

Theorem 4.1. Let B_{1}, B_{2} ∈ 𝔹_{n}. Then B_{1} ⊎ B_{2} ≠ B_{1} ∪ B_{2} if and only if

1. ∃i ∈ {1, …, n} . π_{i}(B_{1}) ⊕ π_{i}(B_{2}) ≠ π_{i}(B_{1}) ∪ π_{i}(B_{2}); or

2. ∃i, j ∈ {1, …, n} . i ≠ j ∧ π_{i}(B_{1}) ⊈ π_{i}(B_{2}) ∧ π_{j}(B_{2}) ⊈ π_{j}(B_{1}).

Proof. Suppose that B_{1} = ∅ so that, for each i ∈ {1, …, n}, π_{i}(B_{1}) = ∅. Then, neither condition (1) nor condition (2) can hold, so that the lemma holds. By a symmetric reasoning, the lemma holds if B_{2} = ∅. Hence, in the following we assume that both B_{1} and B_{2} are non-empty boxes.

Suppose first that B_{1} ⊎ B_{2} ≠ B_{1} ∪ B_{2}; then there exists a point p ∈ B_{1} ⊎ B_{2} such that p ∉ B_{1} and p ∉ B_{2}. Hence, for some i, j ∈ {1, …, n}, we have that p_{i} ∉ π_{i}(B_{1}) and p_{j} ∉ π_{j}(B_{2}). Note that as p ∈ B_{1} ⊎ B_{2}, we also have p_{i} ∈ π_{i}(B_{1}) ⊕ π_{i}(B_{2}) and p_{j} ∈ π_{j}(B_{1}) ⊕ π_{j}(B_{2}). Suppose that condition (1) does not hold. Then p_{i} ∈ π_{i}(B_{2}) and p_{j} ∈ π_{j}(B_{1}); hence we must have i ≠ j and p_{i} ∈ π_{i}(B_{1}) \ π_{i}(B_{2}) and p_{j} ∈ π_{j}(B_{2}) \ π_{j}(B_{1}); implying that π_{i}(B_{1}) ⊈ π_{i}(B_{2}) and π_{j}(B_{2}) ⊈ π_{j}(B_{1}), so that condition (2) holds.

Assuming that condition (1) or (2) holds, we now prove B_{1} ⊎ B_{2} ≠ B_{1} ∪ B_{2}. First, suppose that condition (1) holds. Then there exists v ∈ π_{i}(B_{1} ⊎ B_{2}) such that v ∉ π_{i}(B_{1}) and v ∉ π_{i}(B_{2}). By definition of π_{i}, there exist a point p ∈ B_{1} ⊎ B_{2} such that π_{i}(p) = v, so that p ∉ B_{1} and p ∉ B_{2}; therefore B_{1} ⊎ B_{2} ≠ B_{1} ∪ B_{2}. Secondly, suppose that condition (2) holds. Then there exist values v_{i} ∈ π_{i}(B_{1}) \ π_{i}(B_{2}) and v_{j} ∈ π_{j}(B_{2}) \ π_{j}(B_{1}); hence, there exist points p_{i} ∈ B_{1} and p_{j} ∈ B_{2} such that π_{i}(p_{i}) = v_{i} and π_{j}(p_{j}) = v_{j}. Let p be such that π_{k}(p) = π_{k}(p_{i}), for all k ∈ {1, …, n} \ {j}, and π_{j}(p) = v_{j}; then p ∉ B_{1} ∪ B_{2}. By definition of the ‘⊎’ operator, p ∈ B_{1} ⊎ B_{2}, so that B_{1} ⊎ B_{2} ≠ B_{1} ∪ B_{2}. □

Example 4.2. Consider the topologically closed boxes

B_{1} = con({0 ≤ x_{1} ≤ 1, 0 ≤ x_{2} ≤ 2}),
B_{2} = con({3 ≤ x_{1} ≤ 4, 0 ≤ x_{2} ≤ 2}),
B_{3} = con({0 ≤ x_{1} ≤ 4, 1 ≤ x_{2} ≤ 2}).

Then we obtain

B_{1} ⊎ B_{2} = B_{1} ⊎ B_{3} = con({0 ≤ x_{1} ≤ 4, 0 ≤ x_{2} ≤ 2}).

Letting p = (2, 0)^{T}, we have p ∈ B_{1} ⊎ B_{2} although p ∉ B_{1} ∪ B_{2} ∪ B_{3}; hence B_{1} ⊎ B_{2} ≠ B_{1} ∪ B_{2} and B_{1} ⊎ B_{3} ≠ B_{1} ∪ B_{3}, i.e., both join computations are inexact. Observe that

π_{1}(B_{1}) ⊕ π_{1}(B_{2}) ≠ π_{1}(B_{1}) ∪ π_{1}(B_{2}),

so that, for boxes B_{1} and B_{2}, condition (1) holds; on the other hand we have

π_{1}(B_{3}) ⊈ π_{1}(B_{1}) and π_{2}(B_{1}) ⊈ π_{2}(B_{3}),

so that, for boxes B_{1} and B_{3}, condition (2) holds.

This result has been introduced for rational boxes for simplicity only. Indeed, it trivially generalizes to any Cartesian product of 1-dimensional numerical abstractions, including: the well-known abstract domain of multi-dimensional, integer-valued intervals [20]; 1-dimensional congruence equations like x = 0 (mod 2); modulo intervals [33, 34]; and circular linear progressions [35]. For full generality, for each i ∈ {1, …, n}, let (𝔸(i), ⊆), with ∅ ∈ 𝔸(i) ⊆ ℘(ℝ), be a bounded join-semilattice where the binary join operator is denoted by ‘⊕_{i}’. (𝔸(i), ⊆) is thus an abstract domain suitable for approximating ℘(ℝ). Then, the trivial combination of the n domains 𝔸(i) by means of Cartesian product, 𝔸_{n} := 𝔸(1) × ⋯ × 𝔸(n), is an abstract domain suitable for approximating ℘(ℝ^{n}).^{5} Theorem 4.1 immediately generalizes to any domain 𝔸_{n} so obtained.

An algorithm for the exact join detection on 𝔸_{n} based on Theorem 4.1 will compute, in the worst case, a linear number of 1-dimensional joins (applying the ‘⊕_{i}’ operators) and a quadratic number of 1-dimensional inclusion tests. Since these 1-dimensional operations take constant time, the worst-case complexity bound for n-dimensional boxes is O(n^{2}).

5. Exact Join Detection for Bounded Difference Shapes

A (rational) bounded difference is a non-strict inequality constraint having one of the forms ±x_{i} ≤ b or x_{i} −x_{j} ≤ b, where i, j ∈ {1, …, n}, i ≠ j and b ∈ ℚ.

5This construction is called a direct product in the field of abstract interpretation. The resulting domain is said to be attribute-independent, in the sense that relational information is not captured. In other words, the constraints on space dimension i are unrelated to those on space dimension j whenever i ≠ j.

A finite system of bounded differences defines a bounded difference shape (BD shape); the set of all BD shapes in the n-dimensional vector space is denoted 𝔹𝔻_{n} and it is a meet-sublattice of ℂℙ_{n}. In this section we specialize the result on topologically closed polyhedra to the case of BD shapes, which can be efficiently represented and manipulated as weighted graphs. To start with, we introduce some notation and terminology (see also [2, 9, 30, 31]).

Let ℚ_{∞} := ℚ ∪ {+∞} be totally ordered by the extension of ‘<’ such that d < +∞ for each d ∈ ℚ. Let N be a finite set of nodes. A weighted directed graph (graph, for short) G in N is a pair (N , w), where w: N × N → ℚ_{∞} is the weight function for G. A pair (n_{i}, n_{j}) ∈ N ×N is an arc of G if w(n_{i}, n_{j}) < +∞; the arc is proper if n_{i} ≠ n_{j}. A path θ = n_{0} ⋯ n_{p} in a graph G = (N , w) is a nonempty and finite sequence of nodes such that, for all i ∈ {1, …, p}, (n_{i−1}, n_{i}) is an arc of G; each arc (n_{i−1}, n_{i}) is said to be in the path θ. If θ_{1} = n_{0} ⋯ n_{h} and θ_{2} = n_{h} ⋯ n_{p} are paths in G, where 0 ≤ h ≤ p, then the path concatenation θ = n_{0} ⋯ n_{h} ⋯ n_{p} of θ_{1} and θ_{2} is denoted by θ_{1} :: θ_{2}; if θ_{1} = n_{0}n_{1} (so that h = 1), then θ_{1} :: θ_{2} will also be denoted by n_{0}·θ_{2}. Note that path concatenation is not the same as sequence concatenation. The path θ is simple if each node occurs at most once in θ; it is proper if all the arcs in it are proper; it is a proper cycle if it is a proper path and n_{0} = n_{p} (so that p ≥ 2). The path θ has weight w(θ) := ∑_{i=1}^{p} w(n_{i−1}, n_{i}). A graph is consistent if it has no negative weight cycles. The set 𝔾 of consistent graphs in N is partially ordered by the relation ‘⊴’ defined, for all G_{1} = (N , w_{1}) and G_{2} = (N , w_{2}), by

G_{1} ⊴ G_{2} ⟺ ∀i, j ∈ N : w_{1}(i, j) ≤ w_{2}(i, j).

When augmented with a bottom element ⊥ representing inconsistency, this partially ordered set becomes a (non-complete) lattice 𝔾_{⊥} = ⟨𝔾∪{⊥}, ⊴, ⊓, ⊔⟩, where ‘⊓’ and ‘⊔’ denote the (finitary) greatest lower bound and least upper bound operators, respectively.

Definition 5.1. (Graph closure/reduction.) A consistent graph G = (N , w) is (shortest-path) closed if the following properties hold:

∀i ∈ N : w(i, i) = 0;  (3)
∀i, j, k ∈ N : w(i, j) ≤ w(i, k) + w(k, j).  (4)

The closure of a consistent graph G in N is

closure(G) := ⨆{ G^{c} ∈ 𝔾 | G^{c} ⊴ G and G^{c} is closed }.

A consistent graph R in N is (shortest-path) reduced if, for each graph G ≠ R such that R ⊴ G, closure(R) ≠ closure(G). A reduction for the consistent graph G is any reduced graph R such that closure(R) = closure(G).

Note that a reduction R for a closed graph G is a subgraph of G, meaning that all the arcs in R are also arcs in G and have the same finite weight.

Any non-empty element bd ∈ 𝔹𝔻_{n} can be represented by a consistent graph G = (N , w), where N = {0, …, n} is the set of graph nodes; each node i > 0 corresponds to the space dimension x_{i} of the vector space, while 0 (the special node) represents a further space dimension whose value is fixed to zero. Graph closure provides a normal form for non-empty BD shapes. Informally, a closed (resp., reduced) graph encodes a system of bounded difference constraints which is closed by entailment (resp., contains no redundant constraint).

If the non-empty BD shapes bd_{1}, bd_{2} ∈ 𝔹𝔻_{n} are represented by closed graphs G_{1} = (N , w_{1}) and G_{2} = (N , w_{2}), respectively, then the BD shape join bd_{1} ⊎bd_{2} is represented by the graph least upper bound G_{1}⊔G_{2} = (N , w), where w(i, j) := max(w_{1}(i, j), w_{2}(i, j))) for each i, j ∈ N; G_{1} ⊔ G_{2} is also closed. Observe too that the set intersection bd_{1} ∩ bd_{2} is represented by the graph greatest lower bound G_{1} ⊓ G_{2}.

Theorem 5.2. For each h ∈ {1, 2}, let bd_{h} ∈ 𝔹𝔻_{n} be a non-empty BD shape represented by the closed graph G_{h} = (N , w_{h}) and let R_{h} be a subgraph of G_{h} such that closure(R_{h}) = G_{h}. Let also G_{1} ⊔ G_{2} = (N , w). Then bd_{1} ⊎ bd_{2} ≠ bd_{1} ∪ bd_{2} if and only if there exist arcs (i, j) of R_{1} and (k, ℓ) of R_{2} such that

(1) w_{1}(i, j) < w_{2}(i, j) and w_{2}(k, ℓ) < w_{1}(k, ℓ); and

(2) w_{1}(i, j) + w_{2}(k, ℓ) < w(i, ℓ) + w(k, j).

Proof. Suppose that bd_{1} ⊎bd_{2} ≠ bd_{1} ∪bd_{2}, so that there exists p ∈ bd_{1} ⊎bd_{2} such that p ∉ bd_{1} and p ∉ bd_{2}. Hence, there exist i, j, k, ℓ ∈ N such that (i, j) is an arc of R_{1} satisfying^{6} π_{i}(p) − π_{j}(p) > w_{1}(i, j) and (k, ℓ) is an arc of R_{2} satisfying π_{k}(p)−π_{ℓ}(p) > w_{2}(k, ℓ). However, as p ∈ bd_{1} ⊎bd_{2}, π_{i}(p)−π_{j}(p) ≤ w(i, j) and π_{k}(p) − π_{ℓ}(p) ≤ w(k, ℓ) so that, by definition of G_{1} ⊔ G_{2}, we have w_{1}(i, j) < w_{2}(i, j) and w_{2}(k, ℓ) < w_{1}(k, ℓ); hence condition (1) holds. Since p ∈ bd_{1} ⊎ bd_{2},

w(i, ℓ) + w(k, j) ≥ π_{i}(p) − π_{ℓ}(p) + π_{k}(p) − π_{j}(p)
= π_{i}(p) − π_{j}(p) + π_{k}(p) − π_{ℓ}(p)
> w_{1}(i, j) + w_{2}(k, ℓ).

Therefore, condition (2) also holds.

We now suppose that there exist arcs (i, j) of R_{1} and (k, ℓ) of R_{2} such that conditions (1) and (2) hold. As G_{1} and G_{2} are closed, w_{1}(i, i) = w_{2}(i, i) = 0 and w_{1}(k, k) = w_{2}(k, k) = 0 so that condition (1) implies i ≠ j and k ≠ ℓ. As G_{1} ⊔ G_{2} is closed, w(i, i) = w(k, k) = 0 so that, if i = ℓ and j = k both hold, condition (2) implies w_{1}(i, j) + w_{2}(j, i) < 0; hence, by condition (1) the graph greatest lower bound G_{1} ⊓ G_{2} contains the negative weight proper cycle i · j · i and thus is inconsistent; hence bd_{1} ∩bd_{2} = ∅; and hence bd_{1} ⊎bd_{2} ≠ bd_{1} ∪bd_{2}. Therefore, in the following we assume that i ≠ ℓ or j ≠ k hold. If the right hand side of the inequalities in conditions (1) and (2) are all unbounded, let ϵ := 1; otherwise let

6We extend notation by letting π_{0}(v) := 0, for each vector v = (v_{1}, …, v_{n})^{T}.

ϵ := min \{ \begin{matrix}w(i, j) − w_{1}(i, j), \\ w(k, ℓ) − w_{2}(k, ℓ), \\ \frac{1}{2}(w(i, ℓ) + w(k, j) − w_{1}(i, j) − w_{2}(k, ℓ)) \end{matrix}\} .

Then, by conditions (1) and (2), ϵ > 0. Consider the graph G′ = (N , w′) where, for each r, s ∈ N,

w′(r, s) := \begin{cases}−w_{1}(i, j) − ϵ, & if (r, s) = (j, i); \\ −w_{2}(k, ℓ) − ϵ, & if (r, s) = (ℓ, k); \\ w(r, s), & otherwise. \end{cases}

We show that G′ is a consistent graph; to this end, since G := G_{1} ⊔G_{2} is known to be consistent, it is sufficient to consider the proper cycles of G′ that contain arcs (j, i) or (ℓ, k). Let θ_{ij} = i ⋯ j and θ_{kℓ} = k ⋯ ℓ be arbitrary simple paths from i to j and from k to ℓ, respectively. Then G′ is consistent if and only if w′(θ_{ij} · i) ≥ 0 and w′(θ_{kℓ} · k) ≥ 0. We only prove w′(θ_{ij} · i) ≥ 0 since the proof that w′(θ_{kℓ} · k) ≥ 0 follows by a symmetrical argument. As θ_{ij} is simple, it does not contain the arc (j, i). Suppose first that θ_{ij} does not contain the arc (ℓ, k). Then

w′(θ_{ij} · i) = w′(θ_{ij}) + w′(j, i)
= w(θ_{ij}) − w_{1}(i, j) − ϵ  [def. of w′]
≥ w(i, j) − w_{1}(i, j) − ϵ  [G closed]
≥ 0  [def. of ϵ].

Suppose now that θ_{ij} = θ_{iℓ} :: (ℓ, k) :: θ_{kj}, where θ_{iℓ} = i ⋯ ℓ and θ_{kj} = k ⋯ j do not contain the arcs (j, i) and (k, ℓ). Then

w′(θ_{ij} · i) = w′(θ_{iℓ}) + w′(ℓ, k) + w′(θ_{kj}) + w′(j, i)
= w(θ_{iℓ}) − w_{2}(k, ℓ) − ϵ + w(θ_{kj}) − w_{1}(i, j) − ϵ [def. of w′]
≥ w(i, ℓ) − w_{2}(k, ℓ) − ϵ + w(k, j) − w_{1}(i, j) − ϵ  [G closed]
= (w(i, ℓ) + w(k, j) − w_{1}(i, j) − w_{2}(k, ℓ)) − 2ϵ
≥ 0  [def. of ϵ].

Therefore G′ is consistent. Moreover, G′ ⊴ G since

w′(j, i) = −w_{1}(i, j) − ϵ  [def. of w′]
≤ −w_{1}(i, j)  [ϵ ≥ 0]
≤ w_{1}(j, i)  [G_{1} consistent]
≤ w(j, i)  [def. G];

similarly, w′(ℓ, k) ≤ w(ℓ, k); hence, for all r, s ∈ N, w′(r, s) ≤ w(r, s).

Let bd′ ∈ 𝔹𝔻_{n} be represented by G′, so that ∅ ≠ bd′ ⊆ bd_{1} ⊎ bd_{2}. Since w′(j, i) + w_{1}(i, j) < 0, we obtain bd′ ∩ bd_{1} = ∅; since w′(ℓ, k) + w_{2}(k, ℓ) < 0, we obtain bd′ ∩ bd_{2} = ∅. Hence, bd_{1} ⊎ bd_{2} ≠ bd_{1} ∪ bd_{2}. □

An algorithm for the exact join detection on 𝔹𝔻_{n} based on Theorem 5.2 will have a worst-case complexity bound in O(n^{4}). Noting that the computation of graph closure and reduction are both in O(n^{3}) [2, 9, 28, 31], a more detailed complexity bound is O(n^{3}+r_{1}r_{2}), where r_{h} is the number of arcs in the subgraph R_{h}; hence, a good choice is to take each R_{h} to be a graph reduction for G_{h}, as it will have a minimal number of arcs.

5.1. Integer BD Shapes

We now consider the case of integer BD shapes, i.e., subsets of ℤ^{n} that are delimited by BD constraints where the bounds are all integral. As for the rational case, these numerical abstractions can be encoded using weighted graphs, but restricting the codomain of the weight function to ℤ_{∞} := ℤ∪{+∞}. Since the set of integer graphs is a sub-lattice of the set of rational graphs, the conditions in Theorem 5.2 can be easily strengthened so as to obtain the corresponding result for integer BD shapes. The algorithm for the integer case shares the same complexity bound of the rational case.

Theorem 5.3. For each h ∈ {1, 2}, let bd_{h} ∈ 𝔹𝔻_{n} be a non-empty integer BD shape represented by the closed integer graph G_{h} = (N , w_{h}) and let R_{h} be a subgraph of G_{h} such that closure(R_{h}) = G_{h}. Let also G_{1} ⊔ G_{2} = (N , w). Then bd_{1} ⊎ bd_{2} ≠ bd_{1} ∪ bd_{2} if and only if there exist arcs (i, j) of R_{1} and (k, ℓ) of R_{2} such that

(1) w_{1}(i, j) < w_{2}(i, j) and w_{2}(k, ℓ) < w_{1}(k, ℓ); and

(2) w_{1}(i, j) + w_{2}(k, ℓ) + 2 ≤ w(i, ℓ) + w(k, j).

Proof. Suppose first that bd_{1} ⊎ bd_{2} ≠ bd_{1} ∪ bd_{2}, so that there exists p ∈ ℤ^{n} such that p ∈ bd_{1} ⊎ bd_{2} but p ∉ bd_{1} and p ∉ bd_{2}. Hence, there exist i, j, k, ℓ ∈ N such that (i, j) is an arc of R_{1} satisfying π_{i}(p) − π_{j}(p) > w_{1}(i, j) and (k, ℓ) is an arc of R_{2} satisfying π_{k}(p) − π_{ℓ}(p) > w_{2}(k, ℓ). However, as p ∈ bd_{1} ⊎ bd_{2}, π_{i}(p) − π_{j}(p) ≤ w(i, j) and π_{k}(p) − π_{ℓ}(p) ≤ w(k, ℓ) so that, by definition of G_{1} ⊔ G_{2}, we have w_{1}(i, j) < w_{2}(i, j) and w_{2}(k, ℓ) < w_{1}(k, ℓ); hence condition (1) holds. Note also that w_{1}(i, j) and w_{2}(k, ℓ) are both finite and hence in ℤ so that w_{1}(i, j) ≤ w_{2}(i, j) + 1 and w_{2}(k, ℓ) ≤ w_{1}(k, ℓ) + 1. Since p ∈ bd_{1} ⊎ bd_{2},

w(i, ℓ) + w(k, j) ≥ π_{i}(p) − π_{ℓ}(p) + π_{k}(p) − π_{j}(p)
= π_{i}(p) − π_{j}(p) + π_{k}(p) − π_{ℓ}(p)
≥ w_{1}(i, j) + w_{2}(k, ℓ) + 2.

Therefore, condition (2) also holds.

We now suppose that there exist arcs (i, j) of R_{1} and (k, ℓ) of R_{2} such that conditions (1) and (2) hold. Let G′ = (N , w′) be a graph defined as in the proof of Theorem 5.2, where however we just define ϵ := 1, so that G′ is an integer graph. By using the same reasoning as in the proof of Theorem 5.2, it can be seen that G′ is consistent and G′ ⊴ G_{1} ⊔ G_{2}. Let bd′ ∈ 𝔹𝔻_{n} be represented by G′, so that ∅ ≠ bd′ ⊆ bd_{1} ⊎ bd_{2}. Since w′(j, i) + w_{1}(i, j) < 0, we obtain bd′ ∩ bd_{1} = ∅; since w′(ℓ, k) + w_{2}(k, ℓ) < 0, we obtain bd′ ∩ bd_{2} = ∅. Hence, bd_{1} ⊎ bd_{2} ≠ bd_{1} ∪ bd_{2}. □

Example 5.4. Consider the 2-dimensional BD shapes

bd_{1} = con({0 ≤ x_{1} ≤ 3, 0 ≤ x_{2} ≤ 2, x_{1} − x_{2} ≤ 2}),
bd_{2} = con({3 ≤ x_{1} ≤ 6, 0 ≤ x_{2} ≤ 2}).

Then, in the case of rational BD shapes, the join bd_{1} ⊎ bd_{2} is not exact, since (2.5, 0)^{T} ∈ bd_{1} ⊎ bd_{2} although (2.5, 0)^{T} ∉ bd_{1} ∪ bd_{2}. Taking i = 1, j = 2, k = 0 and ℓ = 1, it can be seen that both conditions in Theorem 5.2 are satisfied; in particular, for the second condition we have

w_{1}(1, 2) + w_{2}(0, 1) = 2 − 3 ≤ 0 + 0 = w(1, 1) + w(0, 2).

By contrast, in the case of integer BD shapes, the join is exact; in particular, with the above choice for indices i, j, k, ℓ, the second condition of Theorem 5.3 does not hold:

w_{1}(1, 2) + w_{2}(0, 1) + 2 = 2 − 3 + 2 > 0 + 0 = w(1, 1) + w(0, 2).

5.2. Generalizing this result to k BD shapes

We conjecture that the above results for the exact join detection of two (rational or integer) BD shapes can be generalized to any number of component BD shapes. That is, given k BD shapes bd_{1}, …, bd_{k} ∈ 𝔹𝔻_{n}, it is possible to provide a suitable set of conditions that determine whether or not bd_{1} ⊎ ⋯ ⊎ bd_{k} = bd_{1} ∪⋯∪bd_{k}. Here we just present the conjecture, for the rational case, when k = 3.

Conjecture 5.5. For each h ∈ {1, 2, 3}, let bd_{h} ∈ 𝔹𝔻_{n} be a non-empty BD shape represented by the closed graph G_{h} = (N , w_{h}) and let R_{h} be a subgraph of G_{h} such that closure(R_{h}) = G_{h}. Let also G_{1} ⊔ G_{2} ⊔ G_{3} = (N , w). Then bd_{1} ⊎ bd_{2} ⊎ bd_{3} ≠ bd_{1} ∪ bd_{2} ∪ bd_{3} if and only if there exist arcs (i_{1}, j_{1}) of R_{1}, (i_{2}, j_{2}) of R_{2} and (i_{3}, j_{3}) of R_{3}, respectively, such that

(1) for each h ∈ {1, 2, 3}, w_{h}(i_{h}, j_{h}) < w(i_{h}, j_{h});

(2a) w_{1}(i_{1}, j_{1}) + w_{2}(i_{2}, j_{2}) < w(i_{1}, j_{2}) + w(i_{2}, j_{1});

(2b) w_{2}(i_{2}, j_{2}) + w_{3}(i_{3}, j_{3}) < w(i_{2}, j_{3}) + w(i_{3}, j_{2});

(2c) w_{3}(i_{3}, j_{3}) + w_{1}(i_{1}, j_{1}) < w(i_{3}, j_{1}) + w(i_{1}, j_{3});

(3a) w_{1}(i_{1}, j_{1}) + w_{2}(i_{2}, j_{2}) + w_{3}(i_{3}, j_{3}) < w(i_{1}, j_{2}) + w(i_{2}, j_{3}) + w(i_{3}, j_{1}); (3b) w_{1}(i_{1}, j_{1}) + w_{2}(i_{2}, j_{2}) + w_{3}(i_{3}, j_{3}) < w(i_{1}, j_{3}) + w(i_{2}, j_{1}) + w(i_{3}, j_{2}).

Even though the generalization is straightforward from a mathematical point of view, for larger values of k this will result in having to check a rather involved combinatorial combination of all the conditions.

6. Exact Join Detection for Octagonal Shapes

Octagonal constraints generalize BD constraints by also allowing for nonstrict inequalities having the form x_{i} + x_{j} ≤ b or −x_{i} − x_{j} ≤ b. Octagonal constraints can be encoded using BD constraints by splitting each variable x_{i} into two forms: a positive form x_{i}^{+}, interpreted as +x_{i}; and a negative form x_{i}^{−}, interpreted as −x_{i}. For instance, an octagonal constraint such as x_{i}+x_{j} ≤ b can be translated into the potential constraint x_{i}^{+} − x_{j}^{−} ≤ b; alternatively, the same octagonal constraint can be translated into x_{j}^{+} − x_{i}^{−} ≤ b. Unary (octagonal) constraints such as x_{i} ≤ b and −x_{i} ≤ b are encoded as x_{i}^{+} − x_{i}^{−} ≤ 2b and x_{i}^{−} − x_{i}^{+} ≤ −2b, respectively.

From now on, we assume that the set of nodes is N := {0, …, 2n−1}. These will denote the positive and negative forms of the vector space dimensions x_{1}, …, x_{n}: for all i ∈ N, if i = 2k, then i represents the positive form x_{k+1}^{+} and, if i = 2k + 1, then i represents the negative form x_{k+1}^{−} of the dimension x_{k+1}. To simplify the presentation, we let \overline{ı} denote i + 1, if i is even, and i − 1, if i is odd, so that, for all i ∈ N, we also have \overline{ı} ∈ N and \overline{\overline{ı}} = i.

It follows from the above translations that any finite system of octagonal constraints, translated into a set of potential constraints in N as above, can be encoded by a graph G in N. In particular, any finite satisfiable system of octagonal constraints can be encoded by a consistent graph in N. However, the converse does not hold since in any valuation ρ of an encoding of a set of octagonal constraints we must also have ρ(i) = −ρ(\overline{ı}), so that the arcs (i, j) and (\overline{ȷ}, \overline{ı}) should have the same weight. Therefore, to encode rational octagonal constraints, we restrict attention to consistent graphs over N where the arcs in all such pairs are coherent.

Definition 6.1. (Octagonal graph.) A (rational) octagonal graph is any consistent graph G = (N , w) that satisfies the coherence assumption:

∀i, j ∈ N : w(i, j) = w(\overline{ȷ}, \overline{ı}).  (5)

The set 𝕆 of all octagonal graphs (with the usual addition of the bottom element, representing an unsatisfiable system of constraints) is a sub-lattice of 𝔾_{⊥}, sharing the same least upper bound and greatest lower bound operators. Note that, at the implementation level, coherence can be automatically and efficiently enforced by letting arc (i, j) and arc (\overline{ȷ}, \overline{ı}) share the same representation.

The standard shortest-path closure algorithm is not enough to obtain a canonical form for octagonal graphs.

Definition 6.2. (Graph strong closure/reduction.) An octagonal graph G = (N , w) is strongly closed if it is closed and the following property holds:

∀i, j ∈ N : 2w(i, j) ≤ w(i, \overline{ı}) + w(\overline{ȷ}, j).  (6)

The strong closure of an octagonal graph G in N is

S-closure(G) := ⨆{ G′ ∈ 𝕆 | G′ ⊴ G and G′ is strongly closed }.

An octagonal graph R is strongly reduced if, for each octagonal graph G ≠ R such that R ⊴ G, we have S-closure(R) ≠ S-closure(G). A strong reduction for the octagonal graph G is any strongly reduced octagonal graph R such that S-closure(R) = S-closure(G).

Observe that, as was the case for shortest-path reduction, a strong reduction for a strongly closed graph G is a subgraph of G.

We denote by 𝕆ℂ𝕋_{n} the domain of octagonal shapes, whose non-empty elements can be represented by octagonal graphs: 𝔹𝔻_{n} is a meet-sublattice of 𝕆ℂ𝕋_{n}, which in turn is a meet-sublattice of ℂℙ_{n}. A strongly closed (resp., strongly reduced) graph encodes a system of octagonal constraints which is closed by entailment (resp., contains no redundant constraint).

Theorem 6.3. For each h ∈ {1, 2}, let oct_{h} ∈ 𝕆ℂ𝕋_{n} be a non-empty octagonal shape represented by the strongly closed graph G_{h} = (N , w_{h}) and let R_{h} be a subgraph of G_{h} such that S-closure(R_{h}) = G_{h}. Let also G_{1} ⊔G_{2} = (N , w). Then oct_{1} ⊎ oct_{2} ≠ oct_{1} ∪ oct_{2} if and only if there exist arcs (i, j) of R_{1} and (k, ℓ) of R_{2} such that

(1a) w_{1}(i, j) < w_{2}(i, j);

(1b) w_{2}(k, ℓ) < w_{1}(k, ℓ);

(2a) w_{1}(i, j) + w_{2}(k, ℓ) < w(i, ℓ) + w(k, j);

(2b) w_{1}(i, j) + w_{2}(k, ℓ) < w(i, \overline{k}) + w(\overline{ȷ}, ℓ);

(3a) 2w_{1}(i, j) + w_{2}(k, ℓ) < w(i, ℓ) + w(i, \overline{k}) + w(\overline{ȷ}, j);

(3b) 2w_{1}(i, j) + w_{2}(k, ℓ) < w(k, j) + w(\overline{ȷ}, ℓ) + w(i, \overline{ı});

(4a) w_{1}(i, j) + 2w_{2}(k, ℓ) < w(i, ℓ) + w(\overline{ȷ}, ℓ) + w(k, \overline{k});

(4b) w_{1}(i, j) + 2w_{2}(k, ℓ) < w(k, j) + w(i, \overline{k}) + w(\overline{ℓ}, ℓ).

Proof. For each r ∈ N = {0, …, 2n − 1} and each v = (v_{1}, …, v_{n})^{T} ∈ ℝ^{n}, we denote by π̃_{r}(v) the projection of vector v on the space dimension corresponding to the octagonal graph node r, defined as:

π̃_{r}(v) := \begin{cases}v_{s+1}, & if r = 2s; \\ −v_{s+1}, & if r = 2s + 1. \end{cases}

Suppose that oct_{1} ⊎ oct_{2} ≠ oct_{1} ∪ oct_{2}, so that there exists p ∈ oct_{1} ⊎ oct_{2} such that p ∉ oct_{1} and p ∉ oct_{2}. Hence, there exist arcs (i, j) and (k, ℓ) of R_{1} and R_{2}, respectively, satisfying

w(i, j) ≥ π̃_{i}(p) − π̃_{j}(p) > w_{1}(i, j),
w(k, ℓ) ≥ π̃_{k}(p) − π̃_{ℓ}(p) > w_{2}(k, ℓ);

hence conditions (1a) and (1b) hold;

w(i, ℓ) + w(k, j) ≥ π̃_{i}(p) − π̃_{ℓ}(p) + π̃_{k}(p) − π̃_{j}(p)
= π̃_{i}(p) − π̃_{j}(p) + π̃_{k}(p) − π̃_{ℓ}(p)
> w_{1}(i, j) + w_{2}(k, ℓ)

so that condition (2a) holds and, by a symmetric argument, condition (2b) holds;

w(i, ℓ) + w(i, \overline{k}) + w(\overline{ȷ}, j) ≥ (π̃_{i}(p) − π̃_{ℓ}(p)) + (π̃_{i}(p) + π̃_{k}(p)) + (−2 π̃_{j}(p))
= 2(π̃_{i}(p) − π̃_{j}(p)) + π̃_{k}(p) − π̃_{ℓ}(p)
> 2w_{1}(i, j) + w_{2}(k, ℓ)

so that condition (3a) holds; conditions (3b), (4a) and (4b) follow by symmetric arguments.

We now suppose that, for some i, j, k, ℓ ∈ N, all conditions (1a) – (4b) hold. Note that, by (1a) and (1b), i ≠ j and k ≠ ℓ. Suppose first that (i, j) ∈ \{(ℓ, k), (\overline{k}, \overline{ℓ})\}; then, conditions (1a) – (2b) imply w_{1}(i, j) + w_{2}(j, i) < 0, so that the graph greatest lower bound G_{1} ⊓ G_{2} is inconsistent, as it contains a negative weight proper cycle; hence, oct_{1}∩oct_{2} = ∅, which implies oct_{1}⊎oct_{2} ≠ oct_{1} ∪ oct_{2}. Therefore, in the following we assume that (i, j) ∉ \{(ℓ, k), (\overline{k}, \overline{ℓ})\} holds.

If the right hand sides of the inequalities in conditions (1a) – (4b) are all unbounded, let ϵ := 1; otherwise let

ϵ := min \{ \begin{matrix}w(i, j) − w_{1}(i, j), \\ w(k, ℓ) − w_{2}(k, ℓ), \\ \frac{1}{2}(w(i, ℓ) + w(k, j) − w_{1}(i, j) − w_{2}(k, ℓ)), \\ \frac{1}{2}(w(i, \overline{k}) + w(\overline{ȷ}, ℓ) − w_{1}(i, j) − w_{2}(k, ℓ)), \\ \frac{1}{3}(w(i, ℓ) + w(i, \overline{k}) + w(\overline{ȷ}, j) − 2w_{1}(i, j) − w_{2}(k, ℓ)), \\ \frac{1}{3}(w(k, j) + w(\overline{ȷ}, ℓ) + w(i, \overline{ı}) − 2w_{1}(i, j) − w_{2}(k, ℓ)), \\ \frac{1}{3}(w(i, ℓ) + w(\overline{ȷ}, ℓ) + w(k, \overline{k}) − w_{1}(i, j) − 2w_{2}(k, ℓ)), \\ \frac{1}{3}(w(k, j) + w(i, \overline{k}) + w(\overline{ℓ}, ℓ) − w_{1}(i, j) − 2w_{2}(k, ℓ)) \end{matrix}\} .

Then, by conditions (1a) – (4b) ϵ > 0. Consider the graph G′ = (N , w′) where, for each r, s ∈ N,

w′(r, s) := \begin{cases}−w_{1}(i, j) − ϵ, & if (r, s) ∈ \{(j, i), (\overline{ı}, \overline{ȷ})\}; \\ −w_{2}(k, ℓ) − ϵ, & if (r, s) ∈ \{(ℓ, k), (\overline{k}, \overline{ℓ})\}; \\ w(r, s), & otherwise. \end{cases}

Let G := G_{1} ⊔ G_{2}; as G is coherent, G′ is coherent too. We now show that G′ is a consistent graph; to this end, since G is known to be consistent, it is sufficient to consider the proper cycles of G′ that contain arc (j, i) or arc (ℓ, k).^{7} Let θ_{ij} = i ⋯ j and θ_{kℓ} = k ⋯ ℓ be any simple paths from i to j and from k to ℓ, respectively. Then G′ is consistent if and only if w′(θ_{ij} · i) ≥ 0 and w′(θ_{kℓ} · k) ≥ 0. We only prove w′(θ_{ij} · i) ≥ 0 since the proof that w′(θ_{kℓ} · k) ≥ 0 follows by a symmetrical argument. Since θ_{ij} is simple, it does not contain the arc (j, i). In the following we consider in detail five cases, again noting that all the other cases can be proved by symmetrical arguments:

1. θ_{ij} contains none of the arcs (ℓ, k), (\overline{k}, \overline{ℓ}) and (\overline{ı}, \overline{ȷ});

2. θ_{ij} = θ_{i\overline{ı}} :: (\overline{ı}, \overline{ȷ}) :: θ_{\overline{ȷ}j};

3. θ_{ij} = θ_{iℓ} :: (ℓ, k) :: θ_{kj};

4. θ_{ij} = θ_{iℓ} :: (ℓ, k) :: θ_{k\overline{k}} :: (\overline{k}, \overline{ℓ}) :: θ_{\overline{ℓ}j};

5. θ_{ij} = θ_{iℓ} :: (ℓ, k) :: θ_{k\overline{k}} :: (\overline{k}, \overline{ℓ}) :: θ_{\overline{ℓ}\overline{ı}} :: (\overline{ı}, \overline{ȷ}) :: θ_{\overline{ȷ}j},

where the simple paths θ_{i\overline{ı}}, θ_{iℓ}, θ_{kj}, θ_{k\overline{k}}, θ_{\overline{ℓ}j}, θ_{\overline{ℓ}\overline{ı}} and θ_{\overline{ȷ}j} contain none of the arcs (ℓ, k), (\overline{k}, \overline{ℓ}) and (\overline{ı}, \overline{ȷ}).

• Case (1).

w′(θ_{ij} · i) = w′(θ_{ij}) + w′(j, i)
= w(θ_{ij}) − w_{1}(i, j) − ϵ  [def. of w′]
≥ w(i, j) − w_{1}(i, j) − ϵ  [G closed]
≥ 0  [def. of ϵ].

7Any cycle containing arc (\overline{ı}, \overline{ȷ}) (resp., (\overline{k}, \overline{ℓ})) can be transformed to the corresponding coherent cycle containing arc (j, i) (resp., (ℓ, k)), having the same weight.

• Case (2).

w′(θ_{ij} · i) = w′(θ_{i\overline{ı}}) + w′(\overline{ı}, \overline{ȷ}) + w′(θ_{\overline{ȷ}j}) + w′(j, i)
= w′(θ_{i\overline{ı}}) + w′(θ_{\overline{ȷ}j}) + 2w′(j, i)  [G′ coherent]
= w(θ_{i\overline{ı}}) + w(θ_{\overline{ȷ}j}) − 2w_{1}(i, j) − 2ϵ  [def. of w′]
≥ w(i, \overline{ı}) + w(\overline{ȷ}, j) − 2w_{1}(i, j) − 2ϵ  [G closed]
≥ 2w(i, j) − 2w_{1}(i, j) − 2ϵ  [G strongly closed]

= 2(w(i, j) − w_{1}(i, j)) − 2ϵ

≥ 0  [def. of ϵ].

• Case (3).

w′(θ_{ij} · i) = w′(θ_{iℓ}) + w′(ℓ, k) + w′(θ_{kj}) + w′(j, i)
= w(θ_{iℓ}) − w_{2}(k, ℓ) − ϵ + w(θ_{kj}) − w_{1}(i, j) − ϵ [def. of w′]
≥ w(i, ℓ) − w_{2}(k, ℓ) − ϵ + w(k, j) − w_{1}(i, j) − ϵ [G closed]

= (w(i, ℓ) + w(k, j) − w_{1}(i, j) − w_{2}(k, ℓ)) − 2ϵ

≥ 0  [def. of ϵ].

• Case (4).

w′(θ_{ij} · i)

= w′(θ_{iℓ}) + w′(ℓ, k) + w′(θ_{k\overline{k}}) + w′(\overline{k}, \overline{ℓ}) + w′(θ_{\overline{ℓ}j}) + w′(j, i)

= w′(θ_{iℓ}) + 2w′(ℓ, k) + w′(θ_{k\overline{k}}) + w′(θ_{\overline{ȷ}ℓ}) + w′(j, i)  [G′ coherent]
= w(θ_{iℓ}) − 2w_{2}(k, ℓ) − 2ϵ + w(θ_{k\overline{k}}) + w(θ_{\overline{ȷ}ℓ}) − w_{1}(i, j) − ϵ  [def. of w′]
≥ w(i, ℓ) − 2w_{2}(k, ℓ) − 2ϵ + w(k, \overline{k}) + w(\overline{ȷ}, ℓ) − w_{1}(i, j) − ϵ  [G closed]

= (w(i, ℓ) + w(\overline{ȷ}, ℓ) + w(k, \overline{k}) − w_{1}(i, j) − 2w_{2}(k, ℓ)) − 3ϵ

≥ 0  [def. of ϵ].

• Case (5).

w′(θ_{ij} · i) = w′(θ_{iℓ}) + w′(ℓ, k) + w′(θ_{k\overline{k}}) + w′(\overline{k}, \overline{ℓ})
+ w′(θ_{\overline{ℓ}\overline{ı}}) + w′(\overline{ı}, \overline{ȷ}) + w′(θ_{\overline{ȷ}j}) + w′(j, i)
= 2w′(θ_{iℓ}) + 2w′(j, i)
+ w′(θ_{k\overline{k}}) + w′(θ_{\overline{ȷ}j}) + 2w′(ℓ, k)  [G′ coherent]
= 2w(θ_{iℓ}) − 2w_{1}(i, j) − 2ϵ
+ w(θ_{k\overline{k}}) + w(θ_{\overline{ȷ}j}) − 2w_{2}(k, ℓ) − 2ϵ  [def. of w′]
≥ 2w(i, ℓ) − 2w_{1}(i, j) − 2ϵ
+ w(k, \overline{k}) + w(\overline{ȷ}, j) − 2w_{2}(k, ℓ) − 2ϵ  [G closed]
≥ 2w(i, ℓ) − 2w_{1}(i, j) − 2ϵ
+ 2w(k, j) − 2w_{2}(k, ℓ) − 2ϵ  [G strongly closed]
= 2(w(i, ℓ) + w(k, j) − w_{1}(i, j) − w_{2}(k, ℓ)) − 4ϵ
≥ 0  [def. of ϵ].

Therefore G′ is consistent. Moreover, G′ ⊴ G since

w′(j, i) = −w_{1}(i, j) − ϵ  [def. of w′]
≤ −w_{1}(i, j)  [ϵ ≥ 0]
≤ w_{1}(j, i)  [G_{1} consistent]
≤ w(j, i)  [def. G];

similarly, w′(ℓ, k) ≤ w(ℓ, k); hence, for all r, s ∈ N, w′(r, s) ≤ w(r, s).

Let oct′ ∈ 𝕆ℂ𝕋_{n} be represented by G′, so that ∅ ≠ oct′ ⊆ oct_{1} ⊎oct_{2}. Since w′(j, i) + w_{1}(i, j) < 0, we obtain oct′ ∩ oct_{1} = ∅; since w′(ℓ, k) + w_{2}(k, ℓ) < 0, we obtain oct′ ∩ oct_{2} = ∅. Hence, oct_{1} ⊎ oct_{2} ≠ oct_{1} ∪ oct_{2}. □

Since the computation of the strong closure and strong reduction of an octagonal graph are both in O(n^{3}) [2, 9, 31], an algorithm for the exact join detection on 𝕆ℂ𝕋_{n} based on Theorem 6.3 has the same asymptotic worst-case complexity as the corresponding algorithm for 𝔹𝔻_{n}.

Example 6.4. Consider the 2-dimensional octagonal shapes

oct_{1} = con({x_{1} + x_{2} ≤ 0}),
oct_{2} = con({x_{1} ≤ 2}}.

Then, the join oct_{1} ⊎ oct_{2} = ℝ^{2} is not exact. In fact, taking i = 0, j = 3, k = 0 and ℓ = 1, we have w_{1}(i, j) = 0 and w_{2}(k, ℓ) = 4, so that all the left hand sides in conditions (1a) – (4b) are finite; since all the corresponding right hand sides are infinite, all the conditions hold.

6.1. Integer Octagonal Shapes

We now consider the case of integer octagonal constraints, i.e., octagonal constraints where the bounds are all integral and the variables are only allowed to take integral values. These can be encoded by suitably restricting the codomain of the weight function of octagonal graphs.

Definition 6.5. (Integer octagonal graph.) An integer octagonal graph is an octagonal graph G = (N , w) having an integral weight function:

∀i, j ∈ N : w(i, j) ∈ ℤ ∪ {+∞}.

As an integer octagonal graph is also a rational octagonal graph, the constraint system that it encodes will be satisfiable when interpreted to take values in ℚ. However, when interpreted to take values in ℤ, this system may be unsatisfiable since the arcs encoding unary constraints can have an odd weight; we say that an octagonal graph is ℤ-consistent if its encoded integer constraint system is satisfiable. For the same reason, the strong closure of an integer octagonal graph does not provide a canonical form for the integer constraint system.

Definition 6.6. (Graph tight closure/reduction.) An octagonal graph G = (N , w) is tightly closed if it is a strongly closed integer octagonal graph and the following property holds:

∀i ∈ N : w(i, \overline{ı}) is even.  (7)

The tight closure of an octagonal graph G in N is

T-closure(G) := ⨆{ G′ ∈ 𝕆 | G′ ⊴ G and G′ is tightly closed }.

An ℤ-consistent integer octagonal graph R is tightly reduced if, for each integer octagonal graph G ≠ R such that R ⊴ G, we have T-closure(R) ≠ T-closure(G). A tight reduction for the ℤ-consistent integer octagonal graph G is any tightly reduced graph R such that T-closure(R) = T-closure(G).

It follows from these definitions that any tightly closed integer octagonal graph encodes a satisfiable integer constraint system if and only if it is ℤ-consistent [6, 9]. Therefore, tight closure is a kernel operator on the lattice of octagonal graphs, as was the case for strong closure. Observe also that a tight reduction for a tightly closed graph G is a subgraph of G [9].

To prove the Theorem 6.8 below, we will also use the following result proved in [27, Lemma 4].

Lemma 6.7. Let G = (N , w) be an integer octagonal graph with no negative weight cycles and G_{t} = (N , w_{t}), where w_{t} satisfies

w_{t}(i, j) := \begin{cases}2⌊w(i, j)/2⌋, & if j = \overline{ı}; \\ w(i, j), & otherwise; \end{cases}

have a negative weight cycle. Then there exist i, \overline{ı} ∈ N and a cycle π = (i·π_{1}·\overline{ı}) :: (\overline{ı} · π_{2} · i) in G such that w(π) = 0 and the weight of the shortest path in G from i to \overline{ı} is odd.

Theorem 6.8. For each h ∈ {1, 2}, let oct_{h} ∈ 𝕆ℂ𝕋_{n} be a non-empty integer octagonal shape represented by the tightly closed graph G_{h} = (N , w_{h}) and let R_{h} be a subgraph of G_{h} such that T-closure(R_{h}) = G_{h}. Let also G_{1} ⊔ G_{2} = (N , w). Then oct_{1} ⊎ oct_{2} ≠ oct_{1} ∪ oct_{2} if and only if there exists arcs (i, j) of R_{1} and (k, ℓ) of R_{2} such that, letting ϵ_{ij} = 2 if j = \overline{ı} and ϵ_{ij} = 1 otherwise and ϵ_{kℓ} = 2 if ℓ = \overline{k} and ϵ_{kℓ} = 1 otherwise, the following hold:

(1a) w_{1}(i, j) + ϵ_{ij} ≤ w_{2}(i, j);

(1b) w_{2}(k, ℓ) + ϵ_{kℓ} ≤ w_{1}(k, ℓ);

(2a) w_{1}(i, j) + w_{2}(k, ℓ) + ϵ_{ij} + ϵ_{kℓ} ≤ w(i, ℓ) + w(k, j);

(2b) w_{1}(i, j) + w_{2}(k, ℓ) + ϵ_{ij} + ϵ_{kℓ} ≤ w(i, \overline{k}) + w(\overline{ℓ}, j);

(3a) 2w_{1}(i, j) + w_{2}(k, ℓ) + 2ϵ_{ij} + ϵ_{kℓ} ≤ w(i, ℓ) + w(k, \overline{ı}) + w(\overline{ȷ}, j);

(3b) 2w_{1}(i, j) + w_{2}(k, ℓ) + 2ϵ_{ij} + ϵ_{kℓ} ≤ w(k, j) + w(\overline{ȷ}, ℓ) + w(i, \overline{ı});

(4a) w_{1}(i, j) + 2w_{2}(k, ℓ) + ϵ_{ij} + 2ϵ_{kℓ} ≤ w(k, j) + w(i, \overline{k}) + w(\overline{ℓ}, ℓ);

(4b) w_{1}(i, j) + 2w_{2}(k, ℓ) + ϵ_{ij} + 2ϵ_{kℓ} ≤ w(i, ℓ) + w(\overline{ℓ}, j) + w(k, \overline{k}).

Proof. We will use the notation π̃ as defined in the proof of Theorem 6.3. Suppose that oct_{1} ⊎ oct_{2} ≠ oct_{1} ∪ oct_{2}, so that there exists p ∈ oct_{1} ⊎ oct_{2} such that p ∉ oct_{1} and p ∉ oct_{2}. Hence, letting p̃_{ij} := π̃_{i}(p) − π̃_{j}(p) and p̃_{kℓ} := π̃_{k}(p)−π̃_{ℓ}(p), there exist arcs (i, j) and (k, ℓ) of R_{1} and R_{2}, respectively, satisfying p̃_{ij} > w_{1}(i, j) and p̃_{kℓ} > w_{2}(k, ℓ); as p ∈ oct_{1} ⊎ oct_{2}, we also have w_{2}(i, j) ≥ p̃_{ij} and w_{1}(k, ℓ) ≥ p̃_{kℓ}. Note that w_{1}(i, j) and w_{2}(k, ℓ) are both finite and hence in ℤ so that p̃_{ij} ≥ w_{1}(i, j)+1 and p̃_{kℓ} ≥ w_{2}(k, ℓ)+1; also, by the tight coherence rule (7), if j = \overline{ı}, p̃_{ij} ≥ w_{1}(i, j) + 2 and, if k = \overline{ℓ}, p̃_{kℓ} ≥ w_{2}(k, ℓ) + 2. Therefore, by definition of ϵ_{ij} and ϵ_{kℓ}, we have

w_{2}(i, j) ≥ π̃_{i}(p) − π̃_{j}(p)
≥ w_{1}(i, j) + ϵ_{ij},
w_{1}(k, ℓ) ≥ π̃_{k}(p) − π̃_{ℓ}(p)
≥ w_{2}(k, ℓ) + ϵ_{kℓ}

so that conditions (1a) and (1b) hold. Moreover,

w(i, ℓ) + w(k, j) ≥ π̃_{i}(p) − π̃_{ℓ}(p) + π̃_{k}(p) − π̃_{j}(p)
= π̃_{i}(p) − π̃_{j}(p) + π̃_{k}(p) − π̃_{ℓ}(p)
≥ w_{1}(i, j) + w_{2}(k, ℓ) + ϵ_{ij} + ϵ_{kℓ}

so that condition (2a) holds and, by a symmetric argument, condition (2b) holds. Similarly,

w(i, ℓ) + w(k, \overline{ı}) + w(\overline{ȷ}, j) ≥ (π̃_{i}(p) − π̃_{ℓ}(p)) + (π̃_{k}(p) + π̃_{i}(p)) + (−2 π̃_{j}(p))
= 2(π̃_{i}(p) − π̃_{j}(p)) + π̃_{k}(p) − π̃_{ℓ}(p)
≥ 2w_{1}(i, j) + w_{2}(k, ℓ) + 2ϵ_{ij} + ϵ_{kℓ}

so that condition (3a) holds; conditions (3b), (4a) and (4b) follow by a symmetrical argument.

We now suppose that, for some i, j, k, ℓ ∈ N, conditions (1a) – (4b) hold. Consider the graph G′ = (N , w′) where, for each r, s ∈ N,

w′(r, s) := \begin{cases}−w_{1}(i, j) − ϵ_{ij}, & if (r, s) ∈ \{(j, i), (\overline{ı}, \overline{ȷ})\}; \\ −w_{2}(k, ℓ) − ϵ_{kℓ}, & if (r, s) ∈ \{(ℓ, k), (\overline{k}, \overline{ℓ})\}; \\ w(r, s), & otherwise. \end{cases}

Let G := G_{1} ⊔G_{2}; as G is coherent, G′ is coherent too; as G is tightly closed, G′ satisfies property (7). Hence it follows from Lemma 6.7 that G′ is ℤ-consistent if it has no negative weight cycles. By using a reasoning similar to that in the proof of Theorem 6.3, it can be seen that there are no negative weight cycles in G′ so that G′ is ℤ-consistent and G′ ⊴G_{1} ⊔G_{2}. Let oct′ ∈ 𝕆ℂ𝕋_{n} be represented by G′, so that ∅ ≠ oct′ ⊆ oct_{1} ⊎ oct_{2}. Since w′(j, i) + w_{1}(i, j) < 0, we obtain oct′ ∩ oct_{1} = ∅; since w′(ℓ, k) + w_{2}(k, ℓ) < 0, we obtain oct′ ∩ oct_{2} = ∅. Hence, oct_{1} ⊎ oct_{2} ≠ oct_{1} ∪ oct_{2}. □

Since the tight closure and tight reduction procedures are both in O(n^{3}) [9], the exact join detection algorithm for integer octagonal shapes has the same asymptotic worst-case complexity of all the corresponding algorithms for the other weakly relational shapes.

7. Conclusion and Future Work

Several applications dealing with the synthesis, analysis, verification and optimization of hardware and software systems make use of numerical abstractions. These are sets of geometrical objects —with the structure of a bounded joinsemilattice— that are used to approximate the numerical quantities occurring in such systems. In order to improve the precision of the approximation, sets of such objects are often considered and, to limit redundancy and its negative effects, it is important to “merge” objects whose lattice-theoretic join corresponds to their set-theoretic union.

For a wide range of numerical abstractions, we have presented results that state the necessity and sufficiency of relatively simple conditions for the equivalence between join and union. These conditions immediately suggest algorithms that solve the corresponding decision problem. For the case of convex polyhedra, we improve upon one of the algorithms presented in [12, 13] by defining an algorithm with better worst-case complexity. For all the other considered numerical abstractions, we believe the present paper is breaking new ground. In particular, for the case of NNC convex polyhedra, we show that dealing with non-closedness brings significant extra complications. For the other abstractions, the algorithms we propose have worst-case complexities that, in a sense, match the complexity of the abstraction, something that cannot be obtained, e.g., by applying an algorithm for general convex polyhedra to octagonal shapes.

All the above mentioned algorithms have been implemented in the Parma Polyhedra Library [7].^{8} Besides being made directly available to the client applications, they are used internally in order to implement widening operators over powerset domains [4]. Our preliminary experimental evaluation, though not extensive, showed the efficiency of the algorithms is good, also thanks to a careful coding following the “first fail” principle.^{9}

Even though preliminary experimentation suggests that —in practice, at least for some applications [4, 16]— pairwise joins allow the removal of most redundancies, work is still needed in the definition of efficient algorithms to decide the exactness of join for k > 2 objects. Moreover, it would be useful to develop heuristics to mitigate the combinatorial explosion when attempting full redundancy removal from a set of m objects, as it is clearly impractical to invoke 2^{m} − m − 1 times the decision algorithm on k = 2, …, m objects.

Acknowledgments. We are grateful to the participants of the Graphite Workshop (AMD’s Lone Star Campus, Austin, Texas, November 16–17, 2008) for stimulating us to add efficient exact join detection algorithms to the Parma Polyhedra Library, something that led us to the research described in this paper.

References

[1] R. Bagnara, A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages, Science of Computer Programming 30 (1– 2) (1998) 119–155.

[2] R. Bagnara, P. M. Hill, E. Mazzi, E. Zaffanella, Widening operators for weakly-relational numeric abstractions, in: C. Hankin, I. Siveroni (eds.), Static Analysis: Proceedings of the 12th International Symposium, vol. 3672 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, London, UK, 2005.

[3] R. Bagnara, P. M. Hill, E. Zaffanella, Not necessarily closed convex polyhedra and the double description method, Formal Aspects of Computing 17 (2) (2005) 222–257.

[4] R. Bagnara, P. M. Hill, E. Zaffanella, Widening operators for powerset domains, Software Tools for Technology Transfer 8 (4/5) (2006) 449–466, in the printed version of this article, all the figures have been improperly printed (rendering them useless). See [5].

[5] R. Bagnara, P. M. Hill, E. Zaffanella, Widening operators for powerset domains, Software Tools for Technology Transfer 9 (3/4) (2007) 413–414, erratum to [4] containing all the figures properly printed.

8The Parma Polyhedra Library is free software distributed under the terms of the GNU General Public License. See http://www.cs.unipr.it/ppl/ for further details.

9This is a heuristics whereby, in the implementation of a predicate whose success depends on the success of many tests, those that are most likely to fail are tried first.

[6] R. Bagnara, P. M. Hill, E. Zaffanella, An improved tight closure algorithm for integer octagonal constraints, in: F. Logozzo, D. Peled, L. Zuck (eds.), Verification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008), vol. 4905 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, San Francisco, USA, 2008.

[7] R. Bagnara, P. M. Hill, E. Zaffanella, The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Science of Computer Programming 72 (1–2) (2008) 3–21.

[8] R. Bagnara, P. M. Hill, E. Zaffanella, Applications of polyhedral computations to the analysis and verification of hardware and software systems, Theoretical Computer ScienceTo appear.

[9] R. Bagnara, P. M. Hill, E. Zaffanella, Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness, submitted for publication (2009).

[10] I. Bárány, K. Fukuda, A case when the union of polytopes is convex, Linear Algebra and its Applications 397 (2005) 381–388.

[11] C. Bastoul, Code generation in the polyhedral model is easier than you think, in: Proceedings of the 13th International Conference on Parallel Architectures and Compilation Techniques (PACT 2004), IEEE Computer Society, Antibes Juan-les-Pins, France, 2004.

[12] A. Bemporad, K. Fukuda, F. D. Torrisi, Convexity recognition of the union of polyhedra, Report AUT00-13, Automatic Control Laboratory, ETHZ, Zurich, Switzerland (2000).

[13] A. Bemporad, K. Fukuda, F. D. Torrisi, Convexity recognition of the union of polyhedra, Computational Geometry: Theory and Applications 18 (3) (2001) 141–154.

[14] A. Bemporad, M. Morari, V. Dua, E. N. Pistikopoulos, The explicit linear quadratic regulator for constrained systems, Automatica 38 (1) (2002) 3– 20, corrected in [15].

[15] A. Bemporad, M. Morari, V. Dua, E. N. Pistikopoulos, Corrigendum to: “The explicit linear quadratic regulator for constrained systems” [Automatica 38(1) (2002) 3–20], Automatica 39 (10) (2003) 1845–1846, corrigendum to [14].

[16] T. Bultan, R. Gerber, W. Pugh, Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results, ACM Transactions on Programming Languages and Systems 21 (4) (1999) 747–789.

[17] N. V. Chernikova, Algorithm for finding a general formula for the nonnegative solutions of system of linear equations, U.S.S.R. Computational Mathematics and Mathematical Physics 4 (4) (1964) 151–158.

[18] N. V. Chernikova, Algorithm for finding a general formula for the nonnegative solutions of system of linear inequalities, U.S.S.R. Computational Mathematics and Mathematical Physics 5 (2) (1965) 228–233.

[19] N. V. Chernikova, Algorithm for discovering the set of all solutions of a linear programming problem, U.S.S.R. Computational Mathematics and Mathematical Physics 8 (6) (1968) 282–293.

[20] P. Cousot, R. Cousot, Static determination of dynamic properties of programs, in: B. Robinet (ed.), Proceedings of the Second International Symposium on Programming, Dunod, Paris, France, Paris, France, 1976.

[21] P. Cousot, R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, ACM Press, New York, 1977.

[22] P. Cousot, R. Cousot, Systematic design of program analysis frameworks, in: Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, ACM Press, New York, 1979.

[23] P. Feautrier, Parametric integer programming, RAIRO Recherche Opérationnelle 22 (3) (1988) 243–268.

[24] G. Frehse, B. H. Krogh, R. A. Rutenbar, Verifying analog oscillator circuits using forward/backward refinement, in: Proceedings of the 9th Conference on Design, Automation and Test in Europe (DATE 06), ACM SIGDA, Munich, Germany, 2006, CD-ROM publication.

[25] K. Fukuda, T. M. Liebling, C. Lütolf, Extended convex hull, Computational Geometry: Theory and Applications 20 (1–2) (2001) 13–23.

[26] C. N. Jones, Polyhedal tools for control, Ph.D. thesis, Department of Engineering,University of Cambridge, Cambridge, U.K. (Jul. 2005).

[27] S. K. Lahiri, M. Musuvathi, An efficient decision procedure for UTVPI constraints, in: B. Gramlich (ed.), Frontiers of Combining Systems: Proceedings of the 5th International Workshop, FroCoS 2005, vol. 3717 of Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, Vienna, Austria, 2005.

[28] K. Larsen, F. Larsson, P. Pettersson, W. Yi, Efficient verification of realtime systems: Compact data structure and state-space reduction, in: Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS’97), IEEE Computer Society Press, San Francisco, CA, 1997.

[29] H. Le Verge, A note on Chernikova’s algorithm, Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France (1992).

[30] A. Miné, A new numerical abstract domain based on difference-bound matrices, in: O. Danvy, A. Filinski (eds.), Proceedings of the 2nd Symposium on Programs as Data Objects (PADO 2001), vol. 2053 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Aarhus, Denmark, 2001.

[31] A. Miné, Weakly relational numerical abstract domains, Ph.D. thesis, École Polytechnique, Paris, France (Mar. 2005).

[32] T. S. Motzkin, H. Raiffa, G. L. Thompson, R. M. Thrall, The double description method, in: H. W. Kuhn, A. W. Tucker (eds.), Contributions to the Theory of Games – Volume II, No. 28 in Annals of Mathematics Studies, Princeton University Press, Princeton, New Jersey, 1953, pp. 51– 73.

[33] T. Nakanishi, A. Fukuda, Modulo interval arithmetic and its application to program analysis, Transactions of Information Processing Society of Japan 42 (4) (2001) 829–837.

[34] T. Nakanishi, K. Joe, C. D. Polychronopoulos, A. Fukuda, The modulo interval: A simple and practical representation for program analysis, in: Proceedings of the 1999 International Conference on Parallel Architectures and Compilation Techniques, IEEE Computer Society, Newport Beach, California, USA, 1999.

[35] R. Sen, Y. N. Srikant, Executable analysis using abstract interpretation with circular linear progressions, in: Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2007), IEEE Computer Society Press, Nice, France, 2007.

[36] J. Stoer, C. Witzgall, Convexity and Optimization in Finite Dimensions I, Springer-Verlag, Berlin, 1970.

[37] F. D. Torrisi, Modeling and reach-set computation for analysis and optimal control of discrete hybrid automata, Doctoral thesis, Swiss Federal Institute of Technology, Zürich, Switzerland (2003).