# Faster Algorithms for Mining Shortest-Path Distances from Massive Time-Evolving Graphs
## 3 A New Algorithm: queue-2 hc
### recover Phase
Therefore, vertices in OUT (IN, respectively) are not connected to (are not reachable from, respectively) \(h\) and hence the visit for \(h\) can terminate. If Q is not empty instead, the vertex \(v\) with minimum priority, say \(\delta\), is extracted and, if \(\delta<PQ(v,h,L,\texttt{IDX}(h))\) (or \(\delta<PQ(h,v,L,\texttt{IDX}(h))\), respectively) then new label entry \((h,\delta)\) is added to \(L_{out}(v)\) (\(L_{in}(v)\), respectively). In particular, if the value of \(\delta\) is smaller than the distance returned by PQ, it follows that the shortest path being discovered is not encoded in the labeling, i.e., that pair \(v,h\) is not covered by L. Please note that the pruning test considers vertices up to index \(\textsc{IDX}(h)\) in the ordering, as done by \(\textsc{resume-2 hc}\) to preserve minimality of the labeling (see [8] for more details on _prefiral correctness_). Now, if a new label entry is added, then only the neighbors of \(v\) that are in \(\textsc{OUT}\) (\(\textsc{IN}\), resp.) are scanned in a relaxation step (see Algorithm 8) to add them to the queue or to decrease their key. In fact, vertices outside \(\textsc{OUT}\) (\(\textsc{IN}\), resp.) by Lemma 2 already satisfy the cover property to \(h\). The algorithm terminates when the queue is empty for all vertices in \(\textsc{OUT}\) and \(\textsc{IN}\). We are now ready to conclude the proof of correctness of Algorithm queue-2 hc. Theorem 3.1: _Let \(F^{L}_{G}(x,y)\) and \(B^{L}_{G}(x,y)\) the forward and backward cover graphs, respectively. Let \(L^{\prime\prime}\) be the labeling returned by Algorithm 4 when applied to graph \(G^{\prime}\), labeling \(L^{\prime}\) and set \(\textsc{OUT}\) and \(\textsc{IN}\), respectively. Then, \(L^{\prime\prime}\) is a minimal well-ordered 2-hop-cover labeling that covers \(G^{\prime}\), i.e., for any pair \(u,v\in V\) we have \(Q(u,v,L^{\prime\prime})=d_{G^{\prime}}(u,v)\)._  
Proof. : First of all, observe that any pair that can have the cover property not satisfied for \(G^{\prime}\) (see Property 4) is considered by Algorithm recover, either in line 5 or in line 8. We focus on proving the claim for all pairs \(h,t\) for a given vertex \(h\in\textsc{OUT}\) (the proof for the case \(h\in\textsc{IN}\) is symmetric). The proof is by induction on the number \(|Q|\) of deleteMin operations on the queue \(Q\). Observe that if \(|Q|=0\) we have that no vertex \(t\in\textsc{IN}\) has at least one viable neighbor. It is easy to see that this implies none of such vertices are reachable, in \(G^{\prime}\), from \(h\) in \(G^{\prime}\). In fact, any viable neighbor, say \(w\), is outside \(\textsc{IN}\) hence pair \(h,w\) is covered by \(L^{\prime}\) by Lemma 4. Moreover, all entries in \(L^{\prime}\) are correct. Thus, \(d_{G^{\prime}}(u,v)=Q(u,v,L^{\prime\prime})=\infty\) and the claim holds. _Base case_ (\(|Q|=1\)). In this case, we have that one vertex, say \(w\), has a viable neighbor and \(w>h\). By Lemma 2 it follows that \(\delta=d^{\prime}_{G}(h,w)\) and hence the cover property is tested in line 27. If \(\delta\) is smaller than \(PQ(h,w,L^{\prime\prime},\textsc{IDX}(h))\), a label entry \((h,\delta)\) is added to \(L_{out}(w)\) thus the claim follows. Otherwise, we have that \(PQ(h,w,L^{\prime\prime},\textsc{IDX}(h)=d^{\prime}_{G}(h,w)\) which, in turn, implies that \(Q(h,w,L^{\prime\prime})=d^{\prime}_{G}(h,w)\) by the definition of \(PQ\). _Inductive Hypothesis._ We assume the claim holds when \(|Q|=k\), i.e., we have \(Q(h,w,L^{\prime\prime})=d^{\prime}_{G}(h,w)\) and \(w<h\) for any vertex \(t\) among the \(k\) vertices that have been extracted up to this point. _Inductive Step._ We consider the case when \(|Q|=k+1\). Observe that the next extracted vertex \(v\) must be a neighbor of some vertex, say \(v^{\prime}\), processed in one of the previous \(k\) iterations, as otherwise \(v\) would not be in \(Q\). Therefore, we have that \(\delta=d^{\prime}_{G}(h,v)\), as otherwise either \(v\) would not be extracted to be the minimum, or \(v^{\prime}\) would not be among the previously extracted vertices.