Widening Operators for Weakly-Relational Numeric Abstractions^{⋆}

Roberto Bagnara^{1}, Patricia M. Hill^{2}, Elena Mazzi^{1}, and Enea Zaffanella^{1}

1 Department of Mathematics, University of Parma, Italy

            {bagnara,mazzi,zaffanella}@cs.unipr.it

2 School of Computing, University of Leeds, UK

                    hill@comp.leeds.ac.uk

Abstract. We discuss the construction of proper widening operators on several weakly-relational numeric abstractions. Our proposal differs from previous ones in that we actually consider the semantic abstract domains, whose elements are geometric shapes, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices. Since the closure by entailment operator preserves geometric shapes, but not their syntactic expressions, our widenings are immune from the divergence issues that could be faced by the previous approaches when interleaving the applications of widening and closure. The new widenings, which are variations of the standard widening for convex polyhedra defined by Cousot and Halbwachs, can be made as precise as the previous proposals working on the syntactic domains. The implementation of each new widening relies on the availability of an effective reduction procedure for the considered constraint description: we provide such an algorithm for the domain of octagonal shapes.

1 Introduction

Numerical properties are of great interest in the broad area of formal methods for their complete generality and since they often play a crucial role 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, the most famous ones are probably the (non-relational) abstract domain of intervals [16] and the (relational) abstract domain of convex polyhedra [19]. As far as the efficiency/precision trade-off is concerned, these domains occupy the opposite extremes of the spectrum: on the one hand, the operations on convex

⋆ 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.

polyhedra achieve a significant level of precision, which is however countered by a worst-case exponential time complexity, often leading to scalability problems; 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 somehow 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 [26, 33], the octagon abstract domain [27], the ‘two variables per inequality’ abstract domain [34], the octahedron abstract domain [15], and the abstract domain of template constraint matrices [32]. 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] and the zone congruence abstract domain [28].

In this paper, we address the issue of the provision of proper widening operators for these domains. 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 [19, 22]. 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 [33]. Unfortunately, as pointed out in [26, 27], 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 [33] 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 [26, 27] to apply the same operator given in [33] 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 this 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 octagonal shapes.

As a by-product of our work on verifying the correctness of this reduction algorithm, we noticed that the algorithm for computing the strong closure of octagonal graphs as described in [26] could be simplified with a consequential improvement in its efficiency. This revised strong closure algorithm is also described here.

The paper is structured as follows: Section 2 recalls the required concepts and notations; Section 3 introduces the domain of bounded difference graphs; a domain of bounded difference shapes is presented in Section 4, where an alternative solution to the divergence problem is proposed; the generalization of the above results to the case of octagons is the subject of Section 5, where we define a new strong reduction procedure and an improved strong closure procedure for octagonal graphs, as well as a semantic widening operator for octagonal shapes. Section 6 argues in favor of the adoption of semantic abstract domains, as opposed to syntactic ones, also discussing some related work. Section 7 concludes. Appendix A, which is not meant to be part of the paper and is included for the convenience of the reviewers, contains the proofs of all the stated results.

2 Preliminaries

The reader is assumed to be familiar with the fundamental concepts of lattice theory [12] and abstract interpretation theory [17, 18]. We refer the reader to the classical works on the numeric domains of intervals [16] and convex polyhedra [19] for the specification of the corresponding widening operators.

Let ℚ_{∞} := ℚ ∪ {+∞} be totally ordered by the extension of ‘<’ such that d < +∞ for each d ∈ ℚ. Let N be a finite set of nodes. A weighted directed graph (graph, for short) G in N is a pair (N , w), where w: N ×N → ℚ_{∞} is the weight function for G. A pair (n_{i}, n_{j}) ∈ N × N is an arc of G if w(n_{i}, n_{j}) < +∞; the arc is proper if n_{i} ≠ n_{j}.

A path π = n_{0} ⋯ n_{p} in a graph G = (N , w) is a 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 arc (n_{i−1}, n_{i}) where i = 1, …, p is said to be in the path π. The path π is proper if all the arcs in it are proper. The path π is a proper cycle if it is a proper path and n_{0} = n_{p} (so that p ≥ 2). 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 a zero-cycle if it is a proper cycle with 0 weight. A graph is consistent if it has no negative weight cycles; it is zero-cycle free if all its proper cycles have strictly positive weights.

The set 𝔾 of consistent graphs in N is partially ordered by the relation ‘⊴’ defined, for all G_{1} = (N , w_{1}) and G_{2} = (N , w_{2}), by

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

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

Definition 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^{c} ∈ 𝔾 | G^{c} ⊴ G and G^{c} is closed }.

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 𝔾_{⊥}.

3 Systems of Bounded Differences

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 [11], 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. Systems of bounded differences have been used by the artificial intelligence community as a way to reason about temporal quantities [2, 20], 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 [21, 25]. In the abstract interpretation field, the idea of using an abstract domain of bounded differences was put forward in [3].

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 0 ∉ V is the special variable, N_{0} = {0} ∪ V, 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) [11]. However, this representation provides no conceptual advantage over the isomorphic graph (or constraint network [20]) 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 [33], 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; since, basically, it corresponds to the closure by entailment of the encoded system of bounded differences. In [33] 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 [16], or as a restriction on the domain of closed BDGs of the standard widening defined on the abstract domain of convex polyhedra [19, 22]: 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 [26, 27], when used in conjunction with shortestpath 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.^{3} 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 [26]. Differently from [33], in [26] 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 [33] is also used in [26]; however, it is observed that this widening “could have intriguing interactions” with shortest-path closure, therefore identifying the divergence issue faced

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

in [33]. This observation has led the author of [26] to concluding that “fixpoint computations must be performed” in the lattice of BDGs, without enforcing closure (emphasis in the original).

4 Bounded Difference Shapes

While the analysis of the divergence problem is absolutely correct, the solution identified in [26] 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 6.

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, a crucial requirement in the specification of the standard widening is that the first argument polyhedron is described by a non-redundant system of constraints [6, 7]. 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 the use of a maximal BDG in the equivalence class of BDGs representing the same geometric shape; 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}).

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 [25] and called shortest-path reduction. Basically, it is an extension of the transitive reduction algorithm of [1] 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 shortestpath reduction algorithm of [25] 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.

4.1 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 [26] 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 [23, 24] or its variation called ‘staged widening with thresholds’ [13, 14, 30]: 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 [6, 7].

5 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 [15, 27, 32, 34]. 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 the minimization algorithm for arbitrary linear inequality constraints is not efficient enough. In this section we provide such a reduction procedure for the octagon abstract domain [27].

The octagon abstract domain allows for the manipulation of octagonal constraints of the form av_{i} + bv_{j} ≤ c, where a, b ∈ {−1, 0, +1} (the same class of constraints was considered in [10], where octagons were called simple sections). Bounded differences can then be used to express octagonal constraints by splitting each variable v_{i} ∈ V into two forms: a positive form v_{i}^{+}, interpreted as +v_{i}; and a negative form v_{i}^{−}, interpreted as −v_{i}. Thus, an octagonal constraint such as v_{i} +v_{j} ≤ d can be translated into the bounded difference constraint v_{i}^{+} −v_{j}^{−} ≤ d; alternatively, the same constraint can be translated into v_{j}^{+} − v_{i}^{−} ≤ d. Note that unary (octagonal) constraints such as v_{i} ≤ d and −v_{j} ≤ d can be encoded as v_{i}^{+} − v_{i}^{−} ≤ 2d and v_{j}^{−} − v_{j}^{+} ≤ 2d, respectively, so that the special variable 0 is no longer needed.

In the following we assume that N^{±} = {0, …, 2n−1} is a fixed and finite set of nodes where, for all i = 0, …, n − 1, the node 2i represents the positive form v_{i}^{+} and 2i + 1 the negative form v_{i}^{−} of the variable v_{i}. Moreover, for all i ∈ N^{±}, \overline{ı} denotes i+1 if i is even, and i−1 if i is odd. Thus, for all i ∈ N^{±}, we also have \overline{ı} ∈ N^{±} and \overline{\overline{ı}} = i. Therefore, any finite system of octagonal constraints on the n variables V = {v_{0}, …, v_{n−1}} can be represented by a weighted directed graph on the 2n nodes N^{±}. Note that, for any i, j ∈ N^{±}, as arcs (i, j) and (\overline{ȷ}, \overline{ı}) denote equivalent expressions, the pair is said to be coherent. We restrict attention to consistent systems of constraints and hence to consistent graphs where coherent pairs of arcs have the same weight.

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{ı}).  (3)

