A.1 A proof for the cyclic edge detection algorithm

As cyclic edge detector algorithm progresses each vertex $v$ is coloured WHITE if it is yet to be explored (i.e. no call $\mathit{\ensuremath{\operatorname{visit}}} (v)$ has yet been made), GREY if $\mathit{\ensuremath{\operatorname{visit}}} (v)$ has been called but not yet returned and BLACK if $\mathit{\ensuremath{\operatorname{visit}}} (v)$ has returned. At time $t$ we consider each vertex to belong to one of the sets $\mathit{\ensuremath{\operatorname{WV}}}_t$ , $\mathit{\ensuremath{\operatorname{GV}}}_t$ or $\mathit{\ensuremath{\operatorname{BV}}}_t$ associated with the three colours. We define similar sets $\mathit{\ensuremath{\operatorname{WE}}}_t$ , $\mathit{\ensuremath{\operatorname{GE}}}_t$ and $\mathit{\ensuremath{\operatorname{BE}}}_t$ for edges that, respectively: have yet to be explored, have been traversed via a call to visit that has not yet returned or that have been traversed via a call to visit that has returned. Using the process of edge classification in [22] we extend the definition of the four distinct types of edges depending on when they are encountered in the DFS process:

Tree

- Any edge $(u, v)$ where $v \in \mathit{\ensuremath{\operatorname{WV}}}_t$ when $v$ is discovered from a call $\mathit{\ensuremath{\operatorname{visit}}} (u)$ at time $t$ .

Forward

- An edge $(u, v)$ where $v \in \mathit{\ensuremath{\operatorname{GV}}}_t$ when $v$ is encountered from $\mathit{\ensuremath{\operatorname{visit}}} (u)$ at time $t$ and $\mathit{\ensuremath{\operatorname{timestamp}}} (v) < \mathit{\ensuremath{\operatorname{timestamp}}} (u)$ .

Back

- An edge $(u, v)$ where $v \in \mathit{\ensuremath{\operatorname{GV}}}_t$ when $v$ is encountered from $\mathit{\ensuremath{\operatorname{visit}}} (u)$ at time $t$ and $\mathit{\ensuremath{\operatorname{timestamp}}} (v) > \mathit{\ensuremath{\operatorname{timestamp}}} (u)$ .

Cross

- An edge $(u, v)$ where $v \in \mathit{\ensuremath{\operatorname{BV}}}_t$ when $v$ is encountered from $\mathit{\ensuremath{\operatorname{visit}}} (u)$ at time $t$ .

From these definitions it is clear that cross edges are never involved in a cycle, so we need not consider them in the proof of correctness. Also, it is clear that each cycle must involve a back edge. Further, for each back edge $(u, v)$ encountered by algorithm cyclic edge detector, $v$ is marked as a cyclic ancestor (i.e. $v_{\mathit{\ensuremath{\operatorname{ca}}}} = v)$ and as the cyclic ancestor of $u$ , $u_{\mathit{\ensuremath{\operatorname{ca}}}} = v$ .

Lemma: At time $t$ for each vertex $a \in \mathit{\ensuremath{\operatorname{BV}}}_t \cup \mathit{\ensuremath{\operatorname{GV}}}_t$ , if $a$ is involved in a cycle, then the cyclic ancestor $c$ of $a$ is the earliest grey vertex ( $\min (\mathit{\ensuremath{\operatorname{timestamp}}} (v)) \forall v \in \mathit{\ensuremath{\operatorname{GV}}}_t$ ) where there exists a directed path from $a$ to $c$ using only BLACK edges.

Proof. Proof is by induction. The initial case occurs when adding a back edge $e = (u, v)$ to $\mathit{\ensuremath{\operatorname{BE}}}$ . We know by definition that $u_{\mathit{\ensuremath{\operatorname{ca}}}} = v$ and there is a path from $u$ to $v$ via the newly BLACK edge $e$ . We now show that for any other edge $f$ that is part of a cycle involving e, as $f$ is added to $\mathit{\ensuremath{\operatorname{BE}}}$ , Lemma 1 remains true.

We know that cross edges cannot be involved in a cycle and back edges are the base case, so we have only the cases of adding tree and forward edges to $\mathit{\ensuremath{\operatorname{BE}}}$ remaining. As a tree or forward edge $e = (u, v)$ is added to $\mathit{\ensuremath{\operatorname{BE}}}$ , if there exists a cyclic ancestor for $v$ , i.e. $v_{\mathit{\ensuremath{\operatorname{ca}}}}$ , then we know there is a directed path from $v$ to $v_{\mathit{\ensuremath{\operatorname{ca}}}}$ . By extension, there is also a path from $u$ to $v_{\mathit{\ensuremath{\operatorname{ca}}}}$ (if $\mathit{\ensuremath{\operatorname{timestamp}}} (v_{\mathit{\ensuremath{\operatorname{ca}}}}) < \mathit{\ensuremath{\operatorname{timestamp}}} (u)$ we set $u_{\mathit{\ensuremath{\operatorname{ca}}}} = v_{\mathit{\ensuremath{\operatorname{ca}}}}$ otherwise we have closed the cycle and know that $e$ is not part of it). Note that for forward edges that are part of cycles, the cycles may involve multiple back edges. For the correct cyclic ancestor to be identified in this case, the back edges must be searched recursively to correctly identify the earliest cyclic ancestor. $\qedsymbol$

Theorem: On termination, algorithm cyclic edge detector correctly identifies the set $E_c$ of all edges involved in a cycle.

Proof. The key is that the invariant of Lemma 1 also holds when, for a given vertex $a \in \mathit{\ensuremath{\operatorname{BV}}}_t \cup \mathit{\ensuremath{\operatorname{GV}}}_t,$ $a_{\mathit{\ensuremath{\operatorname{ca}}}} = a$ . That is, if $a$ is identified as the cyclic ancestor of some cycle then on completion of the algorithm there exists a directed path along BLACK edges from $a$ to itself and using the same rule that is used to identify cyclic ancestors of nodes, each of these edges will have been added to $E_c$ . $\qedsymbol$