Noname manuscript No. (will be inserted by the editor)

Weakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness

Roberto Bagnara · Patricia M. Hill · Enea Zaffanella

Received: September 1, 2008

Abstract Weakly-relational numeric constraints provide a compromise between complexity and expressivity that is adequate for several applications in the field of formal analysis and verification of software and hardware systems. We address the problems to be solved for the construction of full-fledged, efficient and provably correct abstract domains based on such constraints. We first propose to work with semantic abstract domains, whose elements are geometric shapes, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices on which the previous proposals are based. This allows to solve, once and for all, the problem whereby closure by entailment, a crucial operation for the realization of such domains, seemed to impede the realization of proper widening operators. In our approach, the implementation of widenings relies on the availability of an effective reduction procedure for the considered constraint description: one for the domain of bounded difference shapes already exists in the literature; we provide algorithms for the significantly more complex cases of rational and integer octagonal shapes. We also improve upon the state-of-the-art by presenting, along with their proof of correctness, closure by entailment algorithms of reduced complexity for domains based on rational and integer octagonal constraints. The consequences of implementing weakly-relational numerical domains with floating point numbers are also discussed.

This work has been partly supported by MURST projects “Constraint Based Verification of Reactive Systems” and “AIDA — Abstract Interpretation: Design and Applications,” and by a Royal Society (UK) International Joint Project (ESEP) award.

R. Bagnara Department of Mathematics, University of Parma Viale G. P. Usberti 53/A, 43100 Parma, Italy Tel.: +39-0521-906917, Fax: +39-0521-906950, E-mail: bagnara@cs.unipr.it P. M. Hill School of Computing, University of Leeds Leeds LS2 9JT, ENGLAND Tel.: +44-(0)113-3436807, Fax: +44-(0)113-3435468, E-mail: p.m.hill@leeds.ac.uk E. Zaffanella Department of Mathematics, University of Parma, Italy Viale G. P. Usberti 53/A, 43100 Parma, Italy Tel.: +39-0521-906963, Fax: +39-0521-906950, E-mail: zaffanella@cs.unipr.it

1 Introduction

Numerical properties are of great interest in the broad area of formal methods for their complete generality and for the crucial role they often play in the definition of static analyses and program verification techniques. In the field of abstract interpretation, classes of numerical properties are captured by numerical abstract domains. These have been and are widely used, either as the main abstraction for the application at hand, or as powerful ingredients to improve the precision of other abstract domains.

Among the wide spectrum of numerical abstractions proposed in the literature, probably the most famous are the (non-relational) abstract domain of intervals [1] and the (relational) abstract domain of convex polyhedra [2]. As far as the efficiency/precision trade-off is concerned, these domains occupy the opposite ends of the spectrum: on the one hand, the operations on convex polyhedra achieve a significant level of precision, which is however countered by a worst-case exponential time complexity that demands particular care with its use if scalability problems are to be avoided; on the other hand, the great efficiency of the corresponding operations on intervals is made unappealing by the fact that the obtained precision is often unsatisfactory. This well-known dichotomy (which does not impede that, for some applications, convex polyhedra or intervals are the right choices) has motivated recent studies on several abstract domains that lie somewhere between these two extremes, and can therefore be called weakly-relational abstract domains. Examples include domains based on constraint networks [3–5], the abstract domain of difference-bound matrices [6,7], the octagon abstract domain [8], the ‘two variables per inequality’ abstract domain [9], the octahedron abstract domain [10], and the abstract domain of template constraint matrices [11]. Moreover, similar proposals that are not abstractions of the domain of convex polyhedra have been put forward, including the abstract domain of bounded quotients [3], the zone congruence abstract domain [12] and the one of integer octagonal constraints.

The latter constraints —that is, constraints of the form ax + by ≤ d where a, b ∈ {−1, 0, +1}, d ∈ ℤ and the variables x and y range over the integers— are also called Unit Two Variables Per Inequality (UTVPI) integer constraints and constitute an interesting subclass of linear integer constraints admitting polynomial solvability. The place which these constraints occupy in the complexity/expressivity spectrum is, in fact, peculiar. Concerning complexity, relaxing the restriction of (at most) two variables per constraint and/or relaxing the restriction on coefficients make the satisfiability problem NP-complete [13,14]. Concerning expressivity, these constraints have been successfully used in a number of applications [15–18] in the field of formal analysis and verification of software and hardware systems. Besides that, integer octagonal constraints can be used for representing and solving many integer problems in the field of constraint programming, such as temporal reasoning and scheduling [13]. When (integer or rational) octagonal constraints are used to build abstract domains the most critical operation is closure by entailment.^{1} This is the procedure whereby a set of octagonal constraints is augmented with (a finite representation of) all the octagonal constraints that can be inferred from it. The closure algorithms for rational octagonal constraints are sound but not complete for integer octagonal constraints. The latter require so-called tight closure algorithms that fully exploit the integrality of the variables.

In this paper, we address —providing the proofs of all the stated results— several issues that revolve around the closure by entailment operation: its interaction with the widening operators that ensure fixpoint computations terminate after a reasonable number of iterations; its efficient computation, both on rational and integer domain; its correct realization when floating point numbers are used for the implementation.

1 In contrast, in constraint programming, satisfiability check is the crucial operation.

1.1 Closure by Entailment and Widening Operators

For the abstract domain of convex polyhedra, all the widenings that have been proposed are variations of, and/or improvements to, what is commonly referred to as the standard widening [2,19]. This is based on the general widening principle “drop the unstable components” applied to constraints. Not surprisingly, most proposals for widening operators for the weakly relational domains are based on the same principle and analogous to the standard widening. For instance, for the domain of difference bound matrices mentioned above, an operator meant to match the standard widening is given in [7]. Unfortunately, as pointed out by A. Miné in [6,8] and also in his PhD thesis [18], this operator is not a widening, since it has no convergence guarantee. The reason is that closure by entailment, which is systematically performed so as to provide a canonical form for the elements and to improve the precision of several domain operations, has a negative interaction with the extrapolation operator of [7] that compromises the convergence guarantee. Intuitively, what can happen is that, while the extrapolation operator discards unstable constraints, the closure operation reinserts them (because they were redundant): failure to drop such unstable constraints can (and, in practice, quite often does) result in infinite upward iteration sequences. For this reason, it is proposed in [6,8,18] to apply the same operator given in [7] to the “syntactic” version of the same abstract domain, that is, where closure is only very carefully applied during the fixpoint computations.

We have taken a different approach and resolve the apparent conflict by considering a “semantic” abstract domain whose elements are the geometric shapes themselves. Since closure by entailment preserves the geometric shapes (even though it does not preserve their syntactic expressions), the approach is immune from the divergence problem described above. On the other hand, in order to use the standard widening as the basis of the proposed widening, it is important that we can compute reduced representations of the domain elements that encode non-redundant systems of constraints. Thus the implementations of any new widenings based on the semantic approach will need effective reduction procedures for the considered constraint description: here we provide such an algorithm for the domain of rational and integer octagonal shapes.

1.2 Computing the Closure by Entailment

Building upon the theoretical work required to verifying the correctness of the reduction algorithms mentioned above, we show that the algorithm for computing the strong closure of rational octagonal graphs as described in [6] can be simplified with a consequential improvement in its efficiency.

We also show that this result can be extended so as to apply to integer octagonal constraints. This enables us to present and fully justify an O(n^{3}) algorithm to compute the tight closure of a set of UTVPI integer constraints. In particular, this is the first time that an algorithm achieving such a complexity bound is provided with a proof of correctness.

Finally, we illustrate what happens when floating point numbers are used to implement the rational coefficients of weakly relational abstract domains.

1.3 Plan of the Paper

This paper which combines, improves and extends the work presented in [20,21] and [22], is structured as follows: Section 2 recalls the required concepts and notations; Section 3 presents domains based on bounded differences and the solution of wideningclosure conflict on these, simpler numerical abstractions; Section 4 extends such results to domains based on rational octagonal constraints; Section 5 presents the improved algorithm for computing closure by entailment of a system of rational octagonal constraints; Section 6 generalizes the algorithms for closure and reduction to the case of integer octagonal constraints; floating point computations are discussed in Section 7; related work is presented in Section 8; and Section 9 concludes.

2 Preliminaries

The reader is assumed to be familiar with the fundamental concepts of lattice theory [23] and abstract interpretation theory [24,25]. We recall here the definition of widening operator, providing a general mechanism for enforcing or accelerating termination of an abstract interpretation. In its simplest form, a widening operator on a poset ⟨P, ⊑⟩ is a partial function ∇: P × P ↣ P satisfying:

1. for all x, y ∈ P, if x ∇ y is defined then x ⊑ x ∇ y and y ⊑ x ∇ y;

2. for all increasing chains y_{0} ⊑ y_{1} ⊑ ⋯, if the increasing chain x_{0} := y_{0} and x_{i+1} := x_{i} ∇ y_{i+1} is defined for all i ∈ ℕ, then it is not strictly increasing.

We refer the reader to the classical works on the numeric domains of intervals [1] and convex polyhedra [2] for the specification of the corresponding widening operators.

Let ℚ_{∞} := ℚ ∪ {+∞} be totally ordered by the extension of ‘<’ such that d < +∞ for each d ∈ ℚ. A rational-weighted directed graph (graph, for short) G in the finite set of nodes 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 G is a non-empty and finite sequence of nodes such that (n_{i−1}, n_{i}) is an arc of G, for all i = 1, …, p. Each node n_{i} where i = 0, …, p and each arc (n_{i−1}, n_{i}) where i = 1, …, p is said to be in the path π. The length of the path π is the number p of occurrences of arcs in π and denoted by ∥π∥; the weight of the path π is ∑_{i=1}^{p} w(n_{i−1}, n_{i}) and denoted by w(π). 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, n_{0} = n_{p} and p ≥ 2; it is a zero-cycle if it is a proper cycle and w(π) = 0. A graph is zero-cycle free if it has no zero-cycles. If π_{1} = n_{0} ⋯ n_{h} and π_{2} = n_{h} ⋯ n_{p} are paths, 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.

A graph (N , w) can be interpreted as the system of potential constraints

C := { n_{i} − n_{j} ≤ w(n_{i}, n_{j}) | n_{i}, n_{j} ∈ N }.

The graph (N , w) is consistent if and only if the system of constraints it represents is satisfiable in ℚ, i.e., there exists a rational valuation ρ: N → ℚ such that, for each constraint (n_{i} −n_{j} ≤ d) ∈ C, the relation ρ(n_{i})−ρ(n_{j}) ≤ d holds. It is well-known that a graph is consistent if and only if it has no negative weight cycles (see [26, Section 25.5] and [27]).

The set of consistent graphs in N is denoted by 𝔾. This set 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. A graph G′ = (N , w′) is a subgraph of G = (N , w) if, for all i, j ∈ N, we have w′(i, j) = w(i, j) or w′(i, j) = +∞; the subgraph is proper if G′ ≠ G. If G′ is a subgraph of G, then G ⊴ G′ (the converse does not necessarily hold).

Definition 1 (Closed graph.) A consistent graph G = (N , w) is closed if the following properties hold:

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

The (shortest-path) closure of a consistent graph G in N is

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

Although the lattice of rational graphs is not complete, it will include all the infinite least upper bounds defining the closures of rational graphs. Informally, this must hold since the weights of closure(G) must be linear combinations of the rational weights of G and hence are also rational.

When trivially extended so as to behave as the identity function on the bottom element ⊥, shortest-path closure is a kernel operator (monotonic, idempotent and reductive) on the lattice 𝔾_{⊥}, therefore providing a canonical form.

3 Bounded Difference Graphs and Shapes

The typical way to simplify the domain of convex polyhedra is by restricting attention to particular subclasses of linear inequalities. One possibility, which has a long tradition in computer science [28], is to only consider potential constraints, also known as bounded differences: these are restricted to take the form v_{i} − v_{j} ≤ d or ±v_{i} ≤ d, where d is a constant. Systems of bounded differences have been used by the artificial intelligence community as a way to reason about temporal quantities [29,30], as well as by the model checking community as an efficient yet precise way to model and propagate timing requirements during the verification of various kinds of concurrent systems [31, 32]. In the abstract interpretation field, the idea of using an abstract domain of bounded differences was put forward in [3].

3.1 Bounded Difference Graphs

A finite system C of bounded differences on variables V = {v_{0}, …, v_{n−1}} can be represented by a weighted directed graph G = (N_{0}, w) where N_{0} = {0} ∪ V, 0 ∉ V is the special variable, and the weight function w is defined, for each v_{i}, v_{j} ∈ N_{0}, by

w(v_{i}, v_{j}) := \begin{cases}min\{ d ∈ ℚ | (v_{i} − v_{j} ≤ d) ∈ C \}, & if v_{i} ≠ 0 and v_{j} ≠ 0; \\ min\{ d ∈ ℚ | (v_{i} ≤ d) ∈ C \}, & if v_{i} ≠ 0 and v_{j} = 0; \\ min\{ d ∈ ℚ | (−v_{j} ≤ d) ∈ C \}, & if v_{i} = 0 and v_{j} ≠ 0; \\ 0, & if v_{i} = v_{j} = 0. \end{cases}

Notice that we assume that min ∅ = +∞; moreover, unary constraints are encoded by means of the special variable, which is meant to always have value 0. A possible representation of (the weight function of) the graph G is by means of a matrix-like data structure called Difference-Bound Matrix (DBM) [28]. However, this representation provides no conceptual advantage over the isomorphic graph (or constraint network [30]) representation. For this reason we will consistently adopt the terminology and notation introduced in Section 2 for weighted directed graphs. In particular, a graph encoding a consistent system of bounded differences will be called a Bounded Difference Graph (BDG).

The first fully developed application of bounded differences in the field of abstract interpretation can be found in [7], where an abstract domain of closed BDGs is defined. In this case, the shortest-path closure requirement was meant as a simple and well understood way to obtain a canonical form for the domain elements by abstracting away from the syntactic details; basically, it corresponds to the closure by entailment of the encoded system of bounded differences with respect to the transitivity inference rule:

{i − k ≤ d_{1}  k − j ≤ d_{2} \atop i − j ≤ d_{1} + d_{2}}  (3)

In [7] the specification of all the required abstract semantics operators is provided, including an operator that is meant to match the widening operators defined on more classical numeric domains. This operator can be interpreted either as a generalization for closed BDGs of the widening operator defined on the abstract domain of intervals [1], or as a restriction on the domain of closed BDGs of the standard widening defined on the abstract domain of convex polyhedra [2,19]: its implementation is based on the following upper bound operator on the set of consistent graph representations.

Definition 2 (Widening graphs.) Let G_{1} = (N , w_{1}) and G_{2} = (N , w_{2}) be consistent graphs. Then G_{1}∇G_{2} := (N , w), where the weight function w is defined, for each i, j ∈ N, by

w(i, j) := \begin{cases}w_{1}(i, j), & if w_{1}(i, j) ≥ w_{2}(i, j); \\ +∞, & otherwise. \end{cases}

Unfortunately, as pointed out in [6,8], when used in conjunction with shortest-path closure, this extrapolation operator does not provide a convergence guarantee for fixpoint computations, hence it is not a widening. The reason is that, whereas the closure operation adds redundant constraints to the input BDG, a key requirement in the specification of the standard widening is that the first argument polyhedron must be described by a non-redundant system of constraints.^{2} Thus we have a “conflict of interest” between the use of a convenient canonical form for the abstract domain —a form that also allows for increased precision of several domain operations— and the requirements of the widening.

The abstract domain of BDGs has been reconsidered in [6]. Differently from [7], in [6] BDGs are not required to be closed. In this more concrete, syntactic domain, the shortest-path closure operator maps each domain element into the smallest BDG encoding the same geometric shape. Closure is typically used as a preprocessing step before the application of most, though not all, of the abstract semantic operators, allowing for improved accuracy in the results of the abstract computation. The same widening operator proposed in [7] is also used in [6]; however, it is observed that this widening “could have intriguing interactions” with shortest-path closure, therefore identifying the divergence issue faced in [7]. This observation led the author of [6] to the adoption of the syntactic domain of BDGs, where closure is not enforced.

3.2 Bounded Difference Shapes

While the analysis of the divergence problem is absolutely correct, the solution identified in [6] is sub-optimal since, as is usually the case, resorting to a syntactic domain (such as the one of BDGs) has a number of negative consequences, some of which will be recalled in Section 3.4.

To identify a simpler, more natural solution, we first have to acknowledge that an element of our abstract domain should be a geometric shape, rather than (any) one of its graph representations. To stress this concept, such an element will be called a Bounded Difference Shape (BDS). A BDS corresponds to the equivalence class of all the BDGs representing it. The implementation of the abstract domain can freely choose between these possible representations, switching at will from one to the other, as long as the semantic operators are implemented as expected. Notice that, in such a context, the shortest-path closure operator is just a transparent implementation detail: on the abstract domain of BDSs it corresponds to the identity function.

The other step towards the solution of the divergence problem is the simple observation that a BDS is a convex polyhedron and the set of all BDSs is closed under the application of the standard widening on convex polyhedra. Thus, no divergence problem can be incurred when applying the standard widening to an increasing sequence of BDSs. As mentioned in Section 3.1, a crucial requirement in the specification of the standard widening is that the first argument polyhedron is described by a nonredundant system of constraints [33]. Thus it is not surprising that using closed BDGs has problems since it is very likely that they will encode redundant constraints. By contrast, we propose to select, in the equivalence class of BDGs representing the same geometric shape, a BDG which is maximal with respect to the graph lattice ordering ‘⊴’, since such a graph encodes no redundant constraints at all.

Definition 3 (Reduced graph.) A consistent graph G_{1} is reduced if, for each consistent graph G_{2} ≠ G_{1} such that G_{1}⊴G_{2}, we have closure(G_{1}) ≠ closure(G_{2}). A reduction for the consistent graph G is any reduced graph G_{r} such that closure(G) = closure(G_{r}).

2 This requirement was sometimes neglected in recent papers describing the standard widening on convex polyhedra; it was recently recalled and exemplified in [33]. Note that a similar requirement is implicitly present even in the specification of the widening on intervals.

Hence, a graph is reduced if it is maximal in the subset of graphs having the same shortest-path closure. In order to provide a correct and reasonably efficient implementation of the standard widening on the domain of BDSs, all we need is a reduction procedure mapping a BDG representation into (any) one of the equivalent reduced graphs. Such an algorithm was defined in [32] and called shortest-path reduction. Basically, it is an extension of the transitive reduction algorithm of [34] to the case of weighted directed graphs. Note that, since each equivalence class may have many maximal elements, shortest-path reduction is not a properly defined operator on the domain of BDGs. However, the shortest-path reduction algorithm of [32] provides a canonical form as soon as we fix a total order for the nodes in the graph.

In summary, the solution to the divergence problem for BDSs is to apply the operator specified in Definition 2 to a reduced BDG representation of the first argument of the widening. From the point of view of the user, this will be a transparent implementation detail: on the domain of BDSs, shortest-path reduction is the identity function, as was the case for shortest-path closure.

3.3 On the Precision of the Standard Widening

The standard widening on BDSs could result, if used with no precautions, in poorer precision with respect to its counterpart defined on the syntactic domain of BDGs. For increased precision, the specification of [6] prescribes two conditions that the abstract iteration sequence must satisfy:

1. the second argument of the widening should be represented by a closed BDG (note that, in this case, no divergence problem can arise);

