Universal covers, color refinement, and two-variable logic with counting quantifiers: Lower bounds for the depth

Using basic tools of finite model theory, we answer a question in theory of distributed computing posed in 1995 by Nancy Norris [Discr. Appl. Math. 56:61-74]. Given a graph $G$ and its vertex $x$, let $U_x(G)$ denote the universal cover of $G$ obtained by unfolding $G$ into a tree starting from $x$. Suppose that two graphs $G$ and $H$ both consist of $n$ nodes. What is the minimum number $T=T(n)$ such that the isomorphism of $U_x(G)$ and $U_y(H)$ surely follows from the isomorphism of these rooted trees truncated at depth $T$? We show that $T(n)=(2-o(1))n$.