Thus any octagonal graph on the 2n nodes N^{±} encodes a consistent system of octagonal constraints on n variables. The set 𝕆 of all octagonal graphs (with the usual addition of the bottom element, representing the empty octagon) is a sub-lattice of 𝔾_{⊥}, sharing the same least upper bound and greatest lower bound operators. Note that, at the implementation level, coherence can be automatically and efficiently enforced by letting arc (i, j) and arc (\overline{ȷ}, \overline{ı}) share the same representation.

The octagon abstract domain developed in [27] is thus a syntactic domain having octagonal graphs as elements. When dealing with octagonal graphs, one has to remember the relation linking the positive and negative forms of each variable: in particular, besides transitivity, a proper closure by entailment procedure should also consider the following inference rule:

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

Thus, the standard shortest-path closure algorithm is not enough to obtain a canonical form for octagonal graphs: to this end, a modified closure procedure is defined in [27], yielding strongly closed octagonal graphs.

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).  (5)

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

Closure(G) := ⨆{ G^{C} ∈ 𝕆 | G^{C} ⊴ G and G^{C} is strongly closed }.

Similarly to shortest-path closure, strong closure is a kernel operator on the lattice of octagonal graphs.

By repeating the reasoning of the previous section, 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}, we have Closure(G_{1}) ≠ Closure(G_{2}). A strong reduction for the octagonal graph G is any strongly reduced octagonal graph G_{R} such that Closure(G) = Closure(G_{R}).

Note that, in the above definition, we only compare G_{1} with other octagonal graphs. Thus, we explicitly disregard 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.

5.1 A Strong Reduction Procedure for Octagonal Graphs

In this section we generalize the shortest-path reduction algorithm of [25] so as to obtain a strong reduction procedure for octagonal graphs. Clearly, the algorithm of [25] cannot be used without modifications, since it takes no account of the redundancies caused by the new constraint inference rule (4). Nonetheless, the high-level structure of the strong reduction procedure is the same as that defined in [25] 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 the strong closure procedure defined in [27].

Step 2 is also easily implemented by observing that, in a strongly closed octagonal graph, equality constraints correspond to proper 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 zero-equivalence class for G. Then \overline{E} := \{ \overline{ı} ∈ N^{±} | i ∈ E \} is also a zeroequivalence 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 zero-equivalence 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 [25], the first subgraph resulting from the decomposition, relating nodes in different zero-equivalence classes, is obtained by only connecting the leaders. However, we do not connect the leader of the singular zero-equivalence class 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.) Let G = (N^{±}, w) be a strongly closed octagonal graph and L ⊆ N^{±} the set of leaders of the non-singular zero-equivalence classes for G. The non-singular

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.

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

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 zeroequivalence 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 zero-equivalence 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 [25]: 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 zero-equivalence 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

\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

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 zero-equivalence 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.

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

The following definition formalizes the above observations.

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, the strong reduction algorithm computes its strong reduction.

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 [25], once the ordering of variables is fixed, the strong reduction algorithm returns a canonical form for octagonal graphs.

5.2 An Improved Strong Closure Algorithm

The formal proof of Theorem 1 led to a new result regarding the strong closure operator for octagonal graphs. The strong closure algorithm formalized in [27, 31] performs n local propagation steps: in each step, the classical constraint propagation of the Floyd-Warshall algorithm is followed by another constraint propagation corresponding to the new inference rule (4). A finely tuned implementation of this algorithm [29] performs 10n^{3} + 14n^{2} coefficient additions and 10n^{3} + 11n^{2} coefficient comparisons, where n is the dimension of the vector space. It turns out that the interleaving of the two kinds of propagation steps is not needed: the same final result can be obtained by the application of the classical Floyd-Warshall closure algorithm followed by a single local propagation step using the constraint inference rule (4).

Theorem 2. Let G^{c} = (N^{±}, w^{c}) 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^{c}(i, j), w^{c}(i, \overline{ı})/2 + w^{c}(\overline{ȷ}, j)/2\}.

Then G^{S} = Closure(G^{c}).

When applied to the strong closure algorithm of [29], this optimization saves 2n^{3} − 2n additions and 2n^{3} − 3n comparisons: for n ≥ 5, the saving is between 15% and 20% of the total number of these operations.

5.3 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 minor variant, we obtain a “truly semantic” widening operator 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}. 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 3. 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 [22]. 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}.

The definition of a semantic widening for the domain of BDSs is obtained by simply replacing, in Definition 11, the strongly reduced and strongly closed octagonal graph representations with the reduced and closed BDG representations, respectively. Then a result similar to Theorem 3 holds for BDSs.

6 Discussion