2. the first BDG of the abstract iteration sequence G_{0} ⊴ G_{1} ⊴ … ⊴ G_{i} ⊴ … should be closed too.

The effects of both improvements can be obtained also with the semantic domain of BDSs. As for the first one, this can be applied as is, leading to an implementation where the two arguments of the widening are represented by a reduced BDG and a closed BDG, respectively. The result of such a widening operator will depend on the specific reduced form computed for the first argument. The second precision improvement can be achieved by applying the well-known ‘widening up to’ technique defined in [35,36] or its variation called ‘staged widening with thresholds’ [37–39]: in practice, it is sufficient to add to the set of ‘up to’ thresholds all the constraints of the shortest-path closure of the first BDG G_{0}. Further precision improvements can be obtained by applying any delay strategy and/or the framework defined in [33].

3.4 Syntactic vs. Semantic Abstract Domains

In this section we have shown that when considering weakly-relational numeric abstractions, besides the syntactic domains of constraint systems, it is possible to define the semantic domains of the corresponding geometric shapes. To avoid misunderstandings, it is worth stressing that both kinds of abstract domain are well defined and may be safely adopted for the implementation of a static analysis application. Nonetheless, it can be argued that using a semantic abstract domain provides several advantages. Some of the advantages were already pointed out in [6, Section 5] where the domain of BDGs is compared to the domain of closed BDGs.^{3} For instance, it is noted that the domain of closed BDGs allows for the specification of a nicer, injective meaning function; also, the least upper bound operator on BDGs is not the most precise approximation of the union of two geometric shapes. In summary, the discussion in [6, Section 5] makes clear that the solution to the divergence problem for the abstract iteration sequence was the main motivation for adopting a syntactic domain.

One disadvantage of syntactic abstract domains concerns the user-level interfaces of the corresponding software implementations. Namely, the user of a syntactic abstract domain (e.g., the developer of a specific static analysis application using this domain) has to be aware of many details that, in principle, should be hidden by the implementation. As an example, consider the shortest-path closure and reduction procedures for BDGs, which the user might rightfully see as semantics-preserving operations. As a matter of fact, for the syntactic domain of BDGs, these are not semantics-preserving: their application affects both the precision and the convergence of the abstract iteration. In such a situation, the documentation of the abstract domain software needs to include several warnings about the correct usage of these operators, so as to avoid possible pitfalls. In contrast, when adopting the semantic domain of BDSs, both the closure and reduction operators may be excluded from the public interface while the implementation can apply them where and when needed or appropriate. Such an approach is systematically pursued in the implementation of the Parma Polyhedra Library [40].

Another potential drawback of the adoption of a syntactic abstract domain can be found in the application of domain refinement operators. As an example, consider the application of the finite powerset operator [41] to the domains of BDGs and BDSs, so as to obtain two abstract domains that are able to represent finite disjunctions of the corresponding abstract elements. In both cases, by providing the widenings on BDGs and BDSs with appropriate finite convergence certificates [41], it will be possible to lift them to corresponding widenings on the powerset domains. However, when upgrading the syntactic domain, avoidable redundancies will be incurred, since different disjuncts inside a domain element may represent the same geometric shape; furthermore, these “duplicates” cannot be systematically removed, since by doing so we could change the value of the finite convergence certificate of the powerset element, possibly breaking the convergence guarantee of the lifted widening. As a consequence, both efficiency and precision are potentially degraded. In summary, the disadvantages of syntactic domains are amplified when applying domain refinements.

4 Rational Octagonal Graphs and Shapes

From a theoretical point of view, the observations made in the previous section are immediately applicable to any other weakly-relational numeric domain whose elements are convex polyhedra and is closed with respect to the application of the standard widening, therefore including the domains proposed in [8–11]. From a practical perspective, the success of such a construction depends on the availability of a reasonably efficient reduction procedure for the considered subclass of constraints, because algorithms for minimizing arbitrary linear inequality constraints are not efficient enough. In this section we provide such a reduction procedure for the octagon abstract domain [8].

3 Similar observations, tailored to the case of octagons, are also in [8, Section VII].

We assume in the following that there is a fixed set V = {v_{0}, …, v_{n−1}} of n variables. The octagon abstract domain allows for the manipulation of octagonal constraints of the form av_{i} + bv_{j} ≤ d, where a, b ∈ {−1, 0, +1}, a ≠ 0, v_{i}, v_{j} ∈ V, v_{i} ≠ v_{j} and d ∈ ℚ (the same class of constraints was considered in [15], where octagons were called simple sections). Octagonal constraints can be encoded using potential constraints by splitting each variable v_{i} into two forms: a positive form v_{i}^{+}, interpreted as +v_{i}; and a negative form v_{i}^{−}, interpreted as −v_{i}. Then any octagonal constraint av_{i} + bv_{j} ≤ d can be written as a potential constraint v − v′ ≤ d_{0} where v, v′ ∈ {v_{i}^{+}, v_{i}^{−}, v_{j}^{+}, v_{j}^{−}} and d_{0} ∈ ℚ. Namely, an octagonal constraint such as v_{i} + v_{j} ≤ d can be translated into the potential constraint v_{i}^{+} − v_{j}^{−} ≤ d; alternatively, the same octagonal constraint can be translated into v_{j}^{+} − v_{i}^{−} ≤ d. Furthermore, unary (octagonal) constraints such as v_{i} ≤ d and −v_{i} ≤ d can be encoded as v_{i}^{+} − v_{i}^{−} ≤ 2d and v_{i}^{−} − v_{i}^{+} ≤ 2d, respectively, so that the special variable 0 is no longer needed.

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 variables in V: for all i ∈ N^{±}, if i = 2k, then i represents the positive form v_{k}^{+} and, if i = 2k + 1, then i represents the negative form v_{k}^{−} of the variable v_{k}. To simplify the presentation, for each i ∈ N^{±}, 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. Then we can rewrite a potential constraint v − v′ ≤ d where v ∈ {v_{k}^{+}, v_{k}^{−}} and v′ ∈ {v_{l}^{+}, v_{l}^{−}} as the potential constraint i − j ≤ d in N^{±} where, if v = v_{k}^{+}, i = 2k and if v = v_{k}^{−}, i = 2k + 1; similarly, if v′ = v_{l}^{+}, j = 2l and if v′ = v_{l}^{−}, j = 2l + 1.

It follows that any finite system of octagonal constraints on V, translated into a set of potential constraints in N^{±} as above, can be encoded by a graph G in N^{±}. In particular, any 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 4 (Octagonal graph.) An octagonal graph in N^{±} is any consistent graph G = (N^{±}, w) satisfying the coherence assumption:

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

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. This also implies that an octagonal constraint such as v_{i} + v_{j} ≤ d will always be translated into both v_{i}^{+} − v_{j}^{−} ≤ d and v_{j}^{+} − v_{i}^{−} ≤ d.

The octagon abstract domain developed in [8] is thus a syntactic domain having octagonal graphs as elements. When dealing with octagonal graphs, observe that the coherence assumption links the positive and negative forms of variables. A closure by entailment procedure, besides classical transitivity as encoded by the explicit paths in the graph, should also consider the following strengthening inference rule:

{i − \overline{ı} ≤ d_{1}  \overline{ȷ} − j ≤ d_{2} \atop 2(i − j) ≤ d_{1} + d_{2}}  (5)

Thus shortest-path closure for consistent graphs does not provide a canonical form for octagonal graphs; to this end, strong closure, first defined in [8], is used instead.

Definition 5 (Strongly closed graph.) 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}.

When trivially extended with a bottom element, strong closure is a kernel operator on the lattice of octagonal graphs.

4.1 A Strong Reduction Procedure for Octagonal Graphs

By repeating the reasoning motivating the bounded difference shapes, we define the semantic abstract domain of octagonal shapes, whose elements are equivalence classes of octagonal graphs representing the same geometric shape. Hence, strong closure maps an octagonal graph representation of a non-empty octagonal shape into the minimum element of the corresponding equivalence class. The dual procedure, mapping the octagonal graph into (any) one of the maximal elements in its equivalence class, is called strong reduction.

Definition 6 (Strongly reduced graph.) An octagonal graph G_{1} is strongly reduced if, for each octagonal graph G_{2} ≠ G_{1} such that G_{1}⊴G_{2}, S-closure(G_{1}) ≠ S-closure(G_{2}). A strong reduction for the octagonal graph G is any strongly reduced octagonal graph G_{R} such that S-closure(G) = S-closure(G_{R}).

In the above definition, we only compare G_{1} with other octagonal graphs G_{2} ∈ 𝕆, thereby disregarding those trivial redundancies that are due to the coherence assumption. This is not a real problem because, as discussed before, any reasonable implementation will automatically and efficiently filter away this kind of redundancies.

We now generalize the shortest-path reduction algorithm of [32] so as to obtain a strong reduction procedure for octagonal graphs. Clearly, the algorithm of [32] cannot be used without modifications, since it takes no account of the redundancies caused by the strengthening inference rule (5). Nonetheless, the high-level structure of the strong reduction procedure is the same as that defined in [32] for shortest-path reduction:

1. compute the closure by entailment of the constraint graph;

2. partition the nodes into equivalence classes based on equality constraints;

3. decompose the graph so as to separate those arcs that link different equivalence classes (encoding only inequalities) from the partition information (encoding the equivalence classes themselves, i.e., all the equalities);

4. reduce the subgraph that gives constraints on different equivalence classes; 5. reduce the partition information;

6. merge the results of steps 4 and 5 to obtain the reduced constraint graph.

We now describe each of the above steps, formally stating the correctness of the overall procedure.

Step 1 of the algorithm can be performed by applying any strong closure procedure, e.g., the one originally defined in [8] or the more efficient one given in Section 5.

Step 2 is also easily implemented by observing that, in a strongly closed octagonal graph, equality constraints correspond to zero-cycles having length two.

Definition 7 (Zero-equivalence.) Let G = (N^{±}, w) be a strongly closed octagonal graph. The nodes i, j ∈ N^{±} are zero-equivalent in G, denoted i ≡_{G} j, if and only if w(i, j) = −w(j, i).

While step 6 carries over from BDGs to octagonal graphs, the formal definition of steps 3–5 of the reduction algorithm is more difficult for octagonal graphs than it was for BDGs, as it requires some understanding of the structure of the zero-equivalence classes. As a first observation, note that i ≡_{G} j if and only if \overline{ı} ≡_{G} \overline{ȷ}, so that we have the following lemma.

Lemma 1 Let G = (N^{±}, w) be a strongly closed octagonal graph and E ⊆ N^{±} a zeroequivalence class for G. Then \overline{E} := \{ \overline{ı} ∈ N^{±} | i ∈ E \} is also a zero-equivalence class for G.

Let G be a strongly closed octagonal graph and, for a zero-equivalence class E of G, let \overline{E} be defined as in Lemma 1. Then we say that E is non-singular if E ∩ \overline{E} = ∅ and singular if E = \overline{E}.

Lemma 2 Let G = (N^{±}, w) be a strongly closed octagonal graph. Then there is at most one singular zero-equivalence class for G.

If it exists, the singular zero-equivalence class encodes all the unary equality constraints.^{4} In contrast, all the other (non-singular) zero-equivalence classes can only encode binary equality constraints.

We associate to each zero-equivalence class E ⊆ N^{±} a leader ℓ_{E} := min E; the class having the leader in positive (resp., negative) form will be said to be a positive (resp., negative) zero-equivalence class. Note that, this means that the singular zeroequivalence class, if present, is always positive and, for non-singular zero-equivalence classes E and \overline{E}, we have ℓ\overline{E} = \overline{ℓ}_{E}.

We are now ready to provide a formal specification for step 3 of the strong reduction algorithm. As was the case in [32], the first subgraph resulting from the decomposition, relating nodes in different zero-equivalence classes, is obtained by only connecting the leaders; however, the leader of the singular zero-equivalence class should not be connected to the other leaders. The second subgraph only encodes those constraints relating nodes in the same zero-equivalence class.

Definition 8 (Non-singular leaders and zero-equivalence subgraphs.) Assume G = (N^{±}, w) is a strongly closed octagonal graph and L ⊆ N^{±} is the set of leaders of the non-singular zero-equivalence classes for G. The non-singular leaders’ subgraph of G is the graph L = (N^{±}, w_{L}), where the weight function w_{L} is defined, for each i, j ∈ N^{±}, by

4 When computing a reduced BDG, such a singular zero-equivalence class is always present:

it is the zero-equivalence class containing the special variable 0.

w_{L}(i, j) := \begin{cases}w(i, j), & if i = j or \{i, j\} ⊆ L; \\ +∞, & otherwise. \end{cases}

The zero-equivalence subgraph of G is the graph E = (N^{±}, w_{E}), where the weight function w_{E} is defined, for each i, j ∈ N^{±}, by

w_{E}(i, j) := \begin{cases}w(i, j), & if i ≡_{G} j; \\ +∞, & otherwise. \end{cases}

The following result states that the two subgraphs are still strongly closed and the non-singular leaders’ subgraph encodes no equality constraints, therefore describing a fully dimensional octagonal shape.

Lemma 3 Let L and E be the non-singular leaders’ subgraph and the zero-equivalence subgraph of the strongly closed octagonal graph G, respectively. Then, L and E are strongly closed octagonal graphs and L is zero-cycle free.

Step 4 of the strong reduction algorithm is implemented by checking, for each proper arc in the non-singular leaders’ subgraph, whether it can be obtained from the other arcs by a single application of the constraint inference rules. Once again, note that we disregard redundancies caused by the coherence assumption.

Definition 9 (Strongly atomic arc and subgraph.) Let G = (N^{±}, w) be an octagonal graph. An arc (i, j) of G is atomic if it is proper and, for all k ∈ N^{±} \ {i, j}, w(i, j) < w(i, k) + w(k, j). The arc (i, j) is strongly atomic if it is atomic and either i = \overline{ȷ} or 2w(i, j) < w(i, \overline{ı}) + w(\overline{ȷ}, j).

The strongly atomic subgraph of G is the graph A = (N^{±}, w_{A}) where the weight function w_{A} is defined, for all i, j ∈ N^{±}, by

w_{A}(i, j) = \begin{cases}w(i, j), & if (i, j) is strongly atomic in G; \\ +∞, & otherwise. \end{cases}

The implementation of step 5 of the algorithm, i.e., the strong reduction of the zeroequivalence subgraph, is performed by reducing each zero-equivalence class in isolation. Once again, we exploit the total ordering defined on N^{±}.

The strong reduction for a positive non-singular zero-equivalence class E follows that of [32]: it creates a single zero-cycle connecting all nodes in E following their total ordering, where the weights of the component arcs are as in the strong closure of the graph. By the coherence assumption, the nodes in the corresponding negative zeroequivalence class \overline{E} are automatically connected in the opposite order. Figure 1 shows the arcs in the strong reduction of both E and \overline{E}, where E = \{z_{0}, …, z_{m}\} is the positive class and where z_{0} < ⋯ < z_{m}. The strong reduction for a singular zero-equivalence class E is similar except that there is now a single zero-cycle connecting all the positive and negative nodes in E. Figure 2 shows the strong reduction for the singular zeroequivalence class E = \{z_{0}, \overline{z}_{0}, …, z_{m}, \overline{z}_{m}\}, where z_{0} < \overline{z}_{0} < ⋯ < z_{m} < \overline{z}_{m}. In both Figures 1 and 2, the dashed arcs are those that can be obtained from the non-dashed ones by application of the coherence assumption.

The following definition formalizes the above observations.

\begin{matrix}E & z_{0} & z_{1} & … & z_{m} \\ \overline{E} & ^{\overline{z}_{0}} & ^{\overline{z}_{1}} & … & ^{\overline{z}_{m}} \end{matrix}

Fig. 1 Strong reduction for non-singular zero-equivalence classes

E  z_{0}  z_{1}  …  z_{m}^{\overline{z}_{0}}  ^{\overline{z}_{1}}  …  ^{\overline{z}_{m}}

Fig. 2 Strong reduction for the singular zero-equivalence class

Definition 10 (Zero-equivalence reduction.) Let G = (N^{±}, w) be a strongly closed octagonal graph and let w′ be the weight function defined, for all i, j ∈ N^{±}, as follows: if i, j ∈ E for some positive zero-equivalence class E of G and

– if E = {z_{0}, …, z_{m}} is non-singular, assuming z_{0} < ⋯ < z_{m},

w′(i, j) := \begin{cases}w(i, j), & if i = z_{h−1}, j = z_{h}, for some h = 1 …, m; \\ w(i, j), & if i = z_{m}, j = z_{0} and m > 0; \\ +∞, & otherwise; \end{cases}

– if E = \{z_{0}, \overline{z}_{0}, …, z_{m}, \overline{z}_{m}\} is singular, assuming z_{0} < \overline{z}_{0} < ⋯ < z_{m} < \overline{z}_{m},

w′(i, j) := \begin{cases}w(i, j), & if i = z_{h−1}, j = z_{h}, for some h = 1 …, m; \\ w(i, j), & if i = \overline{z}_{0}, j = z_{0} or i = z_{m}, j = \overline{z}_{m}; \\ +∞, & otherwise; \end{cases}

and w′(i, j) := +∞, otherwise. Then, the zero-equivalence reduction for G is the octagonal graph Z = (N^{±}, w_{Z}), where, for each i, j ∈ N^{±},

w_{Z}(i, j) := min\{w′(i, j), w′(\overline{ȷ}, \overline{ı})\}.

The final step 6 of the strong reduction algorithm is implemented by computing the greatest lower bound A ⊓ Z, where A is the strongly atomic subgraph of L and Z is the zero-equivalent reduction of E, as obtained at steps 4 and 5 of the algorithm.

Theorem 1 Given an octagonal graph G, the strong reduction algorithm computes a strong reduction for G.

If n is the cardinality of the original set V of variables, then steps 1 and 4 of the algorithm have worst-case complexity in O(n^{3}), while all the others steps are in O(n^{2}). Thus, the overall procedure has cubic complexity. As was the case for the reduction procedure of [32], once the ordering of variables is fixed, the strong reduction algorithm returns a canonical form for octagonal graphs.

4.2 A Semantic Widening for Octagonal Shapes

A correct implementation of the standard widening on octagonal shapes is obtained by computing any strong reduction of the octagonal graph representing the first argument. As in the case of BDSs, for maximum precision the strongly closed representation for the second argument should be computed. Even better, by adopting the following variant, we obtain a “truly semantic” widening for the domain of octagonal shapes.

Definition 11 (Widening octagonal shapes.) Let S_{1}, S_{2} ∈ ℘(ℝ^{n}), where ∅ ≠ S_{1} ⊆ S_{2}, be two octagonal shapes represented by the strongly reduced octagonal graph G_{1} and the strongly closed octagonal graph G_{2}, respectively. Let also S ∈ ℘(ℝ^{n}) be the octagonal shape represented by the octagonal graph G_{1} ∇ G_{2}. Let dim(T) denote the affine dimension of shape T. Then we define

S_{1} ∇ S_{2} := \begin{cases}S_{2}, & if dim(S_{1}) < dim(S_{2}); \\ S, & otherwise. \end{cases}

By refraining from applying the graph-based widening when the affine dimension of the geometric shapes is increasing, the operator becomes independent from the specific strongly reduced form computed, i.e., from the total ordering defined on the nodes of the graphs. Also note that the test dim(S_{1}) < dim(S_{2}) can be efficiently decided by checking whether the nodes of the two octagonal graphs are partitioned into different collections of zero-equivalence classes.