In the previous sections 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 [26, Section 5] where the domain of BDGs is compared to the domain of closed BDGs.^{5} For instance, it

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

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 [26, Section 5] makes clear that the solution to the divergence problem for the abstract iteration sequence was the one and only 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 [9] (PPL, http://www.cs.unipr.it/ppl), free software distributed under the GNU General Public License; future releases of the library will support computations on the domains of BDSs and octagonal shapes.

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 [8] 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 [8], 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.

6.1 Related Work

The shortest-path reduction algorithm of [25] has also been recently considered in the PhD thesis of A. Miné [31]. In such a context, the reduction procedure is used as a tool for the computation of hollow (i.e., sparse) representations for BDGs, so as to obtain memory space savings. The author appears not to identify the positive interaction between reduction and widening and, as a consequences, he conjectures that the computation of hollow representations could compromise the convergence of the abstract iteration sequence (see [31, Section 3.8.2]). An adaptation of the reduction algorithm for the case of octagonal graphs is defined in [31, Section 4.5.2] although this differs from the one proposed in Section 5.1. It turns out that the algorithm of [31, 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.

6.2 A Note on Floating-Point Computations

The theoretical results concerning weighted directed graphs hold when the data type adopted for the representation of weights allows for exact computations. If a bounded precision floating-point data type is considered, then most of these results will be broken.

A careful implementation, that rounds on the safe side, may ensure that the shortest-path closure and reduction algorithms, as well as their strong versions working on octagonal graphs, will map a graph representation into another graph representation encoding the same geometric shape. However, due to rounding errors, these procedures will no longer provide canonical representations for the underlying semantic objects: different closed/reduced graphs may still encode the same geometric shape. Thus the implementation of a truly semantic abstract domain is not possible using only bounded precision floating-point computations. Nonetheless, by quotienting the syntactic domain of graph representations according to the 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.

It should also be observed that an abstract domain of BDGs or octagonal graphs having weights in any bounded precision floating-point data type will have a finite cardinality. In such a case, any upper bound operator can be used as a widening.

7 Conclusions

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 easily derived for several weakly-relational numeric abstractions, including the domain of bounded difference shapes and octagonal shapes. For what concerns the efficient representation of octagonal shapes by means of octagonal graphs, we have specified and proved correct a strong reduction procedure, as well as a more efficient strong closure procedure.

References

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

2. J. F. Allen and H. A. Kautz. A model of naive temporal reasoning. In J. R. Hobbs and R. Moore, editors, Formal Theories of the Commonsense World, pages 251–268. Ablex, Norwood, NJ, 1985.

3. R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, March 1997. Printed as Report TD-1/97.

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

5. R. Bagnara, R. Giacobazzi, and G. Levi. An application of constraint propagation to data-flow analysis. In Proceedings of “The Ninth Conference on Artificial Intelligence for Applications”, pages 270–276, Orlando, Florida, March 1993. IEEE Computer Society Press, Los Alamitos, CA.

6. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337–354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.

7. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Science of Computer Programming, 2005. To appear.

8. R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. In B. Steffen and G. Levi, editors, Verification, Model Checking and Abstract Interpretation: Proceedings of the 5th International Conference (VMCAI 2004), volume 2937 of Lecture Notes in Computer Science, pages 135–148, Venice, Italy, 2003. Springer-Verlag, Berlin.

9. R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library User’s Manual. Department of Mathematics, University of Parma, Parma, Italy, release 0.7 edition, December 2004. Available at http://www.cs.unipr.it/ppl/.

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

11. R. Bellman. Dynamic Programming. Princeton University Press, 1957.

12. G. Birkhoff. Lattice Theory, volume XXV of Colloquium Publications. American Mathematical Society, Providence, Rhode Island, USA, third edition, 1967.

13. B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In T. Æ. Mogensen, D. A. Schmidt, and I. Hal Sudborough, editors, The Essence of Computation, volume 2566 of Lecture Notes in Computer Science, pages 85–108. Springer-Verlag, Berlin, 2002.

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

15. R. Clarisó and J. Cortadella. The octahedron abstract domain. In R. Giacobazzi, editor, Static Analysis: Proceedings of the 11th International Symposium, volume 3148 of Lecture Notes in Computer Science, pages 312–327, Verona, Italy, 2004. Springer-Verlag, Berlin.

16. P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In B. Robinet, editor, Proceedings of the Second International Symposium on Programming, pages 106–130. Dunod, Paris, France, 1976.

17. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, New York, 1977. ACM Press.

18. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pages 269–282, New York, 1979. ACM Press.

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

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

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

22. N. Halbwachs. 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, March 1979.

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

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

25. K. Larsen, F. Larsson, P. Pettersson, and W. Yi. 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), pages 14–24, San Francisco, CA, 1997. IEEE Computer Society Press.

26. A. Miné. A new numerical abstract domain based on difference-bound matrices. In O. Danvy and A. Filinski, editors, Proceedings of the 2nd Symposium on Programs as Data Objects (PADO 2001), volume 2053 of Lecture Notes in Computer Science, pages 155–172, Aarhus, Denmark, 2001. Springer-Verlag, Berlin.

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

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

29. A. Miné. The Octagon Abstract Domain Library. Semantics and Abstract Interpretation Computer Science Lab., École Normale Supérieure, Paris, France, release 0.9.6 edition, October 2002. Available at http://www.di.ens.fr/~mine/oct/.

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

31. A. Miné. Weakly Relational Numerical Abstract Domains. PhD thesis, École Polytechnique, Paris, France, March 2005.

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

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

34. A. Simon, A. King, and J. M. Howe. Two variables per linear inequality as an abstract domain. In M. Leuschel, editor, Logic Based Program Synthesis and Tranformation, 12th International Workshop, volume 2664 of Lecture Notes in Computer Science, pages 71–89, Madrid, Spain, 2002. Springer-Verlag, Berlin.

A Proofs

This appendix is not meant to be part of the paper. It is included for the convenience of the reviewers only.

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. We nonetheless include their proofs for the sake of completeness.

A.1 Further Notation and Terminology

Let G = (N , w) be a weighted directed graph. If π_{1} = i_{0} ⋯ i_{h} and π_{2} = i_{h} ⋯ i_{p} are paths in G, where 0 ≤ h ≤ p, then the path concatenation π = i_{0} ⋯ i_{h} ⋯ i_{p} of π_{1} and π_{2} is denoted by π_{1} :: π_{2}; if π_{1} = i_{0}i_{1} (so that h = 1), then π_{1} :: π_{2} will also be denoted by i_{0} · π_{2}. Note that path concatenation is not the same as sequence concatenation. Given a path π = i_{0} ⋯ i_{p} in the graph G, for each h = 0, …, p and k = 1, …, p the node i_{h} and arc (i_{k−1}, i_{k}) are said to be in the path π. The path π is simple if each node occurs at most once in π; it is atomic if all the arcs in π are atomic in G.

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) = +∞. If G′ is a subgraph of G, then G ⊴ G′ (the converse does not necessarily hold). We write G ◁ G′ when G ⊴ G′ and G ≠ G′.

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 (3) of Definition 4, w(π) = w(\overline{π}). A path π in G is strongly atomic if all the arcs in π are strongly atomic in G.

A.2 Results on Weighted Directed Graphs

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 π.

Proof. The proof is by induction on p = ∥π∥. If π is a simple path, then let π′ = π. Suppose now that π is not simple, so that π contains a cycle and p > 0. Thus, π = π_{1} :: π_{2} :: π_{3}, where π_{1} = i ⋯ k, π_{2} = k ⋯ k, π_{3} = k ⋯ j and ∥π_{2}∥ > 0. Consider the path π_{1} :: π_{3}, which is a path in G connecting i and j and such that ∥π_{1} :: π_{3}∥ < p. By the inductive hypothesis, there exists a simple path π′ = i ⋯ j in G such that w(π′) ≤ w(π_{1} :: π_{3}) and each arc in π′ is also an arc in π_{1} :: π_{3} (and thus in π). As G is consistent, we have w(π_{2}) ≥ 0 so that

w(π′) ≤ w(π_{1} :: π_{3})
= w(π_{1}) + w(π_{3})
≤ w(π_{1}) + w(π_{2}) + w(π_{3})
= w(π).
⊓ ⊔

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(π).

Proof. The proof is by induction on p = ∥π∥. If p = 0, then i = j and, by property (1) of Definition 1, w(i, i) = 0. Suppose now that p > 0, so that π = i·π′, where π′ = k ⋯ j and ∥π′∥ = p−1. Then, by the inductive hypothesis, w(k, j) ≤ w(π′). By property (2) of Definition 1, w(i, j) ≤ w(i, k)+w(k, j). Hence

w(i, j) ≤ w(i, k) + w(π′) = w(π).

⊓ ⊔

Lemma 6. Let G = (N , w) be a closed graph. Suppose that, for some path π = j_{0} ⋯ j_{p} in G, w(j_{0}, j_{p}) = w(π). For each q, r ∈ {0, …, p} such that q ≤ r, let π_{qr} = j_{q} ⋯ j_{r} be the subpath of π starting from j_{q} and ending in j_{r}. Then, w(j_{q}, j_{r}) = w(π_{qr}).

Proof. Let q, r ∈ {0, …, p} be such that q ≤ r. By Lemma 5, there exists δ ≥ 0 such that w(π_{qr}) = w(j_{q}, j_{r}) + δ. Then, by hypothesis,

w(j_{0}, j_{p}) = w(π)
= w(π_{0q} :: π_{qr} :: π_{rp})
= w(π_{0q}) + w(π_{qr}) + w(π_{rp})
= w(π_{0q}) + w(j_{q}, j_{r}) + w(π_{rp}) + δ
= w(π_{0q} :: (j_{q}j_{r}) :: π_{rp}) + δ
≥ w(j_{0}, j_{p}) + δ

where the final step uses Lemma 5 again. Thus δ = 0. ⊓ ⊔

Lemma 7. Let G = (N , w) be a closed and zero-cycle free graph. Let also π = j_{0} ⋯ j_{p} be a proper path in G such that w(j_{0}, j_{p}) = w(π). Then π is a simple path.

Proof. The proof is by contraposition; hence we suppose that the path is not simple, i.e., for some q, r ∈ {0, …, p} such that q < r, we have j_{q} = j_{r}. Since the path is proper, j_{q} ≠ j_{q+1} so that j_{r} ≠ j_{q+1}. Thus, the path π′ = j_{q} ⋯ j_{r} is a proper cycle and, since the graph is zero-cycle free, w(π′) > 0. However, by Lemma 6, we also have w(j_{q}, j_{r}) = w(π′); therefore w(j_{q}, j_{r}) > 0, contradicting property (1) of Definition 1, i.e., the assumption that the graph is closed. Thus all the nodes in the path π are distinct, so that the path is simple. ⊓ ⊔

Lemma 8. Let G = (N , w) be a closed and zero-cycle free 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 7, 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 7, 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. ⊓ ⊔

A.3 An Improved Strong Closure Procedure for Octagonal Graphs

The following results, which are exploited in the proof of correctness of the strong reduction procedure, also show the correctness of the improved strong closure procedure described in Section 5.2.

Lemma 9. Let G = (N^{±}, w) be an octagonal 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. If z_{1} = z_{2} then, by property (1) of Definition 1, w^{c}(z_{1}, z_{2}) = 0, so that the results holds by taking π = z_{1}.