Theorem 2 The operator ‘∇’ of Definition 11 is a proper widening on the domain of octagonal shapes. Let ‘∇_{s}’ be the standard widening on the domain of convex polyhedra, as defined in [19]. Then, for all octagonal shapes S_{1}, S_{2} ∈ ℝ^{n} such that ∅ ≠ S_{1} ⊆ S_{2}, we have S_{1} ∇ S_{2} ⊆ S_{1} ∇_{s} S_{2}.

Observe that, in the typical static analysis computation pattern, the result of a widening computed for one iteration will be used as the first input argument for the widening step in the subsequent iteration. By Definition 11, such an input argument will already be either strongly closed or strongly reduced (because the graph widening operator of Definition 2 preserves strong reduction); hence, the full computational cost of strong reduction will be incurred less frequently than expected.

A semantic widening for BDSs enjoying a result similar to Theorem 2 can be obtained by replacing, in Definition 11, the strongly reduced and strongly closed octagonal graph representations by the reduced and closed BDG representations, respectively.

5 An Improved Strong Closure Procedure for Octagonal Graphs

The strong closure algorithm defined in [8,18], whose pseudo-code is reported in Figure 3, performs n local propagation steps, where n is the dimension of the vector space.

function Q consistent(var w [0 . . 2n − 1] [0 . . 2n − 1]) : bool

for i := 0 to 2n − 1 do if w[i, i] < 0 return false; else w[i, i] := 0;

return true; end function

procedure strengthening(var w [0 . . 2n − 1] [0 . . 2n − 1])

for i := 0 to 2n − 1 do

for j := 0 to 2n − 1 do
w[i, j] := min(w[i, j], (w[i, \overline{ı}] + w[\overline{ȷ}, j])/2);

end procedure

function strong closure(var w [0 . . 2n − 1] [0 . . 2n − 1]) : bool

for k := 0 to 2n − 2 step 2 do { Modified Floyd-Warshall: n steps } for i := 0 to 2n − 1 do

for j := 0 to 2n − 1 do

w[i, j] := min(w[i, j], w[i, k] + w[k, j], w[i, \overline{k}] + w[\overline{k}, j], w[i, k] + w[k, \overline{k}] + w[\overline{k}, j], w[i, \overline{k}] + w[\overline{k}, k] + w[k, j]);

{ Strengthening: n steps }

strengthening(w); return Q consistent(w);

end function

Fig. 3 The strong closure algorithm proposed in [8,18] for rational octagonal graphs

In each of these steps, a rather involved variant of the constraint propagation for transitivity as found in the Floyd-Warshall algorithm is followed by another constraint propagation for strengthening, corresponding to the new inference rule (5).

A naive implementation of the algorithm in Figure 3 would perform 48n^{3} coefficient operations (the number of operations is obtained by summing the number of coefficient additions and the number of coefficient comparisons implementing the computation of the minima, whose realization typically requires a coefficient subtraction; we disregard simpler operations, such as zero initialization, division by the constant 2 and comparison with the constant 0, which are also less frequent). Several optimizations can be applied: for instance, some invariant computations can be moved out of the body of the inner loop; more importantly, the number of iterations can be lowered by resorting to an appropriate data structure [18, Section 4.5.1] recording the weight function w, here denoted to be similar to a two-dimensional array, so that it automatically implements the coherence assumption for octagonal graphs (i.e., property (4) of Definition 4). In particular, the finely tuned implementation that can be found in [42], performs 20n^{3} + 24n^{2} coefficient operations. Nonetheless, a significant efficiency improvement,

function shortest path closure(var w [0 . . 2n − 1] [0 . . 2n − 1]) : bool { Classical Floyd-Warshall } for k := 0 to 2n − 1 do

for i := 0 to 2n − 1 do
for j := 0 to 2n − 1 do
w[i, j] := min(w[i, j], w[i, k] + w[k, j]);

return Q consistent(w); end function

function strong closure(var w [0 . . 2n − 1] [0 . . 2n − 1]) : bool if not shortest path closure(w) return false; strengthening(w); return true;

end function

Fig. 4 An improved strong closure algorithm for rational octagonal graphs

which is probably beyond any hand crafted and/or compiler assisted optimization of the algorithm in Figure 3, can be obtained thanks to the following theorem.

Theorem 3 Let G = (N^{±}, w) be a closed octagonal graph. Consider the graph G_{S} = (N^{±}, w_{S}), where w_{S} is defined, for each i, j ∈ N^{±}, by

w_{S}(i, j) := min\{w(i, j), \frac{w(i, \overline{ı})}{2} + \frac{w(\overline{ȷ}, j)}{2} \}.

Then G_{S} = S-closure(G).

Intuitively, the theorem states that strong closure can be obtained by application of any shortest-path closure algorithm followed by a single strengthening step, leading to a much simpler implementation.

Figure 4 shows an improved strong closure algorithm based on Theorem 3 and on the classical Floyd-Warshall shortest-path closure algorithm. Here too the pseudo-code relies on a data structure that automatically implements the coherence assumption. The naive implementation of this new algorithm leads to the computation of 16n^{3} + 8n^{2} coefficient operations: while it is still in the O(n^{3}) complexity class, the saving with respect to the highly optimized algorithm in [42] is always above 20%.

If the case of sparse graphs is considered, then Theorem 3 allows for a further improvement to the complexity bound: to this end, it is enough to modify the code in Figure 4 so as to compute the shortest-path closure using Johnson’s algorithm [26]: the worst case complexity of such an implementation will be O(n^{2} log n + mn), which significantly improves upon the O(n^{3}) worst case complexity of the Floyd-Warshall algorithm when, e.g., m ∈ Θ(n). However, as observed elsewhere [18,43], some of the targeted applications (e.g., static analysis) typically require the computation of graphs that are dense, so that the Floyd-Warshall algorithm is often a better choice from a practical perspective.

Observe that Theorem 3 also allows for enhancements in the incremental variant of the strong closure algorithm, proposed in [18]. Once again, the improved algorithm can be obtained by any incremental version of shortest-path closure (e.g., the incremental version of the Floyd-Warshall algorithm) followed by a single strengthening step.

6 Integer Octagonal Graphs, Tight Closure and Tight Reduction

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 12 (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 that it encodes and we need to consider the following tightening inference rule:

{i − \overline{ı} ≤ d \atop i − \overline{ı} ≤ 2⌊d/2⌋}.  (7)

Definition 13 (Tightly closed graph.) 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.  (8)

The tight closure of an octagonal graph G in N^{±} is

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

It follows from Definition 13 that any tightly closed integer octagonal graph will satisfy property (8), thereby encoding a satisfiable integer constraint system, and therefore will be ℤ-consistent. Moreover, since the encoding of any satisfiable integer constraint system will result in a ℤ-consistent integer octagonal graph G that satisfies property (8), its tight closure T-closure(G) will also be ℤ-consistent. This means that, if G is not ℤ-consistent, then T-closure(G) = ⨆ ∅ = ⊥; that is, the tight closure operator computes either a tightly closed graph or the bottom element. Therefore, tight closure is a kernel operator on the lattice of octagonal graphs, as was the case for strong closure.

An incremental closure procedure for obtaining the tight closure of an octagonal graph was defined in [13] and improved in [44]. The algorithm, which is also presented and discussed in [18, Section 4.3.5], maintains the tight closure of a system of octagonal constraints by performing at most O(n^{2}) operations each time a new constraint is added: thus, for m constraints, the worst case complexity is O(mn^{2}). In particular, for the case of a dense system of octagonal constraints where m ∈ O(n^{2}), the worst case complexity is O(n^{4}).

procedure tightening(var w [0 . . 2n − 1] [0 . . 2n − 1])

for i := 0 to 2n − 1 do

w[i, \overline{ı}] := 2 · floor(w[i, \overline{ı}]/2);

end procedure

procedure tight closure if consistent(var w [0 . . 2n − 1] [0 . . 2n − 1]) shortest path closure(w); tightening(w); strengthening(w);

end procedure

Fig. 5 A O(n^{3}) tight closure algorithm for ℤ-consistent integer octagonal graphs

The following theorem shows that a more efficient tight closure algorithm can be obtained by a simple modification to the improved strong closure algorithm based on Theorem 3. Basically, the tightening inference rule (7) must be applied to ensure that property (8) holds before applying the strengthening inference rule (5).

Theorem 4 Let G = (N^{±}, w) be a closed integer octagonal graph. Consider the graph G_{T} = (N^{±}, w_{T}), where w_{T} is defined, for each i, j ∈ N^{±}, by

w_{T}(i, j) := min\{w(i, j), ⌊ \frac{w(i, \overline{ı})}{2} ⌋ + ⌊ \frac{w(\overline{ȷ}, j)}{2} ⌋\}.  (9)

Then, if G_{T} is an octagonal graph, G_{T} = T-closure(G).

Figure 5 shows the pseudo-code for a O(n^{3}) tight closure algorithm based on Theorem 4 and on the classical Floyd-Warshall shortest-path closure algorithm. As in the rational case, if the graph is sparse, a better complexity bound can be obtained by using Johnson’s algorithm [26] for shortest-path closure: the worst case complexity will again be O(n^{2} log n + mn), which improves upon the O(mn^{2}) worst case complexity of [13, 44] when m ∈ Ω(log n). In contrast, the same worst case complexity bound of [13,44] is obtained when considering the incremental variant of the tight closure algorithm.

It follows from the statement of Theorem 4 that an implementation based on it also needs to check the consistency of G_{T}. In principle, one could apply again a shortestpath closure procedure so as to check whether G_{T} contains some negative weight cycles. However, a more efficient solution can be obtained by exploiting the following result.

Theorem 5 Let G and G_{T} be as defined in Theorem 4. Consider G_{t} = (N^{±}, w_{t}) where, for each i, j ∈ N^{±},

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

and suppose that, for all i ∈ N^{±}, w_{t}(i, \overline{ı})+w_{t}(\overline{ı}, i) ≥ 0. Then G_{T} is an octagonal graph.

The combination of the results stated in Theorems 4 and 5, together with the well known result for rational consistency, leads to an O(n^{3}) tight closure algorithm, such as that given by the pseudo-code in Figure 6, that computes the tight closure of any (possibly inconsistent) coherent integer-weighted graph returning the Boolean value ‘true’ if and only if the input graph is ℤ-consistent.

function Z consistent(var w [0 . . 2n − 1] [0 . . 2n − 1]) : bool

for i := 0 to 2n − 2 step 2 do

if w[i, \overline{ı}] + w[\overline{ı}, i] < 0 return false; return true;

end function

function tight closure(var w [0 . . 2n − 1] [0 . . 2n − 1]) : bool if not shortest path closure(w) return false; tightening(w); if not Z consistent(w) return false; strengthening(w); return true;

end function

Fig. 6 A O(n^{3}) tight closure algorithm for integer coherent graphs

6.1 A Tight Reduction Procedure for Integer Octagonal Graphs

A definition of tight reduction of a ℤ-consistent integer octagonal graph could be easily introduced by a blind adaptation of (strong) reduction. Such an approach, however, would result in a rather unnatural tight reduction procedure.

Example 1 Let C = {v_{0} ≤ 0, −v_{0} ≤ 0} be a system of integer octagonal constraints on V = {v_{0}}. Then, N^{±} = {v_{0}^{+}, v_{0}^{−}} and we encode C by the integer octagonal graph G = (N^{±}, w), where w(i, j) = 0 for all i, j ∈ N^{±}. Clearly, G = T-closure(G). Let G_{1} = (N^{±}, w_{1}) be the subgraph of G having only arcs (v_{0}^{+}, v_{0}^{−}) and (v_{0}^{−}, v_{0}^{+}): it is easy to observe that T-closure(G_{1}) = T-closure(G) and no proper subgraph of G_{1} satisfies this property. However, the maximum integer octagonal graph equivalent to G is G_{2} = (N^{±}, w_{2}), where the two arcs mentioned above have weights w_{2}(v_{0}^{+}, v_{0}^{−}) = 1 and w_{2}(v_{0}^{−}, v_{0}^{+}) = −1. Note that G_{2} represents the (non-redundant, but unnecessarily involved) integer octagonal constraints C_{2} = {2v_{0} ≤ 1, −2v_{0} ≤ −1}; in particular, G_{2} is not a subgraph of the tight closure of G. ⊓ ⊔

To avoid cases such as Example 1, we require that a tight reduction for G is found among the subgraphs of T-closure(G).

Definition 14 (Tightly reduced graph.) A ℤ-consistent integer octagonal graph G_{1} is tightly reduced if G_{1} is a subgraph of T-closure(G_{1}) and, for each integer octagonal graph G_{2} such that G_{2} is a proper subgraph of G_{1}, T-closure(G_{1}) ≠ T-closure(G_{2}). A tight reduction for the ℤ-consistent integer octagonal graph G is any tightly reduced graph G_{R} such that T-closure(G) = T-closure(G_{R}).

Unsurprisingly, the strong reduction algorithm of Section 4.1, in isolation, will not compute a tight reduction for a ℤ-consistent integer octagonal graph, since it disregards redundancies caused by the tightening inference rule (8).

Example 2 Let C = {v_{0}−v_{1} ≤ 0, v_{0}+v_{1} ≤ 3, v_{0} ≤ 1} be an integer octagonal constraint system on V = {v_{0}, v_{1}}. By applying the strong reduction algorithm of Section 4.1, we would conclude that no constraint in C is redundant. However, v_{0} ≤ 1 is indeed redundant, as it can be obtained by transitivity (3) followed by tightening (7). ⊓ ⊔

In the example above, the constraint v_{0} ≤ 1 is encoded by arc (v_{0}^{+}, v_{0}^{−}) having weight 2: this arc is strongly atomic, hence it is not identified as redundant by the strong reduction procedure. However, if the arc is untightened, we would obtain an arc having weight 3, hence not (strongly) atomic, i.e., redundant.

Definition 15 (Graph untightening.) Let G = (N^{±}, w) be a ℤ-consistent integer octagonal graph. Arc (i, \overline{ı}) is tightly redundant in G if w(i, \overline{ı}) is even and there exists k ∈ N^{±} \ \{i, \overline{ı}\} such that w(i, k) + w(k, \overline{ı}) ≤ w(i, \overline{ı}) + 1. The untightening of G is the graph U = (N^{±}, w_{U}), where the weight function w_{U} is defined, for all i, j ∈ N^{±}, by

w_{U}(i, j) = \begin{cases}+∞, & if j = \overline{ı} and (i, \overline{ı}) is tightly redundant in G; \\ w(i, j), & otherwise. \end{cases}

A correct and efficient tight reduction procedure is obtained by a simple adaptation of the strong reduction procedure of Section 4.1: in step 1 of the algorithm, we compute tight closure (rather than strong closure); steps 2–5 are unchanged and yield graphs A and Z (resulting from steps 4 and 5, respectively); in step 6, the final result is computed as U ⊓ Z, where U is the untightening of A.

Theorem 6 Given a ℤ-consistent integer octagonal graph G, the tight reduction algorithm computes a tight reduction for G.

The tight reduction algorithm has cubic complexity and, when the variable ordering is fixed, computes a canonical form for integer octagonal graphs.

To the best of our knowledge, this is the first time that a reduction procedure for the class of integer octagonal constraints is proposed and proved correct. Previous approaches were based either on more general classes of constraints (thereby incurring into avoidable inefficiencies), or on the rational relaxation of the constraints (thereby failing to identify all redundancies).

7 A Note on Floating-Point Computations

The formal definitions and theoretical results concerning weighted directed graphs assume that the data type adopted for the weights allows for their exact representation and propagation, therefore avoiding any possible problems with overflow, underflow and rounding errors. In actual implementations, by trading some efficiency, such an assumption can be easily fulfilled by adopting unbounded precision data types (integer or rational, depending on the underlying problem), as provided by several software libraries such as GMP, the GNU Multiple Precision arithmetic library.

Catering for inexact data types needs some care since, in particular, this requires that the notion of a correct approximation is made explicit. As an example, consider the case of shortest-path closure for a weighted graph whose variables are meant to take rational values. The computation of the weight of a path corresponds to several applications of the constraint inference rule for transitivity: approximating such a weight from above leads to a correct (but possibly imprecise) inference, whereas approximating it from below is unsafe. Therefore, an implementation willing to correctly approximate the rational shortest-path closure using unbounded precision integers will just need to correctly approximate the input graph (rounding upwards all the rational weights) and then apply any standard closure algorithm.

Example 3 Consider the graph G = (N , w) having k + 1 nodes N = {0, …, k} connected to form a simple path by k ≥ 1 arcs having the same rational weight:

∀i ∈ {1, …, k} : w(i − 1, i) = 1/k.

Clearly, the one and only (hence shortest) path π = 0 ⋯ k from node 0 to node k has rational weight w(π) = 1, which happens to be an integer. By approximating the rational weight function w using an integer weight function w_{ℤ} and then applying closure, we will compute w_{ℤ}(π) = ∑_{i=1}^{k} w_{ℤ}(i − 1, i) = ∑_{i=1}^{k}⌈1/k⌉ = k. ⊓ ⊔

Even though a correct approximation has occurred with respect to the ideal rational computation, the implementation based on unbounded integers can be said to be precise in that no further approximations are introduced besides those incurred during the initial integer encoding of the rational weights. In few words, the representation of input weights is approximate, but their propagation is accurate. In particular, the approximated algorithm still implements a lower closure operator on the domain of weighted graphs.

Things are more difficult if we consider a data type that causes an inexact (though correct) propagation of the weights. This is the case, for instance, when adopting bounded precision floating point coefficients. Correctness can be achieved, almost as easily as before, by applying the appropriate rounding mode not only when approximating the rational weights of the input graph, but also when computing operations such as floating point addition, which is an inexact operation. When reasoning on precision, however, an important issue surfaces: the basic definition of weight of a path as given in Section 2, assumes that addition is an associative operation, but such a property fails to hold for floating point data types. In order to compute the minimum sum of the arc weights in a path, we would need to identify an optimal order of application for additions, probably resulting in algorithms that are too slow.

As an alternative approach, we could incrementally modify the weighted graph by repeated applications of the transitive inference rule (3), until either a fixpoint is reached or an inconsistency is detected. This will result in the definition of a lower closure operator on the lattice 𝔾, below denoted as ‘fpw’, that correctly approximates the ideal one. However, the computed weights might be larger than the minimal ones, as shown in the following example.

Example 4 Let ‘↑’ denote the upward approximation of a rational number using a floating point number and ‘⊞’ denote floating point addition with upward rounding. Consider the graph G = (N , w) where the nodes in N = {a, b, c, d} are connected by three arcs having (rational and floating point) weights w(a, b) = ↑(1/3), w(b, c) = ↑(1/2) = 1/2 and w(c, d) = − ↑(1/3). Clearly, the exact rational weight of path π = abcd is w(abcd) = 1/2. In principle, the same rational weight could also be computed using floating points, as follows:

w(b, c) ⊞ [w(a, b) ⊞ w(c, d)] = 1/2.

However, the result is obtained by a reassociation of the sequence of additions that corresponds to none of the subpaths of π; hence, it can not be computed by incremental applications of the transitivity inference rule, which would instead result in the following approximation:

fpw(abcd) = fpw(ab) ⊞ fpw(bcd)
= fpw(ab) ⊞ [fpw(bc) ⊞ fpw(cd)]
= w(a, b) ⊞ [w(b, c) ⊞ w(c, d)]
= ↑(1/3) ⊞ [1/2 ⊞ (− ↑(1/3))] > 1/2.

⊓ ⊔

It is tempting to adopt ‘fpw’ as the natural definition of floating point weight of a path, since by construction it enjoys an optimal substructure property, so that its implementation can be based on dynamic programming techniques. However, the following example shows that the classical Floyd-Warshall algorithm for rational/integer shortest-path closure is not enough to compute ‘fpw’.

Example 5 Consider the graph G = (N , w) where the nodes in N = {a, b, c, d} are connected by three arcs having floating point weights w(a, b) = 1/2, w(b, c) = ↑(1/3) and w(c, d) = − ↑(1/3). Let w_{fw} be the weight function computed by the classical Floyd-Warshall algorithm, instantiated to use the given floating point data type with upward rounding operations. Clearly, the shortest path from node a to node d has (rational and floating point) weight w(abcd) = fpw(abcd) = 1/2. However, the algorithm will instead compute

w_{fw}(a, d) = w_{fw}(abc) ⊞ w_{fw}(cd)
= [w_{fw}(ab) ⊞ w_{fw}(bc)] ⊞ w_{fw}(cd)
= [w(a, b) ⊞ w(b, c)] ⊞ w(c, d)
= [1/2 ⊞ ↑(1/3)] ⊞ (− ↑(1/3)) > 1/2,

even though w_{fw}(bcd) = fpw(bcd) = 0. This happens because the algorithm, by assuming associativity, does not attempt to improve the computed path weight using the other association fpw(ab) ⊞ fpw(bcd). ⊓ ⊔

In principle, the computation of ‘fpw’ can be carried out by repeatedly applying the Floyd-Warshall algorithm until reaching a fixpoint: we conjecture that such an approach would achieve an O(n^{4}) worst case complexity bound.

It is worth stressing that the observations and examples made above, illustrating the issues caused by inexact floating point addition, can be easily adapted so as to show corresponding issues due to overflows. Such a case is even more general, in that it applies not only to floating point data types, but also to bounded precision integer data types.

In summary, the implementation of a truly semantic abstract domain is not possible using only bounded precision and inexact computations. Nonetheless, by quotienting the syntactic domain of graph representations according to the approximate closure/reduction operators, we obtain a more abstract (but still syntactic) domain where most, although not all, of the redundancies have been removed. As a consequence, the negative side to the adoption of a syntactic abstract domain will be greatly mitigated.

8 Related Work

The shortest-path reduction algorithm of [32] was also considered in [18]. Here the reduction procedure is used, as originally proposed in [32], as a tool for the computation of hollow representations for BDGs, i.e., representations that are appropriate to the case of sparse graphs, so as to obtain memory space savings. This thesis does not appear to identify the positive interaction between reduction and widening and, as a consequence, the thesis conjectures that the computation of hollow representations could compromise the convergence of the abstract iteration sequence (see [18, Section 3.8.2]). When adopting our semantic widenings, the sparse representation can be used even when storing abstract elements at widening points. An adaptation of the reduction algorithm for the case of octagonal graphs is defined in [18, Section 4.5.2] although this differs from the one proposed in Section 4.1. It turns out that the algorithm of [18, Section 4.5.2] may not obtain a strongly reduced graph in the sense of Definition 6: the adapted hollow representation for octagonal graphs can still encode some redundant constraints, as it does not take into proper account the peculiarities of the singular zero-equivalence class. No reduction algorithm is proposed in [18] for the integer octagonal case.

In 2001, Seater and Wonnacott observed that the Omega test [45] could be used to decide the satisfiability of a (non trivially redundant) system of UTVPI integer constraints achieving an O(n^{3}) worst-case complexity bound [46]. In 2005, Lahiri and Musuvathi proposed an O(mn) algorithm for the same satisfiability problem [47], where m is the number of constraints. They also sketched, without formal definitions and proofs, an O(n^{3}) tight closure algorithm. Still in 2005, Miné proposed a modification of the strong (i.e., non-tight) closure algorithm for rational octagonal constraints and argued that this would provide a good and efficient approximation of tight closure [18, 48]. In the same year we showed that the algorithm for computing the strong closure of rational octagonal constraints as described in [8,18,48] could be simplified with a consequential improvement in its efficiency [20,21].

Some of the issues related to the adoption of an inexact data type for the representation of graph weights have also been discussed in [18, Sections 7.3.2 and 7.5.3].

9 Conclusions

We have address the problem of the construction of full-fledged, efficient and provably correct weakly-relational numeric abstract domains.

By considering the semantic abstract domains of geometric shapes, instead of the more concrete abstract domains of their syntactic representations in terms of constraint networks, we have shown how proper widening operators can be derived for several weakly-relational numeric abstractions, including the domain of bounded difference shapes and (rational and integer) octagonal shapes.

For what concerns the efficient representation of octagonal shapes by means of octagonal graphs, we have specified and proved correct strong and tight reduction procedures, as well as more efficient strong and tight closure procedures.

The theoretical results concerning weighted directed graphs hold when the data type adopted for the representation of weights allows for exact computations. If a floating-point data type is considered, then most of these results will be broken due to rounding errors, so that the implementation of a truly semantic abstract domain will not be possible. Nonetheless, the (approximate) reduction operators allow for the removal of most of the syntactic redundancies.

The algorithms presented in this paper have been experimentally validated and are available as part of the Parma Polyhedra Library [40], which is free software distributed under the GNU General Public License. (http://www.cs.unipr.it/ppl/).

Acknowledgements We would like to thank Katy Dobson and Elena Mazzi for useful discussions on topics related to this work.

References

1. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: B. Robinet (ed.) Proceedings of the Second International Symposium on Programming, pp. 106–130. Dunod, Paris, France, Paris, France (1976).

2. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pp. 84–96. ACM Press, Tucson, Arizona (1978).

3. Bagnara, R.: Data-flow analysis for constraint logic-based languages. Ph.D. thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy (1997). Printed as Report TD-1/97

4. Bagnara, R., Giacobazzi, R., Levi, G.: Static analysis of CLP programs over numeric domains. In: M. Billaud, P. Castéran, M. Corsini, K. Musumbu, A. Rauzy (eds.) Actes “Workshop on Static Analysis ’92”, Bigre, vol. 81–82, pp. 43–50. Atelier Irisa, IRISA Campus de Beaulieu, Bordeaux (1992). Extended abstract

5. Bagnara, R., Giacobazzi, R., Levi, G.: An application of constraint propagation to dataflow analysis. In: Proceedings of “The Ninth Conference on Artificial Intelligence for Applications”, pp. 270–276. IEEE Computer Society Press, Los Alamitos, CA, Orlando, Florida (1993)

6. Miné, A.: 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), Lecture Notes in Computer Science, vol. 2053, pp. 155–172. Springer-Verlag, Berlin, Aarhus, Denmark (2001)

7. Shaham, R., Kolodner, E.K., Sagiv, S.: Automatic removal of array memory leaks in Java. In: D.A. Watt (ed.) Proceedings of the 9th International Conference on Compiler Construction (CC 2000), Lecture Notes in Computer Science, vol. 1781, pp. 50–66. Springer-Verlag, Berlin, Berlin, Germany (2000)

8. Miné, A.: The octagon abstract domain. In: Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE’01), pp. 310–319. IEEE Computer Society Press, Stuttgart, Germany (2001)

9. Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: M. Leuschel (ed.) Logic Based Program Synthesis and Tranformation, 12th International Workshop, Lecture Notes in Computer Science, vol. 2664, pp. 71–89. Springer-Verlag, Berlin, Madrid, Spain (2002)

10. Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: R. Giacobazzi (ed.) Static Analysis: Proceedings of the 11th International Symposium, Lecture Notes in Computer Science, vol. 3148, pp. 312–327. Springer-Verlag, Berlin, Verona, Italy (2004)

11. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: R. Cousot (ed.) Verification, Model Checking and Abstract Interpretation: Proceedings of the 6th International Conference (VMCAI 2005), Lecture Notes in Computer Science, vol. 3385, pp. 25–41. Springer-Verlag, Berlin, Paris, France (2005)

12. Miné, A.: A few graph-based relational numerical abstract domains. In: M.V. Hermenegildo, G. Puebla (eds.) Static Analysis: Proceedings of the 9th International Symposium, Lecture Notes in Computer Science, vol. 2477, pp. 117–132. Springer-Verlag, Berlin, Madrid, Spain (2002)

13. Jaffar, J., Maher, M.J., Stuckey, P.J., Yap, R.H.C.: Beyond finite domains. In: A. Borning (ed.) Principles and Practice of Constraint Programming: Proceedings of the Second International Workshop, Lecture Notes in Computer Science, vol. 874, pp. 86–94. Springer-Verlag, Berlin, Rosario, Orcas Island, Washington, USA (1994)

14. Lagarias, J.C.: The computational complexity of simultaneous Diophantine approximation problems. SIAM Journal on Computing 14(1), 196–209 (1985)

15. Balasundaram, V., Kennedy, K.: A technique for summarizing data access and its use in parallelism enhancing transformations. In: B. Knobe (ed.) Proceedings of the ACM SIGPLAN’89 Conference on Programming Language Design and Implementation (PLDI), ACM SIGPLAN Notices, vol. 24(7), pp. 41–53. ACM Press, Portland, Oregon, USA (1989)

16. Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. In: R. Alur, D. Peled (eds.) Computer Aided Verification: Proceedings of the 16th International Conference, Lecture Notes in Computer Science, vol. 3114, pp. 457–461. Springer-Verlag, Berlin, Boston, MA, USA (2004)

17. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The Astrée analyzer. In: M. Sagiv (ed.) Programming Languages and Systems, Proceedings of the 14th European Symposium on Programming, Lecture Notes in Computer Science, vol. 3444, pp. 21–30. Springer-Verlag, Berlin, Edinburgh, UK (2005)

18. Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique, Paris, France (2005)

19. Halbwachs, N.: Détermination automatique de relations linéaires vérifiées par les variables d’un programme. Thèse de 3^{ème} cycle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, France (1979)

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

21. Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E.: Widening operators for weakly-relational numeric abstractions. Quaderno 399, Dipartimento di Matematica, Università di Parma,

Italy (2005). Available at http://www.cs.unipr.it/Publications/

22. Bagnara, R., Hill, P.M., Zaffanella, E.: 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), Lecture Notes in Computer Science, vol. 4905, pp. 8–21. Springer-Verlag, Berlin, San Francisco, USA (2008).

23. Birkhoff, G.: Lattice Theory, Colloquium Publications, vol. XXV, third edn. American Mathematical Society, Providence, Rhode Island, USA (1967)

24. Cousot, P., Cousot, R.: 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, pp. 238–252. ACM Press, New York (1977)

25. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pp. 269– 282. ACM Press, New York (1979).

26. Cormen, T.H., Leiserson, T.E., Rivest, R.L.: Introduction to Algorithms. The MIT Press, Cambridge, MA (1990)

27. Pratt, V.R.: Two easy theories whose combination is hard (1977). Memo sent to Nelson and Oppen concerning a preprint of their paper [49]

28. Bellman, R.: Dynamic Programming. Princeton University Press (1957)

29. Allen, J.F., Kautz, H.A.: A model of naive temporal reasoning. In: J.R. Hobbs, R. Moore (eds.) Formal Theories of the Commonsense World, pp. 251–268. Ablex, Norwood, NJ (1985)

30. Davis, E.: Constraint propagation with interval labels. Artificial Intelligence 32(3), 281– 331 (1987)

31. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: J. Sifakis (ed.) Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, vol. 407, pp. 197–212. Springer-Verlag, Berlin, Grenoble, France (1989)

32. Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structure and state-space reduction. In: Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS’97), pp. 14–24. IEEE Computer Society Press, San Francisco, CA (1997)

33. Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Science of Computer Programming 58(1–2), 28–56 (2005).

34. Aho, A.V., Garey, M.R., Ullman, J.D.: The transitive reduction of a directed graph. SIAM Journal on Computing 1(2), 131–137 (1972)

35. Halbwachs, N., Proy, Y.E., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: B. Le Charlier (ed.) Static Analysis: Proceedings of the 1st International Symposium, Lecture Notes in Computer Science, vol. 864, pp. 223–237. Springer-Verlag, Berlin, Namur, Belgium (1994).

36. Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2), 157–185 (1997)

37. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safetycritical real-time embedded software. In: T.Æ. Mogensen, D.A. Schmidt, I.H. Sudborough (eds.) The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday], Lecture Notes in Computer Science, vol. 2566, pp. 85–108. Springer-Verlag, Berlin (2002)

38. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI’03), pp. 196–207. ACM Press, San Diego, California, USA (2003)

39. Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: D. Schmidt (ed.) Programming Languages and Systems: Proceedings of the 13th European Symposium on Programming, Lecture Notes in Computer Science, vol. 2986, pp. 3–17. Springer-Verlag, Berlin, Barcelona, Spain (2004)

40. Bagnara, R., Hill, P.M., Zaffanella, E.: 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), 3–21 (2008).

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

42. Miné, A.: The Octagon Abstract Domain Library. Semantics and Abstract Interpretation Computer Science Lab., École Normale Supérieure, Paris, France, release 0.9.6 edn. (2002).

Available at http://www.di.ens.fr/~mine/oct/

43. Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation (PLDI’04), pp. 231–242. ACM Press, Washington, DC, USA (2004)

44. Harvey, W., Stuckey, P.J.: A unit two variable per inequality integer constraint solver for constraint logic programming. In: M. Patel (ed.) ACSC’97: Proceedings of the 20th Australasian Computer Science Conference, vol. 19, pp. 102–111. Australian Computer Science Communications (1997)

45. Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Supercomputing 91 (1991)

46. Seater, R., Wonnacott, D.: Polynomial time array dataflow analysis. In: H.G. Dietz (ed.) Languages and Compilers for Parallel Computing, 14th International Workshop, Lecture Notes in Computer Science, vol. 2624, pp. 411–426. Springer-Verlag, Berlin, Cumberland Falls, KY, USA (2001)

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

48. Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)

49. Nelson, G., Oppen, D.C.: Fast decision algorithms based on Union and Find. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS’77), pp. 114–119. IEEE Computer Society Press, Providence, RI, USA (1977). The journal version of this paper is [51]

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

51. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the ACM 27(2), 356–364 (1980). An earlier version of this paper is [49]

A Proofs

In the following we provide some further notation and terminology, as well as the formal proofs for all the results stated in the previous sections. Most of the proofs are based on auxiliary lemmas, some of which are well-known results of graph theory.

A.1 Further Notation and Simple Results on Weighted Graphs

For weighted directed graphs G_{1}, G_{2} ∈ 𝔾, we will write G_{1} ◁ G_{2} when G_{1} ⊴ G_{2} and G_{1} ≠ G_{2}.

Let G = (N^{±}, w) be an octagonal graph. If π = j_{0} ⋯ j_{p} is a path in G, then \overline{π} denotes the path \overline{ȷ}_{p} ⋯ \overline{ȷ}_{0}. Note that, by the coherence assumption (4) of Definition 4, w(π) = w(\overline{π}). A path π in G is said to be (strongly) atomic if all the arcs in π are (strongly) atomic in G.

Definition 16 (Weakly closed graph.) An octagonal graph G = (N^{±}, w) is weakly closed if it satisfies rule (1) in Definition 1 and

∀i, j, k ∈ N^{±} : w(i, k) + w(k, j) ≥ min\{w(i, j), (w(i, \overline{ı}) + w(\overline{ȷ}, j))/2\}.  (11)

The following three lemmas (namely, Lemmas 4, 5 and 6) recall results for weighted graphs that are well-known and/or rather simple. The reader that, for the sake of completeness, is interested in their proofs is referred to the corresponding lemmas in [21] (Lemmas 4, 5 and 7, respectively).

Lemma 4 Let G = (N , w) be a consistent graph. Let also π = i ⋯ j be a path in G. Then there exists a simple path π′ = i ⋯ j such that w(π′) ≤ w(π). Moreover each arc in π′ is also an arc in π.

Lemma 5 Let G = (N , w) be a closed graph. Then, for any path π = i ⋯ j in G, it holds that w(i, j) ≤ w(π).

Lemma 6 Let G = (N , w) be a closed and zero-cycle free graph. Let also π = i ⋯ j be a proper path in G such that w(i, j) = w(π). Then π is a simple path.

Lemma 7 Let G = (N , w) be a consistent graph and G_{c} = (N , w_{c}) be the closure of G. Let also (z_{1}, z_{2}) be an arc in G_{c}. Then there exists a simple path π = z_{1} ⋯ z_{2} in G such that w_{c}(z_{1}, z_{2}) = w(π).

Proof For each i, j ∈ N, let sp(i, j) := min{ w(π) | π = i ⋯ j is a path in G }, so that the graph G_{sp} = (N , sp) directly encodes the shortest-path weights of G. (sp is well defined, because G is consistent and min ∅ = +∞.) For each arc (i, j) of G_{sp}, let also π_{ij} = i ⋯ j be a corresponding simple shortest-path in G such that w(π_{ij}) = sp(i, j).

Note that G_{sp} satisfies property (1) of Definition 1, since the 0-length path i is a shortestpath from node i to itself, so that w(π_{ii}) = sp(i, i) = 0. To see that G_{sp} also satisfies property (2) of Definition 1, by contraposition, we assume that there exist i, j, k ∈ N such that sp(i, j) > sp(i, k) + sp(k, j). Hence, w(π_{ij}) > w(π_{ik}) + w(π_{kj}), i.e., w(π_{ij}) > w(π_{ik} :: π_{kj}), contradicting the assumption that π_{ij} is a shortest-path in G. Hence, G_{sp} is closed and, since by construction G_{sp} ⊴ G, by Definition 1 we obtain G_{sp} ⊴ G_{c}.

Now let (i, j) be any arc in G_{sp}, so that π_{ij} is a shortest-path in G. Since G_{c} ⊴ G, π_{ij} is also a path in G_{c} and w_{c}(π_{ij}) ≤ w(π_{ij}) = sp(i, j). By Lemma 5, w_{c}(i, j) ≤ w_{c}(π_{ij}). Hence, w_{c}(i, j) ≤ sp(i, j), so that G_{c} ⊴ G_{sp}.

As G_{c} = G_{sp}, the thesis follows by definition of G_{sp}, taking π = π_{z_{1}z_{2}}. ⊓ ⊔

A.2 Proofs of the Results Stated in Sections 5 and 6

We anticipate here the proofs of the results stated in Sections 5 and 6 because the proofs of theorems stated in Section 4.1 use these results.

Lemma 8 Let G = (N^{±}, w) be a weakly closed octagonal graph. Then, for all i, j ∈ N^{±},

w(i, \overline{ı}) ≤ 2w(i, j) + w(j, \overline{ȷ}).

Proof Let i, j ∈ N^{±}. Rule (11) of Definition 16, applied to the triple of nodes i, \overline{ı}, j gives

w(i, \overline{ı}) ≤ w(i, j) + w(j, \overline{ı}).

Moreover, with the triple of nodes j, \overline{ı}, \overline{ȷ}, the same rule (11) implies that one of the following two inequalities holds:^{5}

w(j, \overline{ı}) ≤ w(j, \overline{ȷ}) + w(\overline{ȷ}, \overline{ı}), 2w(j, \overline{ı}) ≤ w(j, \overline{ȷ}) + w(i, \overline{ı}).

If the first holds, then