Suppose now that z_{1} ≠ z_{2}. The proof is by contraposition; we assume that w^{c}(z_{1}, z_{2}) ≠ w(z_{1} ⋯ z_{2}), for all simple paths z_{1} ⋯ z_{2} in G. Let G be the smallest octagonal graph for which this property holds and such that closure(G) = G^{c}. It follows that G^{c} ◁ G.

As closure(G) ◁ G, by Definition 1, for some i, j, k ∈ N^{±}, w(i, j) > w(i, k) + w(k, j). Let G_{k} = (N^{±}, w_{k}) where the weight function w_{k} is defined, for all h_{1}, h_{2} ∈ N^{±}, by

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

By Definition 1, G_{k} is octagonal, G^{c} ⊴ G_{k} ◁ G and closure(G_{k}) = G^{c}. Thus, by our minimality assumption on G, there exists a simple path π_{0} = z_{1} ⋯ z_{2} in G_{k} such that

w^{c}(z_{1}, z_{2}) = w_{k}(π_{0}).

Let π_{1} be the path in G_{k} obtained from π_{0} by replacing all subpaths (ij) by the path (ikj) and replacing all subpaths (\overline{ȷ}\overline{ı}) by the path (\overline{ȷ}\overline{k}\overline{ı}). Thus, by equation (6), w_{k}(π_{0}) = w_{k}(π_{1}) and w_{k}(π_{1}) = w(π_{1}) so that

w^{c}(z_{1}, z_{2}) = w(π_{1}).

Moreover, by Lemma 4, there exists a simple path π = z_{1} ⋯ z_{2} in G such that w(π_{1}) ≥ w(π) so that

w^{c}(z_{1}, z_{2}) ≥ w(π).

However, as G^{c} is closed, by Lemma 5, w^{c}(z_{1}, z_{2}) ≤ w^{c}(π) and, as G^{c} ◁ G, w^{c}(π) ≤ w(π), so that w^{c}(z_{1}, z_{2}) ≤ w(π). Therefore

w^{c}(z_{1}, z_{2}) = w(π),

contradicting the assumption for G. ⊓ ⊔

Lemma 10. Let G = (N^{±}, w) be a closed octagonal graph and i, j ∈ N^{±} be such that i ≠ \overline{ȷ} and 2w(i, j) ≥ w(i, \overline{ı})+w(\overline{ȷ}, j). Let G_{s}^{c} = (N^{±}, w_{s}^{c}) = closure(G_{s}) where G_{s} = (N^{±}, w_{s}) and, 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}  (7)

Let also z_{1}, z_{2} ∈ N^{±}. Then one or both of the following hold:

w_{s}^{c}(z_{1}, z_{2}) = w(z_{1}, z_{2});
2w_{s}^{c}(z_{1}, z_{2}) ≥ w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}).

Proof. By Definition 4, the graph G_{s} is octagonal. By construction, G_{s}^{c} ⊴G_{s} ⊴G. If (z_{1}, z_{2}) is not an arc in G_{s}^{c}, then w_{s}^{c}(z_{1}, z_{2}) = +∞; thus, as G_{s}^{c} ⊴ G, we also have w(i, j) = +∞ and hence w_{s}^{c}(z_{1}, z_{2}) = w(z_{1}, z_{2}). Suppose now that (z_{1}, z_{2}) is an arc in G_{s}^{c}. Then we can apply Lemma 9, so that there exists a simple path π = z_{1} ⋯ z_{2} in G_{s} such that w_{s}^{c}(z_{1}, z_{2}) = w_{s}(π).

Suppose first that w_{s}(π) = w(π). Then, as G is closed, by Lemma 5 we obtain w(π) ≥ w(z_{1}, z_{2}) so that w_{s}^{c}(z_{1}, z_{2}) ≥ w(z_{1}, z_{2}). However G_{s}^{c} ⊴ G so that w_{s}^{c}(z_{1}, z_{2}) ≤ w(z_{1}, z_{2}) and therefore w_{s}^{c}(z_{1}, z_{2}) = w(z_{1}, z_{2}).

Secondly suppose that w_{s}(π) ≠ w(π). Then, by equation (7), one or both of (i, j) and (\overline{ȷ}, \overline{ı}) must be in π. Thus, without loss of generality, we need to consider the following two cases:

π = π_{1} :: (ij) :: π_{2}  (8)
π = π_{1} :: (ij) :: π_{3} :: (\overline{ȷ}\overline{ı}) :: π_{4},  (9)

where π_{1} = z_{1} ⋯ i, π_{2} = j ⋯ z_{2}, π_{3} = j ⋯ \overline{ȷ}, π_{4} = \overline{ı} ⋯ z_{2} are simple paths in G_{s} that do not contain the arcs (i, j) and (\overline{ȷ}, \overline{ı}). Therefore, by equation (7), for each k = 1, …, 4 we have w_{s}(π_{k}) = w(π_{k}) and

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

Consider first equation (8). Let

π′_{1} = π_{1} :: (i\overline{ı}) :: \overline{π}_{1}, π′_{2} = \overline{π}_{2} :: (\overline{ȷ}j) :: π_{2}.

As G is an octagonal graph,

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

As G is closed, by Lemma 5, w(π′_{1}) ≥ w(z_{1}, \overline{z}_{1}) and w(π′_{2}) ≥ w(\overline{z}_{2}, z_{2}). Thus

2w_{s}(π) = 2w_{s}(π_{1}) + 2w_{s}(i, j) + 2w_{s}(π_{2})
= 2w(π_{1}) + w(i, \overline{ı}) + w(\overline{ȷ}, j) + 2w(π_{2})
= w(π′_{1}) + w(π′_{2})
≥ w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}).

Consider next equation (9). Let

π′_{1} = π_{1} :: (i\overline{ı}) :: \overline{π}_{1}, π′_{3} = (\overline{ȷ}j) :: π_{3} :: (\overline{ȷ}j) :: \overline{π}_{3}, π′_{4} = \overline{π}_{4} :: (i\overline{ı}) :: π_{4}.

As G satisfies the coherence assumption,

w(π′_{1}) = 2w(π_{1}) + w(i, \overline{ı}),
w(π′_{3}) = 2w(π_{3}) + 2w(\overline{ȷ}, j),
w(π′_{4}) = 2w(π_{4}) + w(i, \overline{ı}).

As G is consistent, 0 ≤ w(π′_{3}) and, as G is closed, by Lemma 5, w(π′_{1}) ≥ w(z_{1}, \overline{z}_{1}) and w(π′_{4}) ≥ w(\overline{z}_{2}, z_{2}). Thus, we have

2w_{s}(π) = 2w_{s}(π_{1}) + 2w_{s}(i, j) + 2w_{s}(π_{3}) + 2w_{s}(\overline{ȷ}, \overline{ı}) + 2w_{s}(π_{4})

= 2w(π_{1}) + w(i, \overline{ı}) + w(\overline{ȷ}, j) + 2w(π_{3}) + w(\overline{ȷ}, j) + w(i, \overline{ı}) + 2w(π_{4})

= w(π′_{1}) + w(π′_{3}) + w(π′_{4})
≥ w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}).

Thus, if either equation (8) or (9) holds, 2w_{s}(π) ≥ w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}). Therefore, as 2w_{s}^{c}(z_{1}, z_{2}) = 2w_{s}(π), we have 2w_{s}^{c}(z_{1}, z_{2}) ≥ w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}), as required. ⊓ ⊔

Lemma 11. Let G = (N^{±}, w) be a closed octagonal graph. Let G^{C} = (N^{±}, w^{C}) be such that G^{C} = Closure(G) and suppose that z_{1}, z_{2} ∈ N^{±}. Then one or both of the following hold:

w^{C}(z_{1}, z_{2}) = w(z_{1}, z_{2});  (10)
2w^{C}(z_{1}, z_{2}) = w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}).  (11)

Proof. The proof is by contraposition; thus we assume that neither (10) nor (11) hold. Let G be the smallest octagonal graph for which these equalities do not hold and such that Closure(G) = G^{C}. It follows that G^{C} ≠ G.