w(i, \overline{ı}) ≤ w(i, j) + w(j, \overline{ı})
≤ w(i, j) + w(j, \overline{ȷ}) + w(\overline{ȷ}, \overline{ı})
= 2w(i, j) + w(j, \overline{ȷ}),

where the last step follows from the coherence assumption (4) of Definition 4. On the other hand, if the second inequality holds, then

2w(i, \overline{ı}) ≤ 2w(i, j) + 2w(j, \overline{ı})
≤ 2w(i, j) + w(j, \overline{ȷ}) + w(i, \overline{ı}).

and hence again we have

w(i, \overline{ı}) ≤ 2w(i, j) + w(j, \overline{ȷ}).

⊓ ⊔

Lemma 9 Let G = (N^{±}, w) be a weakly closed octagonal graph and i, j ∈ N^{±} be such that

2w(i, j) > w(i, \overline{ı}) + w(\overline{ȷ}, j).  (12)

Let G_{s} = (N^{±}, w_{s}) where, for each h_{1}, h_{2} ∈ N^{±},

w_{s}(h_{1}, h_{2}) := \begin{cases}(w(i, \overline{ı}) + w(\overline{ȷ}, j))/2, & if (h_{1}, h_{2}) ∈ \{(i, j), (\overline{ȷ}, \overline{ı})\}; \\ w(h_{1}, h_{2}), & otherwise. \end{cases}  (13)

Then G_{s} is a weakly closed octagonal graph.

Proof By Definition 4, the graph G_{s} is octagonal. By construction, G_{s} ⊴ G. As G is weakly closed, rule (1) of Definition 1 holds so that w(i, i) = 0. As G is consistent, it has no negative weight cycles and hence, 2w(i, i) ≤ w(i, \overline{ı}) + w(\overline{ı}, i). Thus, by hypothesis (12), we have i ≠ j and G_{s} satisfies rule (1) of Definition 1.

Observe that, as G is weakly closed, rule (11) of Definition 16 holds. Also, since G_{s} ⊴ G,

∀h_{1}, h_{2} ∈ N^{±} : w_{s}(h_{1}, h_{2}) ≤ w(h_{1}, h_{2}).  (14)

Suppose z_{1}, z_{2}, z ∈ N^{±}. Then, by Definition 16, to prove that G_{s} is weakly closed, we need to show that

w_{s}(z_{1}, z) + w_{s}(z, z_{2}) ≥ min\{w_{s}(z_{1}, z_{2}), (w_{s}(z_{1}, \overline{z}_{1}) + w_{s}(\overline{z}_{2}, z_{2}))/2\}.  (15)

If (z_{1}, z), (z, z_{2}) ∉ \{(i, j), (\overline{ȷ}, \overline{ı})\}, then, by (13), we have w_{s}(z_{1}, z) = w(z_{1}, z) and w_{s}(z, z_{2}) = w(z, z_{2}) and it follows from rule (11) and property (14) that (15) holds.

5 Note that rule (11) has the form A ≥ min{B, C}; from this we can conclude that A ≥ B (when B is the minimum) or B ≥ C (when C is the minimum).

The remaining cases where (z_{1}, z) ∈ \{(i, j), (\overline{ȷ}, \overline{ı})\} or (z, z_{2}) ∈ \{(i, j), (\overline{ȷ}, \overline{ı})\} are all similar so, to complete the proof, we just consider the case when (z_{1}, z) = (i, j). By hypothesis (13), we have

2w_{s}(i, j) + 2w_{s}(j, z_{2}) = w(i, \overline{ı}) + w(\overline{ȷ}, j) + 2w(j, z_{2});

hence, by the coherence assumption (4) of Definition 4,

2w_{s}(i, j) + 2w_{s}(j, z_{2}) = w(i, \overline{ı}) + w(\overline{ȷ}, j) + 2w(\overline{z}_{2}, \overline{ȷ});

hence, by Lemma 8 (instantiated using nodes \overline{z}_{2} and \overline{ȷ}),

2w_{s}(i, j) + 2w_{s}(j, z_{2}) ≤ w(i, \overline{ı}) + w(\overline{z}_{2}, z_{2});

hence, by hypothesis (13),

2w_{s}(i, j) + 2w_{s}(j, z_{2}) ≤ w_{s}(i, \overline{ı}) + w_{s}(\overline{z}_{2}, z_{2}).

Therefore (15) holds. ⊓ ⊔

Lemma 10 Let G = (N^{±}, w) be weakly closed. Consider the graph G_{S} = (N^{±}, w_{S}) where

∀z_{1}, z_{2} ∈ N^{±} : w_{S}(z_{1}, z_{2}) := min\{w(z_{1}, z_{2}), (w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}))/2\}.  (16)

Then G_{S} is strongly closed.

Proof We first prove that G_{S} is weakly closed, by induction on the number of pairs z_{1}, z_{2} ∈ N^{±} such that 2w(z_{1}, z_{2}) > w(z_{1}, \overline{z}_{1})+w(\overline{z}_{2}, z_{2}). In the base case, when no such pair exists, by (16) we obtain G_{S} = G, so that G_{S} is also weakly closed.

In the inductive case, there exist i, j ∈ N^{±} such that 2w(i, j) > w(i, \overline{ı}) + w(\overline{ȷ}, j); so that i ≠ \overline{ȷ}. Since G and nodes i, j satisfy the hypotheses in Lemma 9, we can define G′ = (N^{±}, w′) equal to the octagonal graph G_{s} = (N^{±}, w_{s}) defined in Lemma 9; it follows that G′ is a weakly closed octagonal graph and

w′(i, j) = min\{w(i, j), (w(i, \overline{ı}) + w(\overline{ȷ}, j))/2\}.  (17)

Let G′_{S} = (N^{±}, w′_{S}) where

∀z_{1}, z_{2} ∈ N^{±} : w′_{S}(z_{1}, z_{2}) := min\{w′(z_{1}, z_{2}), (w′(z_{1}, \overline{z}_{1}) + w′(\overline{z}_{2}, z_{2}))/2\}.

Let z_{1}, z_{2} ∈ N^{±} where (z_{1}, z_{2}) ∉ \{(i, j), (\overline{ȷ}, \overline{ı})\}; then w′(z_{1}, z_{2}) = w(z_{1}, z_{2}); also, as i ≠ \overline{ȷ}, w′(z_{1}, \overline{z}_{1}) = w(z_{1}, \overline{z}_{1}) and w′(z_{2}, \overline{z}_{2}) = w(z_{2}, \overline{z}_{2}); thus we have w′(z_{1}, z_{2}) ≤ (w′(z_{1}, \overline{z}_{1}) + w′(\overline{z}_{2}, z_{2}))/2 if and only if w(z_{1}, z_{2}) ≤ (w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}))/2. Therefore, the induction hypothesis can be applied to G′_{S}, so that G′_{S} must be weakly closed.

By property (17), G_{S} = G′_{S} so that G_{S} is weakly closed. By hypothesis (16), w_{S}(z_{1}, \overline{z}_{1}) = w(z_{1}, \overline{z}_{1}) and w_{S}(\overline{z}_{2}, z_{2}) = w(\overline{z}_{2}, z_{2}), so that, again by hypothesis (16), we have

∀z_{1}, z_{2} ∈ N^{±} : w_{S}(z_{1}, z_{2}) = min\{w_{S}(z_{1}, z_{2}), (w_{S}(z_{1}, \overline{z}_{1}) + w_{S}(\overline{z}_{2}, z_{2}))/2\};

hence, by Definition 16, property (2) of Definition 1 holds, so that G_{S} is closed; and, also, property (6) of Definition 5 holds, so that G_{S} is strongly closed. ⊓ ⊔

Proof (of Theorem 3 on page 17) Let G^{s} = (N^{±}, w^{s}) be such that G^{s} = S-closure(G). By property (6) of Definition 5, for each i, j ∈ N^{±}, w^{s}(i, j) ≤ w_{S}(i, j) so that G^{s} ⊴ G_{S}. Moreover, by construction, G_{S} ⊴ G so that we obtain G^{s} ⊴ G_{S} ⊴ G. Since G is closed, by Definition 16, it is also weakly closed. Hence, by Lemma 10, G_{S} is strongly closed. Hence, G^{s} = G_{S}. ⊓ ⊔

The proof of Theorem 4 relies on an auxiliary lemma.

Lemma 11 Let G = (N^{±}, w) be a weakly closed octagonal graph. Let G_{t} = (N^{±}, w_{t}) where, for each h_{1}, h_{2} ∈ N^{±},

w_{t}(h_{1}, h_{2}) := \begin{cases}w(h_{1}, h_{2}) − 1, & if h_{1} = \overline{h}_{2} and w(h_{1}, h_{2}) is odd; \\ w(h_{1}, h_{2}), & otherwise. \end{cases}  (18)

Then, if G_{t} is consistent, G_{t} is a weakly closed octagonal graph.

Proof Suppose that the graph G_{t} is consistent. By construction, G_{t} is octagonal and G_{t} ⊴ G. As G is weakly closed, rule (1) of Definition 1 holds so that, for all h ∈ N^{±}, w(h, h) = 0 and, by hypothesis (18), w_{t}(h, h) = w(h, h); hence, G_{t} satisfies rule (1) of Definition 1 too. Observe that, as G is weakly closed, rule (11) of Definition 16 holds.

Suppose z_{1}, z_{2}, z ∈ N^{±}. Then, by Definition 16, to prove that G_{t} is weakly closed, we need to show that

w_{t}(z_{1}, z) + w_{t}(z, z_{2}) ≥ min\{w_{t}(z_{1}, z_{2}), (w_{t}(z_{1}, \overline{z}_{1}) + w_{t}(\overline{z}_{2}, z_{2}))/2\}.  (19)

If z_{1} = z_{2}, then (19) is equivalent to w_{t}(z_{1}, z)+w_{t}(z, z_{1}) ≥ 0, which holds due to the hypothesis that G_{t} is consistent. If w_{t}(z_{1}, z) = w(z_{1}, z) and w_{t}(z, z_{2}) = w(z, z_{2}) then, as G_{t} ⊴G, it follows from rule (11) that (19) holds.

Suppose now that z_{1} ≠ z_{2} and w_{t}(z_{1}, z) ≠ w(z_{1}, z); then w_{t}(z_{1}, z_{2}) = w(z_{1}, z_{2}) and, by hypothesis (18), z = \overline{z}_{1}. By application of Lemma 8 to graph G and nodes \overline{z}_{2} and z_{1}, we obtain w(\overline{z}_{2}, z_{2}) ≤ 2w(\overline{z}_{2}, z_{1}) + w(z_{1}, \overline{z}_{1}) so that, by coherence,. w(\overline{z}_{2}, z_{2}) ≤ 2w(\overline{z}_{1}, z_{2}) + w(z_{1}, \overline{z}_{1}). Note however that, if w(\overline{z}_{2}, z_{2}) = 2w(\overline{z}_{1}, z_{2}) + w(z_{1}, \overline{z}_{1}), then w(\overline{z}_{2}, z_{2}) will be odd if and only if w(z_{1}, \overline{z}_{1}) is odd so that, by hypothesis (18), w_{t}(\overline{z}_{2}, z_{2}) = 2w_{t}(\overline{z}_{1}, z_{2}) + w_{t}(z_{1}, \overline{z}_{1}); on the other hand, if w(\overline{z}_{2}, z_{2}) < 2w(\overline{z}_{1}, z_{2}) + w(z_{1}, \overline{z}_{1}), then w(\overline{z}_{2}, z_{2}) ≤ 2w(\overline{z}_{1}, z_{2}) + w(z_{1}, \overline{z}_{1}) − 1 so that, by hypothesis (18), w_{t}(\overline{z}_{2}, z_{2}) ≤ 2w_{t}(\overline{z}_{1}, z_{2}) + w_{t}(z_{1}, \overline{z}_{1}). Therefore, in both cases, 2w_{t}(z_{1}, \overline{z}_{1}) + 2w_{t}(\overline{z}_{1}, z_{2}) ≥ w_{t}(z_{1}, \overline{z}_{1}) + w_{t}(\overline{z}_{2}, z_{2}) so that (19) holds. ⊓ ⊔

Proof (of Theorem 4 on page 19) Let G^{T} := T-closure(G). By definition of G_{T}, G_{T} ⊴G so that T-closure(G_{T}) ⊴ G^{T}. As G_{T} is an octagonal graph, G_{T} is consistent, and hence G^{T} ≠ ⊥; let G^{T} = (N^{±}, w^{T}). Let G_{t} = (N^{±}, w_{t}) be as defined in Lemma 11 so that G_{t} is weakly closed. Then, for all i, j ∈ N^{±},

w_{T}(i, j) = min\{w_{t}(i, j), \frac{w_{t}(i, \overline{ı})}{2} + \frac{w_{t}(\overline{ȷ}, j)}{2} \}.

Therefore, by Lemma 10, G_{T} is strongly closed so that, by Definition 13, G_{T} ⊴ G^{T}. By Definitions 1, 5 and 13, for all i, j ∈ N^{±}, both w^{T}(i, j) ≤ w(i, j) and

w^{T}(i, j) ≤ ⌊ \frac{w(i, \overline{ı})}{2} ⌋ + ⌊ \frac{w(\overline{ȷ}, j)}{2} ⌋

so that, by definition of G_{T}, we have G^{T} ⊴ G_{T}. ⊓ ⊔

Theorem 5 is a corollary of the following result proved in [47, Lemma 4].

Lemma 12 Let G = (N^{±}, w) be an integer octagonal graph with no negative weight cycles and G_{t} = (N^{±}, w_{t}), where w_{t} satisfies (10), have a negative weight cycle. Then there exists 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.

Proof (of Theorem 5 on page 19) The proof is by contradiction; suppose G_{T} is not an octagonal graph; then by Definitions 1, 5 and 13, G_{T} is inconsistent. We show that G_{t} is also inconsistent. Again, we assume to the contrary that G_{t} is consistent and derive a contradiction. Let i, j ∈ N^{±}. By (10), we have w_{t}(i, j) ≤ w(i, j) and w_{t}(i, \overline{ı})/2 + w_{t}(\overline{ȷ}, j)/2 = k_{ij}, where k_{ij} := ⌊w(i, \overline{ı})/2⌋ + ⌊w(\overline{ȷ}, j)/2⌋. Letting S-closure(G_{t}) = (N^{±}, w_{S}), we have, by Definition 5, w_{S}(i, j) ≤ w_{t}(i, j) and w_{S}(i, j) ≤ w_{t}(i, \overline{ı})/2 + w_{t}(\overline{ȷ}, j)/2. Thus w_{S}(i, j) ≤ min\{w(i, j), k_{ij}\}. As this holds for all i, j ∈ N^{±}, by (9), S-closure(G_{t}) ⊴ G_{T}, contradicting the assumption that G_{t} was consistent. Hence G_{t} is inconsistent and therefore contains a negative weight cycle.

By Lemma 12, there exists 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. As G is closed, w(i, \overline{ı}) ≤ w(i · π_{1} · \overline{ı}) and w(\overline{ı}, i) ≤ w(\overline{ı} · π_{2} · i). Thus w(i, \overline{ı}) + w(\overline{ı}, i) ≤ w(π) = 0. Moreover, (i\overline{ı}) is a path and hence the shortest path from i to \overline{ı} so that w(i\overline{ı}) is odd; hence, by (10), w(i, \overline{ı}) = w_{t}(i, \overline{ı}) + 1 and w(\overline{ı}, i) ≥ w_{t}(\overline{ı}, i). Therefore w_{t}(i, \overline{ı}) + w_{t}(\overline{ı}, i) < 0. ⊓ ⊔

A.3 Proofs of the Results Stated in Section 4.1

Proof (of Lemma 1 on page 12) As E is a zero-equivalence class, it is not empty and thus, by construction, \overline{E} is not empty.

Suppose i ∈ \overline{E} and j ∈ N^{±}; then by construction, \overline{ı} ∈ E. As E is a zero-equivalence class, by Definition 7, \overline{ȷ} ∈ E if and only if w(\overline{ı}, \overline{ȷ}) = −w(\overline{ȷ}, \overline{ı}); by the coherence rule (4), w(\overline{ȷ}, \overline{ı}) = −w(\overline{ı}, \overline{ȷ}) if and only if w(i, j) = −w(j, i); hence w(i, j) = −w(j, i) if and only if j ∈ \overline{E}. Hence, by Definition 7, \overline{E} is a zero-equivalence class. ⊓ ⊔

Lemma 13 Let G = (N^{±}, w) be a strongly closed octagonal graph and E ⊆ N^{±} be a zeroequivalence class for G. Then, for each i, j ∈ E and k ∈ N^{±}, we have w(i, k) = w(i, j)+w(j, k) and w(k, i) = w(k, j) + w(j, i).

Proof As G is closed, by property (2) of Definition 1, we have w(i, k) ≤ w(i, j) + w(j, k) and w(k, i) ≤ w(k, j) + w(j, i). Hence, we only have to prove that w(i, k) ≥ w(i, j) + w(j, k) and w(k, i) ≥ w(k, j) + w(j, i). This is equivalent to proving that:

w(j, k) ≤ −w(i, j) + w(i, k),
w(k, j) ≤ −w(j, i) + w(k, i).

Since i, j ∈ E, we have i ≡_{G} j so that, by Definition 7, w(i, j) = −w(j, i). Hence,

w(j, k) ≤ w(j, i) + w(i, k),
w(k, j) ≤ w(i, j) + w(k, i),

which are true, again by property (2) of Definition 1. ⊓ ⊔

Lemma 14 Let G = (N^{±}, w) be a strongly closed octagonal graph with a singular zeroequivalence class E. Then, for each i ∈ E and j ∈ N^{±},

2w(i, j) = w(i, \overline{ı}) + w(\overline{ȷ}, j).

Proof Let i ∈ E and j ∈ N^{±}. As G is a strongly closed octagonal graph, by property (6) of Definition 5, we have 2w(i, j) ≤ w(i, \overline{ı}) + w(\overline{ȷ}, j). Therefore, it remains to be proved that 2w(i, j) ≥ w(i, \overline{ı}) + w(\overline{ȷ}, j).

By hypothesis, i ∈ E so that, as E = \overline{E}, we also have \overline{ı} ∈ E. Therefore, by Lemma 13, w(\overline{ı}, j) = w(\overline{ı}, i) + w(i, j). Since the graph G is octagonal, by the coherence assumption (4) of Definition 4, this can be rewritten as w(\overline{ȷ}, i) = w(\overline{ı}, i) + w(i, j). Thus, by applying property (2) of Definition 1, we obtain:

w(\overline{ȷ}, j) ≤ w(\overline{ȷ}, i) + w(i, j)
= w(\overline{ı}, i) + w(i, j) + w(i, j)
= w(\overline{ı}, i) + 2w(i, j).

Therefore, 2w(i, j) ≥ −w(\overline{ı}, i) + w(\overline{ȷ}, j). As we observed that i ≡_{G} \overline{ı} then, by Definition 7, w(i, \overline{ı}) = −w(\overline{ı}, i), so that we obtain 2w(i, j) ≥ w(i, \overline{ı}) + w(\overline{ȷ}, j). ⊓ ⊔