As G^{C} = Closure(G), G^{C} ◁ G; hence, as G is closed, by Definitions 1 and 5, there exist i, j ∈ N^{±} such that i ≠ \overline{ȷ} and 2w(i, j) > w(i, \overline{ı}) + w(\overline{ȷ}, j). Let G_{1} = (N^{±}, w_{1}) where, for all h_{1}, h_{2} ∈ N^{±},

w_{1}(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}  (12)

Let also

G_{1}^{c} := (N^{±}, w_{1}^{c}) = closure(G_{1}).

Then G_{1}^{c} ◁ G. By Definition 5, G_{1} is octagonal, G^{C} ⊴ G_{1}^{c} and Closure(G_{1}^{c}) = G^{C} so that, by the minimality assumption, one or both of the following hold:

w^{C}(z_{1}, z_{2}) = w_{1}^{c}(z_{1}, z_{2});  (13)
2w^{C}(z_{1}, z_{2}) = w_{1}^{c}(z_{1}, \overline{z}_{1}) + w_{1}^{c}(\overline{z}_{2}, z_{2}).  (14)

Consider (13). By Lemma 10, at least one of w_{1}^{c}(z_{1}, z_{2}) = w(z_{1}, z_{2}) and 2w_{1}^{c}(z_{1}, z_{2}) ≥ w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}) hold. If the first holds, then w^{C}(z_{1}, z_{2}) = w(z_{1}, z_{2}), contradicting the assumption for G. Alternatively, if the second holds, then 2w^{C}(z_{1}, z_{2}) ≥ w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}). However, by Definition 5, we have 2w^{C}(z_{1}, z_{2}) ≤ w^{C}(z_{1}, \overline{z}_{1})+w^{C}(\overline{z}_{2}, z_{2}); and, as G^{C} ⊴G, w^{C}(z_{1}, \overline{z}_{1})+w^{C}(\overline{z}_{2}, z_{2}) ≤ w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}); so that 2w^{C}(z_{1}, z_{2}) ≤ w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}). Therefore 2w^{C}(z_{1}, z_{2}) = w(z_{1}, \overline{z}_{1}) + w(\overline{z}_{2}, z_{2}), contradicting the assumption for G.

Finally consider (14). By Lemma 10, w_{1}^{c}(z_{1}, \overline{z}_{1}) = w(z_{1}, \overline{z}_{1}) and w_{1}^{c}(\overline{z}_{2}, z_{2}) = w(\overline{z}_{2}, z_{2}). Thus 2w^{C}(z_{1}, z_{2}) = w(z_{1}, \overline{z}_{1})+w(\overline{z}_{2}, z_{2}), contradicting the assumption for G. ⊓ ⊔

Proof (of Theorem 2). Let G^{C} = (N^{±}, w^{C}) be such that G^{C} = Closure(G^{c}). We will show that, for each i, j ∈ N^{±}, w^{S}(i, j) = w^{C}(i, j).

By Definition 5, w^{C}(i, j) ≤ w^{S}(i, j) and 2w^{C}(i, j) ≤ w^{S}(i, \overline{ı})+w^{S}(\overline{ȷ}, j). Moreover, by Lemma 11, either w^{C}(i, j) = w^{c}(i, j) or 2w^{C}(i, j) = w^{c}(i, \overline{ı}) + w^{c}(\overline{ȷ}, j).

Suppose that w^{C}(i, j) = w^{c}(i, j). Then, as by hypothesis w^{S}(i, j) ≤ w^{c}(i, j), we obtain w^{S}(i, j) = w^{C}(i, j). Suppose now that 2w^{C}(i, j) = w^{c}(i, \overline{ı}) + w^{c}(\overline{ȷ}, j). Then, since by hypothesis 2w^{S}(i, j) ≤ w^{c}(i, \overline{ı}) + w^{c}(\overline{ȷ}, j), we again obtain that w^{S}(i, j) = w^{C}(i, j). ⊓ ⊔

A.4 Proofs of the Results Stated in Section 5.1

Lemma 12. Let G = (N^{±}, w) be a strongly closed octagonal graph and i, j ∈ N^{±}. Then, i ≡_{G} j if and only if \overline{ı} ≡_{G} \overline{ȷ}.

Proof. By Definition 7, i ≡_{G} j if and only if w(i, j) = −w(j, i), which is equivalent to w(j, i) = −w(i, j). Since, by hypothesis, G is an octagonal graph, we can rewrite the latter formula using the coherence assumption (3) of Definition 4, to obtain w(\overline{ı}, \overline{ȷ}) = −w(\overline{ȷ}, \overline{ı}) which, again by Definition 7, is equivalent to \overline{ı} ≡_{G} \overline{ȷ}. ⊓ ⊔

Proof (of Lemma 1 on page 10). In order to prove that \overline{E} is a zero-equivalence class for G, we have to show that:

1. \overline{E} is not the empty set; and

2. for all i ∈ \overline{E} and j ∈ N^{±}, we have j ∈ \overline{E} if and only if i ≡_{G} j.

The first property follows from the observation that, as E is a zero-equivalence class, it is not empty and thus, by construction, \overline{E} is not empty.

To prove the second property, let i ∈ \overline{E} and j ∈ N^{±} so that, by construction, we have \overline{ı} ∈ E. Suppose that j ∈ \overline{E}; then, by construction, \overline{ȷ} ∈ E so that \{\overline{ı}, \overline{ȷ}\} ⊆ E. Since E is a zero-equivalence class, \overline{ı} ≡_{G} \overline{ȷ}. By Lemma 12, we obtain i ≡_{G} j. Suppose now that i ≡_{G} j. Then, by Lemma 12, \overline{ı} ≡_{G} \overline{ȷ} and hence, since \overline{ı} ∈ E and E is a zero-equivalence class, we obtain \overline{ȷ} ∈ E. Therefore we have j ∈ \overline{E}. ⊓ ⊔

Lemma 13. Let G = (N^{±}, w) be a strongly closed octagonal graph and E ⊆ N^{±} be a zero-equivalence 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, 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 and E ⊆ N^{±} be a zero-equivalence class for G. Let also i, j ∈ N^{±} and π = i ⋯ j be a path in G such that every node in π is also in E. Then w(π) = w(i, j).

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

w(π) = w(i, k) + w(π′)
= w(i, k) + w(k, j)
= w(i, j),

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

Lemma 15. Let G = (N^{±}, w) be a strongly closed octagonal graph with a singular zero-equivalence 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 (5) of Definition 5, 2w(i, j) ≤ w(i, \overline{ı}) + w(\overline{ȷ}, j). Therefore, it remains to prove 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 (3) 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 10). 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 15,

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 11). 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, if (i, j) is an arc in L (resp., in E), then (i, j) is an arc in G and we have w_{L}(i, j) = w(i, j) (resp., w_{E}(i, j) = w(i, j)); hence, if π is a path in L (resp., in E), then π is also a path in G and w_{L}(π) = w(π) (resp., w_{E}(π) = w(π)).

We first prove that graphs L and E are octagonal, i.e., by Definition 4, that they are consistent graphs satisfying the coherence assumption (3).

To show that the coherence assumption 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 is octagonal w(i, j) = w(\overline{ȷ}, \overline{ı}) so that w_{L}(i, j) = w_{L}(\overline{ȷ}, \overline{ı}). Hence, L is a graph that satisfied the coherence assumption (3).

To show that the coherence assumption 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 12, 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 is octagonal, w(i, j) = w(\overline{ȷ}, \overline{ı}) so that w_{E}(i, j) = w_{E}(\overline{ȷ}, \overline{ı}). Hence, E is a graph that satisfied the coherence assumption (3).

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

Secondly, we prove that L and E are strongly closed. Namely, we show that the weight functions w_{L} and w_{E} satisfy properties (1) and (2) of Definition 1 and property (5) of Definition 5.