Proof (of Lemma 2 on page 12) Let E_{1} and E_{2} be singular zero-equivalence classes for the strongly closed octagonal graph G = (N^{±}, w). Let i ∈ E_{1} and j ∈ E_{2}. Then, as E_{1} = \overline{E}_{1} and E_{2} = \overline{E}_{2}, we have i, \overline{ı} ∈ E_{1} and j, \overline{ȷ} ∈ E_{2}. Hence, by Definition 7, w(i, \overline{ı}) = −w(\overline{ı}, i) and w(\overline{ȷ}, j) = −w(j, \overline{ȷ}). Moreover, by Lemma 14,

2w(j, i) = w(j, \overline{ȷ}) + w(\overline{ı}, i),
2w(i, j) = w(i, \overline{ı}) + w(\overline{ȷ}, j).

Thus we obtain

2w(i, j) = w(i, \overline{ı}) + w(\overline{ȷ}, j)
= −w(\overline{ı}, i) − w(j, \overline{ȷ})
= −2w(j, i).

Hence, w(i, j) = −w(j, i) so that, by Definition 7, i ≡_{G} j. Thus, as i, j were arbitrary nodes in E_{1} and E_{2}, respectively, we have the result E_{1} = E_{2}. ⊓ ⊔ Proof (of Lemma 3 on page 13) Let G = (N^{±}, w), L = (N^{±}, w_{L}) and E = (N^{±}, w_{E}); let also L be the set of leaders of the non-singular zero-equivalence classes for G. By Definition 8, L and E are subgraphs of G.

We first prove that the graphs L and E are octagonal; by Definition 4, this means that we have to show that they are consistent and satisfy (4). Observe that since, by hypothesis, the graph G is octagonal, we can assume that G is consistent and satisfies the coherence assumption (4).

To show that L (resp., E) is consistent, consider any cyclic path π in L (resp., in E). Then, as L and E are subgraphs of G, π is also a cyclic path in G and w_{L}(π) = w(π) (resp., w_{E}(π) = w(π)). As G is consistent, we have w(π) ≥ 0 so that w_{L}(π) ≥ 0 (resp., w_{E}(π) ≥ 0). Therefore L and E are both consistent.

To show that (4) for L holds, let i, j ∈ N^{±}. If i = j, then \overline{ı} = \overline{ȷ} and, as G is a closed graph, w(i, i) = w(\overline{ı}, \overline{ı}) = 0. By Definition 8, w_{L}(i, i) = w(i, i) and w_{L}(\overline{ı}, \overline{ı}) = w(\overline{ı}, \overline{ı}) so that w_{L}(i, i) = w_{L}(\overline{ı}, \overline{ı}) = 0. Suppose next that i ≠ j. If i ∉ L or j ∉ L then, by Lemma 1 and the definition of the total ordering on N^{±}, \overline{ı} ∉ L or \overline{ȷ} ∉ L; thus, by Definition 8, w_{L}(i, j) = w_{L}(\overline{ȷ}, \overline{ı}) = +∞. Suppose now that i, j ∈ L. Then, we also have \overline{ı}, \overline{ȷ} ∈ L so that, again, by Definition 8, w_{L}(i, j) = w(i, j) and w_{L}(\overline{ȷ}, \overline{ı}) = w(\overline{ȷ}, \overline{ı}). Since G satisfies (4), w(i, j) = w(\overline{ȷ}, \overline{ı}) so that w_{L}(i, j) = w_{L}(\overline{ȷ}, \overline{ı}). Hence, the graph L satisfies (4).

To show that (4) for E holds, let i, j ∈ N^{±}. If i = j, then \overline{ı} = \overline{ȷ} and, as G is a closed graph, w(i, i) = w(\overline{ı}, \overline{ı}) = 0. Since i ≡_{G} i and \overline{ı} ≡_{G} \overline{ı}, by Definition 8, w_{E}(i, i) = w(i, i) and w_{E}(\overline{ı}, \overline{ı}) = w(\overline{ı}, \overline{ı}) so that w_{E}(i, i) = w_{E}(\overline{ı}, \overline{ı}) = 0. Suppose next that i ≠ j. By Lemma 1, i ≡_{G} j if and only if \overline{ı} ≡_{G} \overline{ȷ}. Thus, by Definition 8, if i ≢_{G} j we have w_{E}(i, j) = w_{E}(\overline{ȷ}, \overline{ı}) = +∞ and, if i ≡_{G} j, we have w_{E}(i, j) = w(i, j) and w_{E}(\overline{ȷ}, \overline{ı}) = w(\overline{ȷ}, \overline{ı}). In the latter case, as G satisfies (4), w(i, j) = w(\overline{ȷ}, \overline{ı}) so that w_{E}(i, j) = w_{E}(\overline{ȷ}, \overline{ı}). Hence, E is a graph that satisfies (4).

Secondly, using the hypothesis that G is strongly closed, we prove that L and E are strongly closed. Namely, we show that given that the weight function w satisfies properties (1) and (2) of Definition 1 and property (6) of Definition 5, we show that the weight functions w_{L} and w_{E} also satisfy properties (1), (2) and (6).

Consider property (1). Let i ∈ N^{±}; as w satisfies (1), w(i, i) = 0, so that, by Definition 8, we also have w_{L}(i, i) = 0 and w_{E}(i, i) = 0.

Consider property (2). Let i, j, k ∈ N^{±}; then we have to show that:

w_{L}(i, j) ≤ w_{L}(i, k) + w_{L}(k, j),  (20)
w_{E}(i, j) ≤ w_{E}(i, k) + w_{E}(k, j).  (21)

When k ∈ {i, j}, (20) and (21) trivially hold. Suppose now that k ∉ {i, j}. Consider first the graph L. If {i, j, k} ⊈ L, then, by Definition 8, w_{L}(i, k) = +∞ or w_{L}(k, j) = +∞, so that (20) holds. If, instead, i, j, k ∈ L, then, by Definition 8, w_{L}(i, j) = w(i, j), w_{L}(i, k) = w(i, k) and w_{L}(k, j) = w(k, j). Hence, as w satisfies (2), (20) holds. Consider now the graph E. If i ≢_{G} k or j ≢_{G} k then, by Definition 8, w_{E}(i, k) = +∞ or w_{E}(k, j) = +∞, so that (21) holds. If, instead, i ≡_{G} k and j ≡_{G} k so that i ≡_{G} j; then, by Definition 8, w_{E}(i, j) = w(i, j), w_{E}(i, k) = w(i, k) and w_{E}(k, j) = w(k, j). Hence, as w satisfies (2), (21) holds.

Consider property (6). Let i, j ∈ N^{±}; then we have to show that:

2w_{L}(i, j) ≤ w_{L}(i, \overline{ı}) + w_{L}(\overline{ȷ}, j),  (22)
2w_{E}(i, j) ≤ w_{E}(i, \overline{ı}) + w_{E}(\overline{ȷ}, j).  (23)

When i = j, it follows from the consistency and property (1), proved in previous paragraphs for L and E that (22) and (23) hold. Suppose now that i ≠ j. Consider first the graph L. If \{i, j\} ⊈ L, then, by Definition 8, w_{L}(i, \overline{ı}) = +∞ or w_{L}(\overline{ȷ}, j) = +∞ so that (22) holds. If, instead, i, j ∈ L; then by Lemma 1 and the definition of the total ordering on N^{±}, \overline{ı}, \overline{ȷ} ∈ L so that w_{L}(i, j) = w(i, j), w_{L}(i, \overline{ı}) = w(i, \overline{ı}) and w_{L}(\overline{ȷ}, j) = w(\overline{ȷ}, j). Hence, as w satisfies (4), (22) holds. Consider now the graph E. If i ≢_{G} \overline{ı} or j ≢_{G} \overline{ȷ}, then, by Definition 8, w_{E}(i, \overline{ı}) = +∞ or w_{E}(\overline{ȷ}, j) = +∞, so that (23) holds. Suppose, instead that both i ≡_{G} \overline{ı} and j ≡_{G} \overline{ȷ}; then, by Definition 8, w_{E}(i, j) = w(i, j), w_{E}(i, \overline{ı}) = w(i, \overline{ı}) and w_{E}(\overline{ȷ}, j) = w(\overline{ȷ}, j). Hence, as w satisfies (4), (23) holds.

Finally, we prove that L is a zero-cycle free graph. Let π = j_{0}j_{1} ⋯ j_{p} be a proper cycle in L; thus j_{0} = j_{p} and j_{0} ≠ j_{1}. As w_{L}(j_{0}, j_{1}) < +∞, by Definition 8, we have j_{0}, j_{1} ∈ L, so that j_{0} ≢_{G} j_{1}. Hence, by Definition 7, w_{L}(j_{0}, j_{1}) + w_{L}(j_{1}, j_{0}) > 0. We have already shown that L is closed; hence, by Lemma 5, w_{L}(j_{1} ⋯ j_{p}) ≥ w_{L}(j_{1}, j_{p}) = w_{L}(j_{1}, j_{0}) so that w_{L}(π) ≥ w_{L}(j_{0}, j_{1}) + w_{L}(j_{1}, j_{0}) > 0. ⊓ ⊔ Lemma 15 Let G = (N^{±}, w) be a closed and zero-cycle free octagonal graph. Suppose that (i, j) is an arc in G. Then there exists a simple and atomic path π = i ⋯ j in G such that w(i, j) = w(π).

Proof If i = j, let π = i so that π is a simple and atomic path such that w(π) = 0. As G is closed, w(i, j) = 0 so that w(i, j) = w(π) as required.

Suppose now that i ≠ j. Let π = j_{0} ⋯ j_{p} be a path of length p in G where i = j_{0}, j = j_{p} and w(i, j) = w(π) (for instance we can take p = 1). Suppose that j_{a−1} = j_{a}, for some a ∈ {1, …, p}. Then, as G is closed, w(j_{a−1}, j_{a}) = 0 and, since i ≠ j, we can drop the non-proper arc (j_{a−1}, j_{a}) from path π and obtain another path π′ from i to j such that w(i, j) = w(π′). Therefore, we can assume that π is a proper path. By Lemma 6, the path is also simple. Thus, as N is finite, we can assume that p is maximal such that w(i, j) = w(π) and π is a simple path in G.

Suppose, for some q = 1, …, p, that the arc (j_{q−1}, j_{q}) in π is not atomic in G. Then, by property (2) of Definition 1 and Definition 9, there must exist k ∈ N \ {j_{q−1}, j_{q}} such that w(j_{q−1}, j_{q}) = w(j_{q−1}, k)+w(k, j_{q}). Thus, letting π_{1} = j_{0} ⋯ j_{q−1} and π_{2} = j_{q} ⋯ j_{p}, we obtain

w(j_{0}, j_{p}) = w(π_{1} :: (j_{q−1}j_{q}) :: π_{2})
= w(π_{1}) + w(j_{q−1}, j_{q}) + w(π_{2})
= w(π_{1}) + w(j_{q−1}, k) + w(k, j_{q}) + w(π_{2})
= w(π_{1} :: (j_{q−1}kj_{q}) :: π_{2}).

By Lemma 6, the path π′ = π_{1} :: (j_{q−1}kj_{q}) :: π_{2}, which has length p + 1, is simple too, contradicting the maximality assumption for path π. Thus (j_{q−1}, j_{q}) is atomic in G. As this holds for any arc in π, the path π is atomic. ⊓ ⊔

Lemma 16 Let G = (N^{±}, w) be a closed and zero-cycle free octagonal graph. Suppose that, for some i ∈ N^{±}, there is a proper path π = j_{0} ⋯ j_{p}, where i = j_{0}, \overline{ı} = j_{p} and w(i, \overline{ı}) = w(π). Then there is at most one arc in the path π that is atomic but not strongly atomic in G.

Proof The proof is by contraposition. Suppose that, for some q, r ∈ {1, …, p} such that q < r, the arcs (j_{q−1}, j_{q}) and (j_{r−1}, j_{r}) are atomic but not strongly atomic in G. Then, by Definition 9,

2w(j_{q−1}, j_{q}) ≥ w(j_{q−1}, \overline{ȷ}_{q−1}) + w(\overline{ȷ}_{q}, j_{q}),
2w(j_{r−1}, j_{r}) ≥ w(j_{r−1}, \overline{ȷ}_{r−1}) + w(\overline{ȷ}_{r}, j_{r}).

Let π_{1} = j_{0} ⋯ j_{q−1}, π_{2} = j_{q} ⋯ j_{r−1} and π_{3} = j_{r} ⋯ j_{p}, so that π = π_{1} :: (j_{q−1}j_{q}) :: π_{2} :: (j_{r−1}j_{r}) :: π_{3}. Since w(i, \overline{ı}) = w(π), we obtain

2w(i, \overline{ı}) = 2w(π_{1} :: (j_{q−1}j_{q}) :: π_{2} :: (j_{r−1}j_{r}) :: π_{3})
= 2w(π_{1}) + 2w(j_{q−1}, j_{q}) + 2w(π_{2}) + 2w(j_{r−1}, j_{r}) + 2w(π_{3}).

As G is an octagonal graph, this can be rewritten

2w(i, \overline{ı}) ≥ w(π_{1}) + w(j_{q−1}, \overline{ȷ}_{q−1}) + w(\overline{π}_{1})
+ w(\overline{ȷ}_{q}, j_{q}) + w(π_{2}) + w(j_{r−1}, \overline{ȷ}_{r−1}) + w(\overline{π}_{2})
+ w(\overline{π}_{3}) + w(\overline{ȷ}_{r}, j_{r}) + w(π_{3})
= w(π_{1} :: (j_{q−1}\overline{ȷ}_{q−1}) :: \overline{π}_{1})
+ w((\overline{ȷ}_{q}j_{q}) :: π_{2} :: (j_{r−1}\overline{ȷ}_{r−1}) :: \overline{π}_{2})
+ w(\overline{π}_{3} :: (\overline{ȷ}_{r}j_{r}) :: π_{3}).

Note that the path π′_{2} = (\overline{ȷ}_{q}j_{q}) :: π_{2} :: (j_{r−1}\overline{ȷ}_{r−1}) :: \overline{π}_{2} is a proper cycle from node \overline{ȷ}_{q} to itself. Moreover, both paths π′_{1} = π_{1} :: (j_{q−1}\overline{ȷ}_{q−1}) :: \overline{π}_{1} and π′_{3} = \overline{π}_{3} :: (\overline{ȷ}_{r}j_{r}) :: π_{3} go from node i to node \overline{ı} so that, by Lemma 5, we have w(i, \overline{ı}) ≤ w(π′_{1}) and w(i, \overline{ı}) ≤ w(π′_{3}). As a consequence,

2w(i, \overline{ı}) ≥ w(i, \overline{ı}) + w(π′_{2}) + w(i, \overline{ı}).

Therefore we obtain w(π′_{2}) ≤ 0, contradicting the hypothesis that the graph G is consistent and zero-cycle free. It follows that q = r. ⊓ ⊔ Lemma 17 Let G = (N^{±}, w) be a closed and zero-cycle free octagonal graph. Suppose that (i, \overline{ı}) is an arc in G. Then there exists a strongly atomic path π = j_{0} ⋯ j_{p} in G, where i = j_{0}, \overline{ı} = j_{p} and w(i, \overline{ı}) = w(π).

Proof By Lemma 15, there exists a simple and atomic path π in G from i to \overline{ı} and w(i, \overline{ı}) = w(π). Since the path is simple, we can take p = ∥π∥ to be maximal in the set of paths having these properties. Suppose that π is not strongly atomic in G. Then, by Lemma 16, there must be exactly one arc (j_{q−1}, j_{q}) in π that is atomic but not not strongly atomic in G. Let h = j_{q−1} and k = j_{q}. Thus, π = π_{h} :: (hk) :: π_{k}, where the subpaths π_{h} = j_{0} ⋯ j_{q−1} and π_{k} = j_{q} ⋯ j_{p} are strongly atomic in G. As the graph G is octagonal, the paths \overline{π}_{h} and \overline{π}_{k} are also strongly atomic and satisfy w(π_{h}) = w(\overline{π}_{h}) and w(π_{k}) = w(\overline{π}_{k}).

Since the arc (h, k) is atomic but not strongly atomic, by Definition 9,

2w(h, k) ≥ w(h, \overline{h}) + w(\overline{k}, k).

Therefore, as G is octagonal,

2w(i, \overline{ı}) = 2w(π_{h}) + 2w(h, k) + 2w(π_{k})
≥ 2w(π_{h}) + w(h, \overline{h}) + w(\overline{k}, k) + 2w(π_{k})
= w(π_{h}) + w(h, \overline{h}) + w(\overline{π}_{h})
+ w(\overline{π}_{k}) + w(\overline{k}, k) + w(π_{k})
= w(π_{h} :: (h\overline{h}) :: \overline{π}_{h}) + w(\overline{π}_{k} :: (\overline{k}k) :: π_{k}).

Note that both paths π′ = π_{h} :: (h\overline{h}) :: \overline{π}_{h} and π′′ = \overline{π}_{k} :: (\overline{k}k) :: π_{k} go from node i to node \overline{ı}. Thus, by Lemma 5, we have w(i, \overline{ı}) ≤ w(π′) and w(i, \overline{ı}) ≤ w(π′′). As a consequence, we obtain

w(i, \overline{ı}) = w(π′) = w(π′′).

As h ≠ \overline{h} and k ≠ \overline{k} and as π_{h}, \overline{π}_{h} and π_{k}, \overline{π}_{k} are proper paths, both π′ and π′′ are proper paths too; and hence, by Lemma 6, they are both simple paths. Moreover, by the maximality assumption for p, we have ∥π′∥ = ∥π′′∥ = p. Consider now just one of these paths: π′.

To conclude the proof, we will show that (h, \overline{h}) is a strongly atomic arc in G, so that π′ is a strongly atomic path in G. Suppose instead that (h, \overline{h}) is not strongly atomic in G. Then, by Definition 9, it is not atomic, so that there exists ℓ ∈ N^{±} \ \{h, \overline{h}\} such that w(h, \overline{h}) = w(h, ℓ) + w(ℓ, \overline{h}). Consider the path π′′′ = π_{h} :: (hℓ\overline{h}) :: \overline{π}_{h}. Then π′′′ is a proper path in G such that w(i, \overline{ı}) = w(π′′′) and ∥π′′′∥ > p; contradicting the assumption that p was maximal. It follows that the arc (h, \overline{h}) is strongly atomic in G. ⊓ ⊔

Lemma 18 Let G = (N^{±}, w) be a closed and zero-cycle free octagonal graph. Suppose that (i, j) is an arc in G. Then one of the following properties holds:

1. there exists a strongly atomic path π = i ⋯ j in G where w(i, j) = w(π);

2. i ≠ \overline{ȷ}, 2w(i, j) ≥ w(i, \overline{ı}) + w(\overline{ȷ}, j) and there exist strongly atomic paths π_{i} = i ⋯ \overline{ı}, π_{j} = \overline{ȷ} ⋯ j in G where w(i, \overline{ı}) = w(π_{i}) and w(\overline{ȷ}, j) = w(π_{j}).

Proof By Lemma 15, there exists a simple and atomic path π = i ⋯ j in G where w(i, j) = w(π). If i = j, then ∥π∥ = 0, so that the path π is strongly atomic and condition 1 holds. Suppose now that i ≠ j.

If the path is strongly atomic in G, then condition 1 holds. Therefore to complete the proof we assume that π is not strongly atomic in G and show that condition 2 holds.

By Definition 9, there exists at least one arc (h, k) in π that is atomic but not strongly atomic in G. As π is a simple path, h ≠ k so that, again by Definition 9,