Consider property (1) of Definition 1 and let i ∈ N^{±}. As G is consistent, 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) of Definition 1 and let i, j, k ∈ N^{±}. By the previous paragraph, the property trivially holds when i = j or i = k or j = k. Thus we assume that i, j and k are distinct nodes. Consider first the graph L. If i ∉ L then, by Definition 8, w_{L}(i, k) = +∞, so that the property holds. Similarly if j ∉ L the property holds. Suppose now that i, j ∈ L so that, by Definition 8, w_{L}(i, j) = w(i, j). If k ∉ L, then w_{L}(i, k) = w_{L}(k, j) = +∞, so that the property holds. Alternatively, if k ∈ L, w_{L}(i, k) = w(i, k) and w_{L}(k, j) = w(k, j). As G is a closed graph, w(i, j) ≤ w(i, k)+w(k, j) and hence w_{L}(i, j) ≤ w_{L}(i, k)+w_{L}(k, j). Consider now the graph E. If i ≢_{G} j then, by Definition 8, w_{E}(i, k) = +∞ or w_{E}(k, j) = +∞, so that the property holds. Suppose now that i ≡_{G} j so that, by Definition 8, w_{E}(i, j) = w(i, j). If i ≢_{G} k, then w_{E}(i, k) = +∞, so that the property holds. Alternatively, if i ≡_{G} k, then k ≡_{G} j so that w_{E}(i, k) = w(i, k) and w_{E}(k, j) = w(k, j). As G is a closed graph, w(i, j) ≤ w(i, k) + w(k, j) and hence w_{E}(i, j) ≤ w_{E}(i, k) + w_{E}(k, j).

Consider property (5) of Definition 5 and let i, j ∈ N^{±}. By what we have shown above, the property trivially holds when i = j. Thus we assume i ≠ j. Consider first the graph L. If i ∉ L or j ∉ L, then, by Definition 8, w_{L}(i, \overline{ı}) = +∞ or w_{L}(\overline{ȷ}, j) = +∞ so that the property holds. Suppose next that 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). Since G is strongly closed, 2w(i, j) ≤ w(i, \overline{ı}) + w(\overline{ȷ}, j) and hence 2w_{L}(i, j) ≤ w_{L}(i, \overline{ı}) + w_{L}(\overline{ȷ}, j). Consider now the graph E. Suppose first that i or j does not belong to the singular zero-equivalence class. Then, by Lemma 1, we have i ≢_{G} \overline{ı} or j ≢_{G} \overline{ȷ}. By Definition 8, w_{E}(i, \overline{ı}) = +∞ or w_{E}(\overline{ȷ}, j) = +∞, so that the property holds. Suppose next that both i and j belong to the singular zero-equivalence class. Then, i ≡_{G} \overline{ı} ≡_{G} j ≡_{G} \overline{ȷ} so that, 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). Since G is strongly closed, 2w(i, j) ≤ w(i, \overline{ı}) + w(\overline{ȷ}, j) and hence 2w_{E}(i, j) ≤ w_{E}(i, \overline{ı}) + w_{E}(\overline{ȷ}, j).

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}, j_{0} ≠ j_{1} and p ≥ 2. As shown in the first paragraph, π is also a proper cycle in G and w_{L}(π) = w(π). As G is a closed graph, by Lemma 5, w(j_{1} ⋯ j_{p}) ≥ w(j_{1}, j_{p}) = w(j_{1}, j_{0}) so that w(π) ≥ w(j_{0}, j_{1})+w(j_{1}, j_{0}). As w(j_{0}, j_{1}) < +∞ and 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(j_{0}, j_{1}) + w(j_{1}, j_{0}) > 0. As a consequence, w_{L}(π) = w(π) > 0. ⊓ ⊔

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}),
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 octagonal graph G is 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 8, 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 7, 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 8, 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 Closure(A) = G.

Proof. Let G = (N^{±}, w) and Closure(A) = (N^{±}, w^{C}). Since G⊴A and the strong closure operator is both monotonic and idempotent, we obtain G ⊴ Closure(A). Therefore, to prove the result, it remains for us to show that Closure(A) ⊴ G.

Letting (i, j) be any arc of G, we will show that w^{C}(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^{C}(π) ≤ w(π). Moreover, by Lemma 5, w^{C}(i, j) ≤ w^{C}(π) and hence w^{C}(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 (5) 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^{C}(π_{i}) ≤ w(π_{i}) and w^{C}(π_{j}) ≤ w(π_{j}). By Lemma 5, w^{C}(i, \overline{ı}) ≤ w^{C}(π_{i}) and w^{C}(\overline{ȷ}, j) ≤ w^{C}(π_{j}); hence w^{C}(i, \overline{ı}) ≤ w(i, \overline{ı}) and w^{C}(\overline{ȷ}, j) ≤ w(\overline{ȷ}, j). Thus, w^{C}(i, \overline{ı})+w^{C}(\overline{ȷ}, j) ≤ 2w(i, j) and, by property (5) of Definition 5, w^{C}(i, j) ≤ w(i, j).

We can therefore conclude that Closure(A) ⊴ G. ⊓ ⊔

Lemma 20. Let G = (N^{±}, w) be an octagonal graph and G^{C} = (N^{±}, w^{C}) be such that G^{C} = Closure(G); let also (i, j) be an arc in G^{C}. Then one of the following properties holds:

1. there exists a simple path π = i ⋯ j in G where w^{C}(i, j) = w(π);

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

Proof. Let G^{c} = (N^{±}, w^{c}) = closure(G). Then we also have G^{C} = Closure(G^{c}).

Suppose that property 1 does not hold. Then, by Lemma 9, w^{C}(i, j) ≠ w^{c}(i, j). Thus, by Lemma 11,

2w^{C}(i, j) = w^{c}(i, \overline{ı}) + w^{c}(\overline{ȷ}, j)

and hence, i ≠ \overline{ȷ}. By Definition 5,

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

and, as Closure(G^{c}) = G^{C}, w^{c}(i, \overline{ı}) ≥ w^{C}(i, \overline{ı}) and w^{c}(\overline{ȷ}, j) ≥ w^{C}(\overline{ȷ}, j). Therefore

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

By Lemma 9, there exist simple paths π_{i} = i ⋯ \overline{ı} in G and π_{j} = \overline{ȷ} ⋯ j in G, where

w^{c}(i, \overline{ı}) = w(π_{i}), w^{c}(\overline{ȷ}, j) = w(π_{j})

so that

w^{C}(i, \overline{ı}) = w(π_{i}), w^{C}(\overline{ȷ}, j) = w(π_{j}).
⊓ ⊔

Lemma 21. Let G be a strongly closed octagonal graph and Z the zero-equiva-lence 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 (3) of Definition 4. Therefore, Z is octagonal and hence, an octagonal subgraph of G. ⊓ ⊔

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 unique simple 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 G, if E contains more than one node, then there is a unique simple 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 non-singular. If E is positive and z_{0} < ⋯ < z_{m}, then, by Definition 10, there is a unique simple cycle π_{E} = z_{0} ⋯ z_{m}z_{0} in (N^{±}, w′). Hence, π_{E} is also a simple cycle in Z. Moreover, since E ∩ \overline{E} = ∅, the arcs in π_{E} are the only arcs in Z connecting nodes in E, so that the simple cycle is still unique. 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 unique simple cycle π\overline{E} = \overline{z}_{0} ⋯ \overline{z}_{m}\overline{z}_{0} in Z connecting the nodes of \overline{E}. As E ∩ \overline{E} = ∅ and Z is octagonal, there is also a unique simple 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 unique simple path π^{+} = z_{0} ⋯ z_{m} in (N^{±}, w′) connecting all and only the positive nodes in E; also, (N^{±}, w′) contains the arcs (\overline{z}_{0}, z_{0}) and (z_{m}, \overline{z}_{m}). Since E = \overline{E} and Z is octagonal, both π^{+} and π^{−} = \overline{π}^{+} = \overline{z}_{m} ⋯ \overline{z}_{0} are unique simple paths in Z connecting all and only the positive and negative nodes of E, respectively. Therefore, π_{E} = π^{+} :: (z_{m}\overline{z}_{m}) :: π^{−} :: (\overline{z}_{0}z_{0}) is a unique simple 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 unique simple cycle π_{E} as defined above; thus, there exists a unique simple path π = i ⋯ j in Z. As Z is a subgraph of E, w_{Z}(π) = w_{E}(π). By Lemma 14, 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 Closure(Z) = E.

Proof. Let Closure(Z) = (N^{±}, w_{Z}^{C}). Consider any i, j ∈ N^{±}. Then we must show that w_{Z}^{C}(i, j) = w_{E}(i, j). By Lemma 3, E is strongly closed. By Lemma 21 Z is a subgraph of E. Hence, E ⊴ Z and E ⊴ Closure(Z).

Suppose first that i ≢_{E} j. Then, by Definition 8, w_{E}(i, j) = +∞. Since E ⊴ Closure(Z), we have w_{Z}^{C}(i, j) = +∞.

We now assume that i ≡_{E} j. If i = j then, by property (1) of Definition 1, w_{E}(i, j) = w_{Z}^{C} = 0. Suppose now that i ≠ j. By Lemma 22, there exists a unique simple path π = i ⋯ j in Z and w_{Z}(π) = w_{E}(i, j). As w_{Z}^{C}(π) ≤ w_{Z}(π) and w_{Z}^{C}(i, j) ≤ w_{Z}^{C}(π), we have w_{Z}^{C}(i, j) < +∞ so that (i, j) is an arc in Closure(Z). By Lemma 20, one of the following properties holds:

1. there exists a simple path π′ = i ⋯ j in Z such that w_{Z}^{C}(i, j) = w_{Z}(π′);

2. 2w_{Z}^{C}(i, j) = w_{Z}^{C}(i, \overline{ı}) + w_{Z}^{C}(\overline{ȷ}, j) and there exist simple paths π_{i} = i ⋯ \overline{ı}, π_{j} = \overline{ȷ} ⋯ j in Z such that w_{Z}^{C}(i, \overline{ı}) = w_{Z}(π_{i}) and w_{Z}^{C}(\overline{ȷ}, j) = w_{Z}(π_{j}).

Consider property 1. By Lemma 22, π′ = π and w_{Z}(π) = w_{E}(i, j) and therefore, w_{Z}^{C}(i, j) = w_{E}(i, j). Consider next property 2. By Lemma 22, w_{Z}(π_{i}) = w_{E}(i, \overline{ı}) and w_{Z}(π_{j}) = w_{E}(\overline{ȷ}, j). Therefore (i, \overline{ı}) and (\overline{ȷ}, j) are arcs in E and hence, by Definition 8, i ≡_{E} \overline{ı} and \overline{ȷ} ≡_{E} j so that E is singular. Thus we can apply Lemma 15, to obtain w_{E}(i, \overline{ı}) + w_{E}(\overline{ȷ}, j) = 2w_{E}(i, j). Therefore w_{Z}^{C}(i, j) = w_{E}(i, j). ⊓ ⊔

Lemma 24. Let G = (N^{±}, w) be an octagonal graph. Suppose that, for all arcs (i, j) in G, the following properties hold:

1. for all simple paths π = i ⋯ j in G such that π ≠ ij, w(i, j) < w(π); 2. if i ≠ \overline{ȷ}, then, for all simple paths π_{i} = i ⋯ \overline{ı} and π_{j} = \overline{ȷ} ⋯ j in G, 2w(i, j) <

w(π_{i}) + w(π_{j}).

Let also G_{1} be a proper subgraph of G. Then Closure(G) ≠ Closure(G_{1}).

Proof. Let G_{1} = (N^{±}, w_{1}). Let also G^{C} = (N^{±}, w^{C}) and G_{1}^{C} = (N^{±}, w_{1}^{C}) be such that G^{C} = Closure(G) and G_{1}^{C} = Closure(G_{1}). As G_{1} is a proper subgraph of G, there exists an arc (i, j) in G that is not an arc in G_{1}. Then, as G and G_{1} are octagonal, (\overline{ȷ}, \overline{ı}) is also an arc in G but not in G_{1}. To prove the result, we show that w^{C}(i, j) < w_{1}^{C}(i, j).

If w_{1}^{C}(i, j) = +∞, then the result follows. Suppose now that w_{1}^{C}(i, j) < +∞. By Lemma 20, either w_{1}^{C}(i, j) = w_{1}(π), for some simple path π = i ⋯ j in G_{1}, or 2w_{1}^{C}(i, j) = w_{1}(π_{i})+w_{1}(π_{j}), for some simple paths π_{i} = i ⋯ \overline{ı} and π_{j} = \overline{ȷ} ⋯ j in G_{1}. If the first equality holds, as G_{1} is a subgraph of G, w(π) = w_{1}(π); also, by hypothesis, we have w(i, j) < w(π). Thus, we have

w^{C}(i, j) ≤ w(i, j) < w(π) = w_{1}(π) = w_{1}^{C}(i, j).

Similarly, if the second equality holds, as G_{1} is a subgraph of G, w(π_{i}) = w_{1}(π_{i}) and w(π_{j}) = w_{1}(π_{j}); also, by hypothesis, we have 2w(i, j) < w(π_{i}) + w(π_{j}). Thus,

2w^{C}(i, j) ≤ 2w(i, j) < w(π_{i}) + w(π_{j}) = w_{1}(π_{i}) + w_{1}(π_{j}) = 2w_{1}^{C}(i, j).
⊓ ⊔

Lemma 25. Let G = (N^{±}, w) be a strongly reduced octagonal graph. Then G is a subgraph of Closure(G).

Proof. Let G^{C} = (N^{±}, w^{C}) = Closure(G). Suppose that (i, j) is an arc in G. We first show that both of the following properties hold:

1. for all paths π = i ⋯ j in G, w(i, j) ≤ w(π);

2. for all paths π_{i} = i ⋯ \overline{ı} and π_{j} = \overline{ȷ} ⋯ j in G, 2w(i, j) ≤ w(π_{i}) + w(π_{j}).

We prove this by contraposition. Thus we suppose either 1 or 2 does not hold. Let G_{1} = (N^{±}, w_{1}) where the weight function w_{1} is defined, for all h_{1}, h_{2} ∈ N^{±}, by

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

Then G ◁ G_{1} and, as G is octagonal, by Definition 4, G_{1} is octagonal. Let G_{1}^{C} = (N^{±}, w_{1}^{C}) = Closure(G_{1}), so that G^{C} ⊴ G_{1}^{C}. We will show that G_{1}^{C} ⊴ G so that G_{1}^{C} = G^{C}; which, by Definition 6, contradicts the assumption that G is strongly reduced.

To prove that G_{1}^{C} ⊴ G, letting (h_{1}, h_{2}) be any arc in G, we must show that w_{1}^{C}(h_{1}, h_{2}) ≤ w(h_{1}, h_{2}). Since strong closure is reductive, w_{1}^{C}(h_{1}, h_{2}) ≤ w_{1}(h_{1}, h_{2}). Thus, by (15), if (h_{1}, h_{2}) ∉ \{(i, j), (\overline{ȷ}, \overline{ı})\}, then w_{1}(h_{1}, h_{2}) = w(h_{1}, h_{2}) and hence, w_{1}^{C}(h_{1}, h_{2}) ≤ w(h_{1}, h_{2}). It therefore remains to consider the case when (h_{1}, h_{2}) ∈ \{(i, j), (\overline{ȷ}, \overline{ı})\}. We just prove that w_{1}^{C}(i, j) ≤ w(i, j), since the other inequality w_{1}^{C}(\overline{ȷ}, \overline{ı}) ≤ w(\overline{ȷ}, \overline{ı}) will follow by using the coherence assumption (3) in Definition 4, as G and G_{1} are both octagonal graphs.

Suppose 1 does not hold. Then, for some path π = i ⋯ j in G, w(i, j) > w(π). Observe that the path π does not contain the arcs (i, j) and (\overline{ȷ}, \overline{ı}). This is because, if π = π_{ii} :: (ij) :: π_{jj}, then, as G is consistent, we obtain w(i, j) > w(i, j) and, similarly, if π = π_{i\overline{ȷ}} :: (\overline{ȷ}\overline{ı}) :: π_{\overline{ı}j}, then, as G satisfies the coherence assumption, w(π) = w(π_{i\overline{ȷ}} :: \overline{π}_{\overline{ı}j}) + w(i, j) so that again, as G is consistent, w(i, j) > w(i, j). Therefore, by (15), w_{1}(π) = w(π). Moreover, by Lemma 5, w_{1}^{C}(i, j) ≤ w_{1}^{C}(π) and, as strong closure is reductive, w_{1}^{C}(π) ≤ w_{1}(π). Therefore,

w_{1}^{C}(i, j) ≤ w_{1}^{C}(π) ≤ w_{1}(π) = w(π) < w(i, j).

Suppose 1 holds but 2 does not hold. Then i ≠ \overline{ȷ} and for some paths π_{i} = i ⋯ \overline{ı} and π = \overline{ȷ} ⋯ j, 2w(i, j) > w(π_{i}) + w(π_{j}). Observe that w(π_{i}) does not contain the arc (i, j); suppose to the contrary that π_{i} = π_{ii} :: (ij) :: π_{j\overline{ı}}. Then, as G is octagonal, 2w(i, j) > w(π_{i}) + w(π_{j}) = w(π_{ii}) + w(i, j) + w(\overline{π}_{j\overline{ı}} :: π_{j}) so that w(i, j) > w(\overline{π}_{j\overline{ı}} :: π_{j}) and 1 does not hold, contradicting our assumption for this case. For similar reasons, π_{i} also cannot contain the arc (\overline{ȷ}, \overline{ı}). Therefore, by (15), we have w(π_{i}) = w_{1}(π_{i}). Similarly w(π_{j}) = w_{1}(π_{j}). Moreover, by Lemma 5, w_{1}^{C}(i, \overline{ı}) ≤ w_{1}^{C}(π_{i}); as strong closure is reductive, w_{1}^{C}(π_{i}) ≤ w_{1}(π_{i}) so that w_{1}^{C}(i, \overline{ı}) ≤ w_{1}(π_{i}). Similarly, w_{1}^{C}(\overline{ȷ}, j) ≤ w_{1}(π_{j}). However, by Definition 5, 2w_{1}^{C}(i, j) ≤ w_{1}^{C}(i, \overline{ı}) + w_{1}^{C}(\overline{ȷ}, j). Therefore

2w_{1}^{C}(i, j) ≤ w_{1}^{C}(i, \overline{ı}) + w_{1}^{C}(\overline{ȷ}, j) ≤ w_{1}(π_{i}) + w_{1}(π_{j}) = w(π_{i}) + w(π_{j}) < 2w(i, j).

We have shown that (i, j) satisfies properties 1 and 2. We next prove that w^{C}(i, j) = w(i, j). As strong closure is reductive, w^{C}(i, j) ≤ w(i, j). We now prove w^{C}(i, j) ≥ w(i, j). By Lemma 20, either there exists a simple path π = i ⋯ j in G such that w^{C}(i, j) = w(π); or there exist simple paths π_{i} = i ⋯ \overline{ı} and π_{j} = \overline{ȷ} ⋯ j such that 2w^{C}(i, j) = w(π_{i}) + w(π_{j}). Since (i, j) satisfies 1 and 2, in both cases, w^{C}(i, j) ≥ w(i, j) and hence, w^{C}(i, j) = w(i, j). Similarly we have w^{C}(\overline{ȷ}, \overline{ı}) = w(\overline{ȷ}, \overline{ı}). Therefore G is a subgraph of G^{C}. ⊓ ⊔

Proof (of Theorem 1 on page 13). 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}^{C} = (N^{±}, w_{R}^{C}) = Closure(G_{R}). Then we need to show that G_{R} is a strongly reduced octagonal graph and G_{R}^{C} = G.

First we show that G_{R} is an octagonal subgraph of G. By Definition 8, both L and E are subgraphs of G; moreover, by Definitions 9 and 10, A is a subgraph of L and Z is a subgraph of E, so that A and Z are also subgraphs of G. Thus, as G_{R} = A ⊓ Z, G_{R} is a subgraph of G; hence, as G is consistent, G_{R} is also a consistent graph. Moreover, since both A and Z are octagonal graphs and, therefore, satisfy the coherence assumption, G_{R} = A ⊓ Z satisfies the coherence assumption. Thus, G_{R} is an octagonal subgraph of G.

Next we show that G_{R}^{C} = G. By Lemma 3, L is a strongly closed an zero-cycle free octagonal graph so that, by Lemma 19, Closure(A) = L; also, by Lemma 23, Closure(Z) = E. Thus, we have

G_{R}^{C} = Closure(Closure(A ⊓ Z))

= Closure(Closure(A) ⊓ Closure(Z))

= Closure(L ⊓ E).

As observed before, L and E are subgraphs of G and hence G ⊴ G_{R}^{C}. It remains to show that G_{R}^{C} ⊴ 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}^{C} ⊴ G, we just need to show that