2w(h, k) = w(h, \overline{h}) + w(\overline{k}, k).

As the graph is octagonal, we have w(i, h) = w(\overline{h}, \overline{ı}) and w(k, j) = w(\overline{ȷ}, \overline{k}). Moreover, by Lemma 5,

w(i, \overline{ı}) ≤ w(i, h) + w(h, \overline{h}) + w(\overline{h}, \overline{ı}),
w(\overline{ȷ}, j) ≤ w(\overline{ȷ}, \overline{k}) + w(\overline{k}, k) + w(k, j).

Thus, as w(i, j) = w(π), we have

2w(i, j) = 2w(i, h) + 2w(h, k) + 2w(k, j)
= 2w(i, h) + w(h, \overline{h}) + w(\overline{k}, k) + 2w(k, j)
= w(i, h) + w(h, \overline{h}) + w(\overline{h}, \overline{ı})
+ w(\overline{ȷ}, \overline{k}) + w(\overline{k}, k) + w(k, j)
≥ w(i, \overline{ı}) + w(\overline{ȷ}, j).

By Lemma 17, there exist strongly atomic paths π_{i} = i ⋯ \overline{ı} and π_{j} = \overline{ȷ} ⋯ j in G where w(i, \overline{ı}) = w(π_{i}) and w(\overline{ȷ}, j) = w(π_{j}); therefore, condition 2 holds. ⊓ ⊔

Lemma 19 Let G be a strongly closed and zero-cycle free octagonal graph and let A be its strongly atomic subgraph. Then A is an octagonal subgraph of G and S-closure(A) = G.

Proof It follows from Definition 9 that A is a subgraph of G and, for all i, j ∈ N^{±}, (i, j) is an arc in A if and only if (\overline{ȷ}, \overline{ı}) is an arc in A. Therefore, as G is octagonal, A is also octagonal.

Since G ⊴ A and the strong closure operator is both monotonic and idempotent, we obtain that G ⊴ S-closure(A). Therefore to prove S-closure(A) = G, we just need to show that S-closure(A) ⊴ G. Letting G = (N^{±}, w), S-closure(A) = (N^{±}, w_{S}) and (i, j) be any arc of G, we will show that w_{S}(i, j) ≤ w(i, j). Since G is closed and zero-cycle free, either one of two cases of Lemma 18 holds.

If case 1 of Lemma 18 holds, then there exists a strongly atomic path π = i ⋯ j in G where w(i, j) = w(π). By Definition 9, π is also a path in A having the same weight w(π). Since strong closure is a reductive operator, w_{S}(π) ≤ w(π). Moreover, by Lemma 5, w_{S}(i, j) ≤ w_{S}(π) and hence w_{S}(i, j) ≤ w(i, j).

If case 2 of Lemma 18 holds, then 2w(i, j) ≥ w(i, \overline{ı})+w(\overline{ȷ}, j) and there exist strongly atomic paths π_{i} = i ⋯ \overline{ı}, π_{j} = \overline{ȷ} ⋯ j in G where w(i, \overline{ı}) = w(π_{i}) and w(\overline{ȷ}, j) = w(π_{j}). By property (6) of Definition 5, we also have 2w(i, j) ≤ w(i, \overline{ı}) + w(\overline{ȷ}, j), so that we obtain

2w(i, j) = w(i, \overline{ı}) + w(\overline{ȷ}, j).

By Definition 9, π_{i} and π_{j} are also paths in A having the same weights w(π_{i}) and w(π_{j}). Since strong closure is a reductive operator, w_{S}(π_{i}) ≤ w(π_{i}) and w_{S}(π_{j}) ≤ w(π_{j}). By Lemma 5, w_{S}(i, \overline{ı}) ≤ w_{S}(π_{i}) and w_{S}(\overline{ȷ}, j) ≤ w_{S}(π_{j}); hence we have w_{S}(i, \overline{ı}) ≤ w(i, \overline{ı}) and w_{S}(\overline{ȷ}, j) ≤ w(\overline{ȷ}, j). Thus, w_{S}(i, \overline{ı}) + w_{S}(\overline{ȷ}, j) ≤ 2w(i, j) and, by property (6) of Definition 5, w_{S}(i, j) ≤ w(i, j).

We can therefore conclude that S-closure(A) ⊴ G. ⊓ ⊔

Lemma 20 Let G be a strongly closed octagonal graph and Z the zero-equivalence reduction for G. Then Z is an octagonal subgraph of G.

Proof Let G = (N^{±}, w) and Z = (N^{±}, w_{Z}). Let the weight function w′ be as defined in Definition 10; then (N^{±}, w′) is a subgraph of G. To show that Z is a subgraph of G, consider any i, j ∈ N^{±} such that w_{Z}(i, j) < +∞. By Definition 10, w_{Z}(i, j) = min\{w′(i, j), w′(\overline{ȷ}, \overline{ı})\} and hence, w_{Z}(i, j) = w(i, j) or w_{Z}(i, j) = w(\overline{ȷ}, \overline{ı}); since G is an octagonal graph, w_{Z}(i, j) = w(i, j). Therefore, Z is a subgraph of G, which implies G ⊴ Z and, as G is consistent, Z is a consistent graph too. Moreover, for all i, j ∈ N^{±}, we have

w_{Z}(i, j) = w_{Z}(\overline{ȷ}, \overline{ı}) = min\{w′(i, j), w′(\overline{ȷ}, \overline{ı})\}.

Thus, w_{Z} also satisfies the coherence assumption (4) of Definition 4. Therefore, Z is octagonal and hence, an octagonal subgraph of G. ⊓ ⊔

Lemma 21 Let E = (N^{±}, w_{E}) be the zero-equivalence subgraph of a strongly closed octagonal graph G. Let also i, j ∈ N^{±} and π = i ⋯ j be a path in E. Then w_{E}(π) = w_{E}(i, j).

Proof The proof is by induction on p = ∥π∥. If p = 0, then i = j, π = i and w_{E}(π) = 0; thus, as (i, i) is an arc in E and G is closed, the result w_{E}(i, i) = 0 holds by property (1) of Definition 1. For the inductive case, when p > 0, let π = i·π′ be a path in E, where the subpath π′ = k ⋯ j is such that ∥π′∥ = p − 1. Thus, by the inductive hypothesis, w_{E}(π′) = w_{E}(k, j) and we obtain

w_{E}(π) = w_{E}(i, k) + w_{E}(π′)
= w_{E}(i, k) + w_{E}(k, j)
= w_{E}(i, j),

where the last step holds by Lemma 13, as i, k are nodes in E. ⊓ ⊔

Lemma 22 Let E = (N^{±}, w_{E}) be the zero-equivalence subgraph of a strongly closed octagonal graph and Z = (N^{±}, w_{Z}) the zero-equivalence reduction for E. Let also i, j ∈ N^{±} be such that i ≡_{E} j. Then there exists a path π = i ⋯ j in Z such that w_{Z}(π) = w_{E}(i, j).

Proof Let w′ and w_{Z} be as specified in Definition 10; thus, (N^{±}, w′) is a subgraph of the octagonal graph Z. We first show that, for any zero-equivalence class E for E, if E contains more than one node, then there is a cycle π_{E} in Z that contains all the nodes in E.

Suppose first that the zero-equivalence class E = {z_{0}, …, z_{m}}, where m > 0, is nonsingular. If E is positive and z_{0} < ⋯ < z_{m}, then, by Definition 10, there is a cycle π_{E} = z_{0} ⋯ z_{m}z_{0} in (N^{±}, w′). Hence, π_{E} is also a cycle in Z. If E is a negative zero-equivalence class, then \overline{E} = \{\overline{z}_{0}, …, \overline{z}_{m}\} is positive and \overline{z}_{0} < ⋯ < \overline{z}_{m} so that, by the previous argument, there is a cycle π\overline{E} = \overline{z}_{0} ⋯ \overline{z}_{m}\overline{z}_{0} in Z connecting the nodes of \overline{E}. By Lemma 20, Z is octagonal, so that there is also a cycle π_{E} = \overline{π}\overline{E} = z_{0}z_{m} ⋯ z_{0} in Z that connects the nodes of E.

Suppose next that the zero-equivalence class E = \{z_{0}, \overline{z}_{0}, …, z_{m}, \overline{z}_{m}\} is singular and that z_{0} < \overline{z}_{0} < ⋯ z_{m} < \overline{z}_{m}. Then, by Definition 10, there is a path π^{+} = z_{0} ⋯ z_{m} in (N^{±}, w′) and, hence, in Z; Since E = \overline{E} and Z is octagonal, there is a path π^{−} = \overline{z}_{m} ⋯ \overline{z}_{0} in Z. Also, by Definition 10, (N^{±}, w′) contains the arcs (\overline{z}_{0}, z_{0}) and (z_{m}, \overline{z}_{m}). Therefore, π_{E} = π^{+} :: (z_{m}\overline{z}_{m}) :: π^{−} :: (\overline{z}_{0}z_{0}) is a cycle in Z that contains all the nodes in E.

As i ≡_{E} j, by Definition 7, for some zero-equivalence class E in E, i, j ∈ E. Note that, since i ≠ j, if E = {z_{0}, …, z_{m}} is non-singular, then it must be m > 0. Thus i and j are nodes in the cycle π_{E} as defined above; thus, there exists a path π = i ⋯ j in Z. As Z is a subgraph of E, w_{Z}(π) = w_{E}(π). By Lemma 21, w_{E}(π) = w_{E}(i, j) and thus, w_{Z}(π) = w_{E}(i, j). ⊓ ⊔

Lemma 23 Let E = (N^{±}, w_{E}) be the zero-equivalence subgraph of a strongly closed octagonal graph. Let also Z = (N^{±}, w_{Z}) be the zero-equivalence reduction for E. Then S-closure(Z) = E.

Proof Let S-closure(Z) = Z^{S} = (N^{±}, w_{Z}^{S}). By Lemma 3, E is strongly closed octagonal graph. By Lemma 20, Z is an octagonal subgraph of E. Hence, E ⊴ Z and E ⊴ Z^{S}. Consider any i, j ∈ N^{±}. Then w_{Z}^{S}(i, j) ≥ w_{E}(i, j); it remains to show that w_{E}(i, j) ≥ w_{Z}^{S}(i, j).

If w_{E}(i, j) = +∞. then, as w_{Z}^{S}(i, j) ≥ w_{E}(i, j), w_{Z}^{S}(i, j) = +∞. Suppose now that w_{E}(i, j) < +∞ so that, by Definition 8, i ≡_{E} j. By Lemma 22, there exists a path π = i ⋯ j in Z such that w_{E}(i, j) = w_{Z}(π); as Z^{S} ⊴ Z, we also have w_{Z}(π) ≥ w_{Z}^{S}(π); and, by Lemma 5, w_{Z}^{S}(π) ≥ w_{Z}^{S}(i, j); therefore w_{E}(i, j) ≥ w_{Z}^{S}(i, j). ⊓ ⊔

Proof (of Theorem 1 on page 14) Let G = (N^{±}, w) be the strong closure of the input octagonal graph, computed at step 1 of the strong reduction procedure; let L = (N^{±}, w_{L}) be the non-singular leaders’ subgraph of G; E = (N^{±}, w_{E}) the zero-equivalence subgraph of G; A = (N^{±}, w_{A}) the strongly atomic subgraph of L; Z = (N^{±}, w_{Z}) the zero-equivalence reduction of E; G_{R} = (N^{±}, w_{R}) = A ⊓ Z; and G_{R}^{S} = (N^{±}, w_{R}^{S}) = S-closure(G_{R}). Then we need to show that G_{R} is a strongly reduced octagonal graph and G_{R}^{S} = G.

By Definition 8 and Lemma 3, both L and E are octagonal subgraphs of G. By Lemma 19, A is an octagonal subgraph of L and, by Lemma 20, Z is an octagonal subgraph of E; hence A and Z are octagonal subgraphs of G. Therefore, G_{R} = A ⊓ Z is an octagonal subgraph of G.

Next we show that G_{R}^{S} = G. By Lemma 3, L is strongly closed and zero-cycle free; by Lemma 19, S-closure(A) = L. By Lemma 23, S-closure(Z) = E. Thus, we have

G_{R}^{S} = S-closure(S-closure(A ⊓ Z))

= S-closure(S-closure(A) ⊓ S-closure(Z))

= S-closure(L ⊓ E).

As observed before, L and E are subgraphs of G and hence G ⊴ G_{R}^{S}. It remains to show that G_{R}^{S} ⊴ G. Let (i, j) be an arc in G and suppose that i ∈ E_{i} and j ∈ E_{j}, where E_{i} and E_{j} are zero-equivalence classes for G. Then, to prove that G_{R}^{S} ⊴ G, we just need to show that

w_{R}^{S}(i, j) ≤ w(i, j).  (24)

To do this, without loss of generality, we need to consider three cases:

1. E_{i} and E_{j} are singular zero-equivalence classes in G;

2. E_{i} is singular and E_{j} is a non-singular zero-equivalence class in G;

3. E_{i} and E_{j} are non-singular zero-equivalence classes in G.

Case 1. By Lemma 2, E_{i} = E_{j} so that w(i, j) = w_{E}(i, j). Therefore, as w_{R}^{S}(i, j) ≤ w_{E}(i, j), Equation (24) holds.

Case 2. Let ℓ_{j} ∈ N^{±} be the leader of E_{j} so that \overline{ℓ}_{j} is the leader of the non-singular zero-equivalence class \overline{E}_{j}. By Definition 8,

\begin{aligned}w(i, \overline{ı}) & = w_{E}(i, \overline{ı}), & w(\overline{ȷ}, \overline{ℓ}_{j}) & = w_{E}(\overline{ȷ}, \overline{ℓ}_{j}), \\ w(ℓ_{j}, j) & = w_{E}(ℓ_{j}, j), & w(\overline{ℓ}_{j}, ℓ_{j}) & = w_{L}(\overline{ℓ}_{j}, ℓ_{j}). \end{aligned}  (25)

By Lemma 13,

w(\overline{ȷ}, j) = w(\overline{ȷ}, \overline{ℓ}_{j}) + w(\overline{ℓ}_{j}, j)
= w(\overline{ȷ}, \overline{ℓ}_{j}) + w(\overline{ℓ}_{j}, ℓ_{j}) + w(ℓ_{j}, j)

so that, by Lemma 14 and Equation (25),

2w(i, j) = w(i, \overline{ı}) + w(\overline{ȷ}, j)
= w(i, \overline{ı}) + w(\overline{ȷ}, \overline{ℓ}_{j}) + w(\overline{ℓ}_{j}, ℓ_{j}) + w(ℓ_{j}, j)
= w_{E}(i, \overline{ı}) + w_{E}(\overline{ȷ}, \overline{ℓ}_{j}) + w_{L}(\overline{ℓ}_{j}, ℓ_{j}) + w_{E}(ℓ_{j}, j).

Moreover, by Lemma 5,

2w_{R}^{S}(i, j) ≤ w_{R}^{S}(i, \overline{ı}) + w_{R}^{S}(\overline{ȷ}, \overline{ℓ}_{j}) + w_{R}^{S}(\overline{ℓ}_{j}, ℓ_{j}) + w_{R}^{S}(ℓ_{j}, j)
≤ w_{E}(i, \overline{ı}) + w_{E}(\overline{ȷ}, \overline{ℓ}_{j}) + w_{L}(\overline{ℓ}_{j}, ℓ_{j}) + w_{E}(ℓ_{j}, j)

since G_{R}^{S} ⊴ L and G_{R}^{S} ⊴ E. Therefore Equation (24) holds.

Case 3. By Definition 8,

w(i, ℓ_{i}) = w_{E}(i, ℓ_{i}), w(ℓ_{j}, j) = w_{E}(ℓ_{j}, j), w(ℓ_{i}, ℓ_{j}) = w_{L}(ℓ_{i}, ℓ_{j}).

Therefore, by Lemma 13,

w(i, j) = w(i, ℓ_{i}) + w(ℓ_{i}, j)
= w(i, ℓ_{i}) + w(ℓ_{i}, ℓ_{j}) + w(ℓ_{j}, j)
= w_{E}(i, ℓ_{i}) + w_{L}(ℓ_{i}, ℓ_{j}) + w_{E}(ℓ_{j}, j).

Moreover, by Lemma 5,

w_{R}^{S}(i, j) ≤ w_{R}^{S}(i, ℓ_{i}) + w_{R}^{S}(ℓ_{i}, ℓ_{j}) + w_{R}^{S}(ℓ_{j}, j)
≤ w_{E}(i, ℓ_{i}) + w_{L}(ℓ_{i}, ℓ_{j}) + w_{E}(ℓ_{j}, j),

since G_{R}^{S} ⊴ L and G_{R}^{S} ⊴ E. Therefore Equation (24) holds and hence G_{R}^{S} = G.

Finally, to show that G_{R} is strongly reduced, as specified in Definition 6, we assume there exists a strongly reduced octagonal graph G_{2} = (N^{±}, w_{2}) such that G_{R} ◁ G_{2} and G = S-closure(G_{2}) and derive a contradiction. Let G_{2}^{c} = (N^{±}, w_{2}^{c}) = closure(G_{2}), G_{R}^{c} = (N^{±}, w_{R}^{c}) = closure(G_{R}) and G_{2}^{S} = (N^{±}, w_{2}^{S}) = S-closure(G_{2}) (so that w = w_{R}^{S} = w_{2}^{S}).

As G_{R} ◁ G_{2}, there exists i, j ∈ N^{±} such that w_{R}(i, j) < w_{2}(i, j); as G_{2}^{c} and G are closed, w_{2}^{c}(i, i) = w(i, i) = 0 so that we can assume that i ≠ j. Moreover w_{R}(i, j) < +∞ so that, as G_{R} is a subgraph of G, w_{R}(i, j) = w(i, j); as closure is both idempotent and reductive, G = closure(G) ⊴ G_{R}^{c} ⊴ G_{R}; hence we have

w(i, j) = w_{R}^{c}(i, j) = w_{R}(i, j).

Since G_{R} ◁ G_{2} we have G_{R}^{c} ⊴ G_{2}^{c} so that w(i, j) ≤ w_{2}^{c}(i, j).

Suppose first that w(i, j) < w_{2}^{c}(i, j). By Theorem 3, since S-closure(G_{2}^{c}) = G, we have 2w(i, j) = w_{2}^{c}(i, \overline{ı}) + w_{2}^{c}(\overline{ȷ}, j). Hence, 2w(i, j) = w(i, \overline{ı}) + w(\overline{ȷ}, j), so that i ≠ \overline{ȷ}, (i, \overline{ı}) and (\overline{ȷ}, j) are arcs in G and, by Definition 9, arc (i, j) is not strongly atomic in G. Hence, since (i, j) is an arc in G_{R}, it must be i ≡_{G} j, so that i, j are in the same equivalence class E and (i, j) is an arc in Z; thus, as i ≠ j, either i or j is not the leader of E; without loss of generality, we assume that i is not the leader. Since w = w_{2}^{S} = w_{R}^{S}, we have w(i, \overline{ı}) = w_{2}^{S}(i, \overline{ı}) = w_{R}^{S}(i, \overline{ı}). By Theorem 3, w_{2}^{S}(i, \overline{ı}) = w_{2}^{c}(i, \overline{ı}) and w_{R}^{S}(i, \overline{ı}) = w_{R}^{c}(i, \overline{ı}); hence w(i, \overline{ı}) = w_{2}^{c}(i, \overline{ı}) = w_{R}^{c}(i, \overline{ı}). By Lemma 7, there exists π_{i} = i ⋯ \overline{ı} in G_{2} such that

w_{2}(π_{i}) = w_{2}^{c}(i, \overline{ı}) = w(i, \overline{ı}) ≤ w_{R}(π_{i}),

where the last inequality follows from Lemma 5 and by closure being a reductive operator. Note that as G_{R} ◁ G_{2}, π_{i} must also be a path in G_{R}. By Definition 10 and the assumption that i is not a leader of E, if, for some h ∈ N^{±}, (i, h) is an arc in G_{R}, then h = j; hence π_{i} = (ij) ⋯ \overline{ı}; also, as G_{R} ◁ G_{2}, for all h_{1}, h_{2} ∈ N^{±}, w_{2}(h_{1}, h_{2}) ≥ w_{R}(h_{1}, h_{2}); hence w_{2}(π_{i}) > w_{R}(π_{i}) which is a contradiction.

Suppose now that w(i, j) = w_{2}^{c}(i, j) so that w_{2}^{c}(i, j) < w_{2}(i, j). By Lemma 7, there exists π = i ⋯ j in G_{2} such that

w_{2}(π) = w_{2}^{c}(i, j) = w(i, j) < w_{2}(i, j).

As w_{2}(π) < w_{2}(i, j), there exists k ∈ N^{±} such that π = (ik) :: π′ for some path π′ = k ⋯ j in G_{2}. Since (i, j) is an arc in G_{R}, by Definitions 9 and 10, w(i, j) < w(i, k) + w(k, j). As G is closed, by Lemma 5, w(k, j) ≤ w(π′) and hence w(i, j) < w(i, k)+w(π′) = w(π); and therefore w_{2}(π) < w(π), contradicting G ◁ G_{2}. ⊓ ⊔

A.4 Proofs of the Results Stated in Section 4.2

The standard widening operator ‘∇_{s}’ for topologically closed convex polyhedra defined in the PhD thesis of N. Halbwachs [19, Définition 5.3.3, p. 57] is slightly different from the specification originally proposed in [2], in that the former does not depend on the particular constraint systems chosen for representing the arguments of the widening. Nonetheless, the following result, which is taken from [33], states that the two definitions happen to be equivalent when applied to polyhedra S_{1} and S_{2} such that S_{1} ⊆ S_{2} and dim(S_{1}) = dim(S_{2}).

Proposition 1 Let S_{1}, S_{2} ⊆ ℝ^{n} be two topologically closed convex polyhedra such that ∅ ≠ S_{1} ⊆ S_{2} and dim(S_{1}) = dim(S_{2}). Let also C_{1} be a finite system of non-strict linear inequalities describing S_{1} and suppose that C_{1} contains no redundant constraint. Then the result of the standard widening S_{1} ∇_{s} S_{2} is described by the constraint system

C_{s} := { β ∈ C_{1} | all the points in S_{2} satisfy β }.

Proof See the proof in [33, Proposition 6]. ⊓ ⊔

Proof (of Theorem 2 on page 15) Let S_{1}, S_{2} ∈ ℘(ℝ^{n}), where ∅ ≠ S_{1} ⊆ S_{2}, be two octagonal shapes represented by the strongly reduced octagonal graph G_{1} and the strongly closed octagonal graph G_{2}, respectively. Let also G = G_{1} ∇G_{2} = (N^{±}, w) and S the octagonal shape represented by G. Let C_{1}, C_{2} and C be the systems of octagonal constraints encoded by G_{1}, G_{2} and G, respectively. Note that, in such a construction, each pair of coherent arcs generates a single octagonal constraint. Since the octagonal graph G_{1} is strongly reduced, the corresponding constraint system C_{1} contains no redundant constraints.

We first assume dim(S_{1}) = dim(S_{2}) so that, by Definition 11, S_{1} ∇ S_{2} = S. We will show that S = S_{1} ∇_{s} S_{2}. Let C_{s} be as defined in Proposition 1. Then it follows from Proposition 1 that to prove S = S_{1} ∇_{s} S_{2}, we just need to show that C = C_{s}. To prove C ⊆ C_{s}, suppose that β = (v_{i} − v_{j} ≤ d_{1}) ∈ C, so that w(i, j) = d_{1} < +∞. Then, by Definition 2, w_{1}(i, j) = d_{1} and w_{2}(i, j) = d_{2} ≤ d_{1}. Thus, there exists γ = (v_{i} − v_{j} ≤ d_{2}) ∈ C_{2}. Since all the points of S_{2} satisfy γ, they also satisfy β and hence, β ∈ C_{s}. To prove the other inclusion C_{s} ⊆ C, suppose that β = (v_{i} − v_{j} ≤ d_{1}) ∈ C_{s} so that, since C_{s} ⊆ C_{1} and C_{1} contains no redundancies, we have w_{1}(i, j) = d_{1}. By definition of C_{s}, all the points of S_{2} satisfy β. Since the octagonal graph G_{2} is strongly closed, there exists γ = (v_{i} − v_{j} ≤ d_{2}) ∈ C_{2} such that d_{1} ≥ d_{2}. Hence, w_{1}(i, j) ≥ w_{2}(i, j) and, by Definition 2, we obtain β ∈ C.

Suppose now that dim(S_{1}) ≠ dim(S_{2}). By hypothesis, S_{1} ⊆ S_{2} so that dim(S_{1}) < dim(S_{2}). Then, by Definition 11, S_{1} ∇ S_{2} = S_{2}. Since the standard widening ‘∇_{s}’ is an upper bound operator, we obtain S_{1} ∇ S_{2} ⊆ S_{1} ∇_{s} S_{2}.

Thus, in both cases the operator ‘∇’ computes an upper bound of its arguments which is at least as precise as the upper bound computed by the standard widening ‘∇_{s}’. To complete the proof, we only have to show that ‘∇’ is a proper widening operator, i.e., it enforces the convergence of any abstract iteration sequence. This property is easily shown to hold by the observation, made above, that the operator of Definition 11 can behave differently from the standard widening only when there is a strict increase in the affine dimension of the arguments. Since such an increase can only happen a finite number of times, the operator ‘∇’ inherits the convergence guarantee of ‘∇_{s}’. ⊓ ⊔

A.5 Proof of Theorem 6 on page 21

The following two lemmas are simple adaptations of Lemma 3 and Lemma 19 to the case of tightly closed graphs.

Lemma 24 Let L and E be the non-singular leaders’ subgraph and the zero-equivalence subgraph of the tightly closed graph G, respectively. Then, L and E are tightly closed graphs and L is zero-cycle free.

Proof Since G is tightly closed, it is also strongly closed. Hence, by Lemma 3, the graphs L and E are strongly closed octagonal graphs and E is zero-cycle free. Since they are subgraphs of G, which is tightly closed, L and E are integer graphs and satisfy property (8) of Definition 13, so that they are tightly closed too. ⊓ ⊔

Lemma 25 Let G be a tightly closed and zero-cycle free graph and A = (N^{±}, w_{A}) be its tightly atomic subgraph; let also U = (N^{±}, w_{U}) be the untightening of A. Then U is an integer octagonal subgraph of G and T-closure(U) = G.

Proof Since G is tightly closed, it is also strongly closed so that, by Lemma 19, A is an octagonal subgraph of G and S-closure(A) = G; as G is tightly closed, we obtain T-closure(A) = G.

By Definition 15, U is an octagonal subgraph of A; hence, U is an integer octagonal subgraph of G. Since G ⊴ U, by monotonicity and idempotency, G ⊴ T-closure(U). Therefore, to prove T-closure(U) = G, we just need to show that T-closure(U) ⊴ G.

Let A = (N^{±}, w_{A}), U = (N^{±}, w_{U}) and U_{T} = (N^{±}, w_{T}) = T-closure(U); we prove that U_{T} ⊴ A. Let i, j ∈ N^{±} be any pair of nodes. If w_{U}(i, j) ≤ w_{A}(i, j) then, since tight closure is a reductive operator, w_{T}(i, j) ≤ w_{A}(i, j). On the other hand, by Definition 15, if w_{U}(i, j) > w_{A}(i, j), then we have that j = \overline{ı}, w_{A}(i, \overline{ı}) is even and there exists k ∈ N^{±} \ \{i, \overline{ı}\} such that w_{A}(i, k)+w_{A}(k, \overline{ı}) ≤ w_{A}(i, \overline{ı})+1. Note that, by Definition 15 and reductivity of tight closure, we have w_{T}(i, k) ≤ w_{U}(i, k) = w_{A}(i, k) and w_{T}(k, \overline{ı}) ≤ w_{U}(k, \overline{ı}) = w_{A}(k, \overline{ı}). Since U_{T} is tightly closed, by property (2) of Definition 1, we obtain

w_{T}(i, \overline{ı}) ≤ w_{T}(i, k) + w_{T}(k, \overline{ı})
≤ w_{A}(i, k) + w_{A}(k, \overline{ı})
≤ w_{A}(i, \overline{ı}) + 1.

Note that w_{A}(i, \overline{ı}) + 1 is an odd integer and, by property (8) of Definition 13, w_{T}(i, \overline{ı}) is even, so that we obtain w_{T}(i, \overline{ı}) ≤ w_{A}(i, \overline{ı}).

Hence, U_{T} ⊴ A and, since the tight closure operator is monotonic and idempotent, we obtain U_{T} = T-closure(U_{T}) ⊴ T-closure(A) = G, completing the proof. ⊓ ⊔

The following proof of Theorem 6 is a simple adaptation of the proof of Theorem 1, exploiting the two lemmas above.

Proof (of Theorem 6 on page 21) Let G = (N^{±}, w) be the tight closure of the input integer octagonal graph, computed at step 1 of the tight reduction procedure; let L = (N^{±}, w_{L}) be the non-singular leaders’ subgraph of G; E = (N^{±}, w_{E}) the zero-equivalence subgraph of G; A = (N^{±}, w_{A}) the strongly atomic subgraph of L; U = (N^{±}, w_{U}) the untightening of A; Z = (N^{±}, w_{Z}) the zero-equivalence reduction of E; G_{R} = (N^{±}, w_{R}) = U ⊓ Z; and G_{R}^{T} = (N^{±}, w_{R}^{T}) = T-closure(G_{R}). Then we need to show that G_{R} is a tightly reduced octagonal graph and G_{R}^{T} = G.

By Definition 8 and Lemma 24, both L and E are octagonal subgraphs of G. By Lemma 25, U is an octagonal subgraph of L and, by Lemma 20, Z is an octagonal subgraph of E; hence U and Z are octagonal subgraphs of G. Hence, G_{R} = U ⊓ Z is an octagonal subgraph of G.

Next we show G_{R}^{T} = G. By Lemma 24, L and E are tightly closed and L is zero-cycle free; by Lemma 25, T-closure(U) = L; by Lemma 23, S-closure(Z) = E, hence T-closure(Z) = E. Thus, we have

G_{R}^{T} = T-closure(T-closure(U ⊓ Z))

= T-closure(T-closure(U) ⊓ T-closure(Z))

= T-closure(L ⊓ E).

As observed before, L and E are subgraphs of G and hence G ⊴ G_{R}^{T}. It remains to show that G_{R}^{T} ⊴ G. Let (i, j) be an arc in G and suppose that i ∈ E_{i} and j ∈ E_{j}, where E_{i} and E_{j} are zero-equivalence classes for G. Then, to prove that G_{R}^{T} ⊴ G, we just need to show that

w_{R}^{T}(i, j) ≤ w(i, j).  (26)

To do this, without loss of generality, we need to consider three cases:

1. E_{i} and E_{j} are singular zero-equivalence classes in G;

2. E_{i} is singular and E_{j} is a non-singular zero-equivalence class in G;

3. E_{i} and E_{j} are non-singular zero-equivalence classes in G.

Case 1. By Lemma 2, E_{i} = E_{j} so that w(i, j) = w_{E}(i, j). Therefore, as w_{R}^{T}(i, j) ≤ w_{E}(i, j), Equation (26) holds.

Case 2. Let ℓ_{j} ∈ N^{±} be the leader of E_{j} so that \overline{ℓ}_{j} is the leader of the non-singular zero-equivalence class \overline{E}_{j}. By Definition 8,

\begin{aligned}w(i, \overline{ı}) & = w_{E}(i, \overline{ı}), & w(\overline{ȷ}, \overline{ℓ}_{j}) & = w_{E}(\overline{ȷ}, \overline{ℓ}_{j}), \\ w(ℓ_{j}, j) & = w_{E}(ℓ_{j}, j), & w(\overline{ℓ}_{j}, ℓ_{j}) & = w_{L}(\overline{ℓ}_{j}, ℓ_{j}). \end{aligned}  (27)

By Lemma 13,

w(\overline{ȷ}, j) = w(\overline{ȷ}, \overline{ℓ}_{j}) + w(\overline{ℓ}_{j}, j)
= w(\overline{ȷ}, \overline{ℓ}_{j}) + w(\overline{ℓ}_{j}, ℓ_{j}) + w(ℓ_{j}, j)

so that, by Lemma 14 and Equation (27),

2w(i, j) = w(i, \overline{ı}) + w(\overline{ȷ}, j)
= w(i, \overline{ı}) + w(\overline{ȷ}, \overline{ℓ}_{j}) + w(\overline{ℓ}_{j}, ℓ_{j}) + w(ℓ_{j}, j)
= w_{E}(i, \overline{ı}) + w_{E}(\overline{ȷ}, \overline{ℓ}_{j}) + w_{L}(\overline{ℓ}_{j}, ℓ_{j}) + w_{E}(ℓ_{j}, j).

Moreover, by Lemma 5,

2w_{R}^{T}(i, j) ≤ w_{R}^{T}(i, \overline{ı}) + w_{R}^{T}(\overline{ȷ}, \overline{ℓ}_{j}) + w_{R}^{T}(\overline{ℓ}_{j}, ℓ_{j}) + w_{R}^{T}(ℓ_{j}, j)
≤ w_{E}(i, \overline{ı}) + w_{E}(\overline{ȷ}, \overline{ℓ}_{j}) + w_{L}(\overline{ℓ}_{j}, ℓ_{j}) + w_{E}(ℓ_{j}, j)

since G_{R}^{T} ⊴ L and G_{R}^{T} ⊴ E. Therefore Equation (26) holds.

Case 3. By Definition 8,

w(i, ℓ_{i}) = w_{E}(i, ℓ_{i}), w(ℓ_{j}, j) = w_{E}(ℓ_{j}, j), w(ℓ_{i}, ℓ_{j}) = w_{L}(ℓ_{i}, ℓ_{j}).

Therefore, by Lemma 13,

w(i, j) = w(i, ℓ_{i}) + w(ℓ_{i}, j)
= w(i, ℓ_{i}) + w(ℓ_{i}, ℓ_{j}) + w(ℓ_{j}, j)
= w_{E}(i, ℓ_{i}) + w_{L}(ℓ_{i}, ℓ_{j}) + w_{E}(ℓ_{j}, j).

Moreover, by Lemma 5,

w_{R}^{T}(i, j) ≤ w_{R}^{T}(i, ℓ_{i}) + w_{R}^{T}(ℓ_{i}, ℓ_{j}) + w_{R}^{T}(ℓ_{j}, j)
≤ w_{E}(i, ℓ_{i}) + w_{L}(ℓ_{i}, ℓ_{j}) + w_{E}(ℓ_{j}, j),

since G_{R}^{T} ⊴ L and G_{R}^{T} ⊴ E. Therefore Equation (26) holds and hence G_{R}^{T} = G.

Finally, to show that G_{R} is tightly reduced as specified in Definition 14, having already shown that G_{R} is a subgraph of T-closure(G_{R}) = G, we assume there exists a proper octagonal subgraph G_{2} = (N^{±}, w_{2}) of G_{R} such that G = T-closure(G_{2}) and derive a contradiction.

Let G_{2}^{c} = (N^{±}, w_{2}^{c}) = closure(G_{2}), G_{R}^{c} = (N^{±}, w_{R}^{c}) = closure(G_{R}) and G_{2}^{T} = (N^{±}, w_{2}^{T}) = T-closure(G_{2}) (so that w = w_{R}^{T} = w_{2}^{T}). As G_{2} is a proper octagonal subgraph of G_{R}, there exists i, j ∈ N^{±} such that w_{R}(i, j) < w_{2}(i, j) = +∞; as G_{2}^{c} and G are closed, w_{2}^{c}(i, i) = w(i, i) = 0 so that we can assume that i ≠ j. Moreover w_{R}(i, j) < +∞ so that, as G_{R} is a subgraph of G, w_{R}(i, j) = w(i, j); as closure is both idempotent and reductive, G = closure(G) ⊴ G_{R}^{c} ⊴ G_{R}; hence we have

w(i, j) = w_{R}^{c}(i, j) = w_{R}(i, j).

Since G_{R} ◁ G_{2} we have G_{R}^{c} ⊴ G_{2}^{c} so that w(i, j) ≤ w_{2}^{c}(i, j).

Suppose first that w(i, j) < w_{2}^{c}(i, j). By Theorem 4, since T-closure(G_{2}^{c}) = G, we have

w(i, j) = ⌊ \frac{w_{2}^{c}(i, \overline{ı})}{2} ⌋ + ⌊ \frac{w_{2}^{c}(\overline{ȷ}, j)}{2} ⌋.

Hence, w(i, j) = ⌊ \frac{w(i,\overline{ı})}{2} ⌋ + ⌊ \frac{w(\overline{ȷ},j)}{2} ⌋. By property (8) of Definition 13, both w(i, \overline{ı}) and w(\overline{ȷ}, j) are even integers, so that 2w(i, j) = w(i, \overline{ı}) + w(\overline{ȷ}, j). Therefore, i ≠ \overline{ȷ} and the two arcs (i, \overline{ı}) and (\overline{ȷ}, j) are in G; thus, by Definition 9, arc (i, j) is not strongly atomic in G, so that (i, j) is not an arc in L; hence, it is neither an arc in U. Since (i, j) is a proper arc in G_{R} = U ⊓ Z, it must be an arc in Z, so that i and j are in the same equivalence class E (i.e., i ≡_{G} j). As i ≠ j, either i or j is not the leader of E; without loss of generality, we assume that i is not the leader. By Definition 10, in G_{R} the only arc exiting from node i is (i, j); since w_{2}(i, j) = +∞ and G_{2} is a subgraph of G_{R}, there is no arc in G_{2} exiting from i, so that i and j cannot belong to the same 0-weight loop; hence i ≢_{G_{2}} j and G ≠ G_{2}^{T}, which is a contradiction.

Suppose now that w(i, j) = w_{2}^{c}(i, j) so that w_{2}^{c}(i, j) < w_{2}(i, j). By Lemma 7, there exists π = i ⋯ j in G_{2} such that

w_{2}(π) = w_{2}^{c}(i, j) = w(i, j) < w_{2}(i, j).

As w_{2}(π) < w_{2}(i, j), there exists k ∈ N^{±} such that π = (ik) :: π′ for some path π′ = k ⋯ j in G_{2}. Since (i, j) is an arc in G_{R}, by Definitions 9 and 10, w(i, j) < w(i, k) + w(k, j). As G is closed, by Lemma 5, w(k, j) ≤ w(π′) and hence w(i, j) < w(i, k)+w(π′) = w(π); and therefore w_{2}(π) < w(π), contradicting G ◁ G_{2}. ⊓ ⊔