w_{R}^{C}(i, j) ≤ w(i, j).  (16)

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}^{C}(i, j) ≤ w_{E}(i, j), equation (16) 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}  (17)

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 15 and (17),

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}^{C}(i, j) ≤ w_{R}^{C}(i, \overline{ı}) + w_{R}^{C}(\overline{ȷ}, \overline{ℓ}_{j}) + w_{R}^{C}(\overline{ℓ}_{j}, ℓ_{j}) + w_{R}^{C}(ℓ_{j}, j)
≤ w_{E}(i, \overline{ı}) + w_{E}(\overline{ȷ}, \overline{ℓ}_{j}) + w_{L}(\overline{ℓ}_{j}, ℓ_{j}) + w_{E}(ℓ_{j}, j)

since G_{R}^{C} ⊴ L and G_{R}^{C} ⊴ E. Therefore equation (16) 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}^{C}(i, j) ≤ w_{R}^{C}(i, ℓ_{i}) + w_{R}^{C}(ℓ_{i}, ℓ_{j}) + w_{R}^{C}(ℓ_{j}, j)
≤ w_{E}(i, ℓ_{i}) + w_{L}(ℓ_{i}, ℓ_{j}) + w_{E}(ℓ_{j}, j)

since G_{R}^{C} ⊴ L and G_{R}^{C} ⊴ E. Therefore equation (16) holds and hence G_{R}^{C} = G.

Finally we show that G_{R} is strongly reduced. Suppose there exists a strongly reduced octagonal graph G_{1} such that G_{R} ◁ G_{1} and G = Closure(G_{1}). Then, by Lemma 25, G_{1} is a subgraph of G. Since G_{R} is also a subgraph of G and G_{R} ◁ G_{1}, then G_{1} is a proper subgraph of G_{R}.

Since A and Z are subgraphs of G_{R} and G_{R} = A ⊓ Z, for each i, j ∈ N^{±}, we have that (i, j) is an arc in G_{R} if and only if it is an arc in A or in Z. Thus, by Definitions 9 and 10, for all i, j ∈ N^{±}, there is at most one simple path π = i ⋯ j in G_{R}. Thus, if (i, j) is an arc and π = i ⋯ j a simple path in G_{R}, we must have π = ij. Therefore condition (1) of Lemma 24 holds.

By Definitions 9 and 10, if (i, j) is an arc in A, 2w_{A}(i, j) < w(i, \overline{ı}) + w(\overline{ȷ}, j) and if (i, j) is an arc in Z, 2w_{Z}(i, j) < w(i, \overline{ı}) + w(\overline{ȷ}, j). Thus, if (i, j) is an arc in G_{R}, 2w_{R}(i, j) < w(i, \overline{ı}) + w(\overline{ȷ}, j). As G is closed, Lemma 5 applies so that, for all paths π_{i} = i ⋯ \overline{ı} and π_{j} = \overline{ȷ} ⋯ j in G_{R}, w(i, \overline{ı}) ≤ w(π_{i}) and w(\overline{ȷ}, j) ≤ w(π_{j}). As G_{R} is a subgraph of G, we have, w(π_{i}) ≤ w_{R}(π_{i}) and w(π_{j}) ≤ w_{R}(π_{j}). Hence 2w_{R}(i, j) < w(π_{i}) + w(π_{j}) ≤ w_{R}(π_{i}) + w_{R}(π_{j}). Therefore condition (2) of Lemma 24 also holds. Thus Lemma 24 can be applied to obtain G_{1}^{C} ≠ G_{R}^{C}, which is a contradiction. ⊓ ⊔

A.5 Proofs of the Results Stated in Section 5.3

The standard widening operator ‘∇_{s}’ for topologically closed convex polyhedra defined in the PhD thesis of N. Halbwachs [22, Définition 5.3.3, p. 57] is slightly different from the specification originally proposed in [19], 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 [6, 7], 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 of [7, Proposition 6]. ⊓ ⊔

Proof (of Theorem 3). 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}’. ⊓ ⊔