Y. Afek, S. Kutten, and M. Yung, The local detection paradigm and its applications to self-stabilization, Theoretical Computer Science, vol.186, issue.1-2, pp.199-229, 1997.
DOI : 10.1016/S0304-3975(96)00286-1

S. Alstrup, P. Bille, and T. Rauhe, Labeling Schemes for Small Distances in Trees, 14th ACM-SIAM Symposium on Discrete Algorithms (SODA), pp.689-698, 2003.
DOI : 10.1137/S0895480103433409

S. Alstrup, C. Gavoille, H. Kaplan, and T. Rauhe, Nearest common ancestors, Proceedings of the fourteenth annual ACM symposium on Parallel algorithms and architectures , SPAA '02, pp.258-264, 2002.
DOI : 10.1145/564870.564914
URL : https://hal.archives-ouvertes.fr/hal-00307617

S. Alstrup and T. Rauhe, Small induced-universal graphs and compact implicit graph representations, The 43rd Annual IEEE Symposium on Foundations of Computer Science, 2002. Proceedings., pp.53-62, 2002.
DOI : 10.1109/SFCS.2002.1181882

H. Arfaoui, P. Fraigniaud, D. Ilcinkas, and F. Mathieu, Distributedly Testing Cycle-Freeness, 40th Int. Workshop on Graph-Theoretic Concepts in Computer Science (WG), pp.15-28, 2014.
DOI : 10.1007/978-3-319-12340-0_2
URL : https://hal.archives-ouvertes.fr/hal-01084297

H. Arfaoui, P. Fraigniaud, and A. Pelc, Local Decision and Verification with Bounded-Size Outputs, 15th Symp. on Stabilization, Safety, and Security of Distributed Systems (SSS), pp.133-147, 2013.
DOI : 10.1007/978-3-319-03089-0_10
URL : https://hal.archives-ouvertes.fr/hal-00922700

B. Awerbuch, S. Kutten, Y. Mansour, B. Patt-shamir, and G. Varghese, Time optimal self-stabilizing synchronization, Proceedings of the twenty-fifth annual ACM symposium on Theory of computing , STOC '93, pp.652-661, 1993.
DOI : 10.1145/167088.167256

B. Awerbuch, B. Patt-shamir, and G. Varghese, Self-stabilization by local checking and correction, [1991] Proceedings 32nd Annual Symposium of Foundations of Computer Science, pp.268-277, 1991.
DOI : 10.1109/SFCS.1991.185378

L. Blin, P. Fraigniaud, and B. Patt-shamir, On Proof-Labeling Schemes versus Silent Self-stabilizing Algorithms, 16th Int. Symp. on Stabilization, Safety, and Security of Distributed Systems (SSS), pp.18-32, 2014.
DOI : 10.1007/978-3-319-11764-5_2
URL : https://hal.archives-ouvertes.fr/hal-01102123

E. Cohen, E. Halperin, H. Kaplan, and U. Zwick, Reachability and Distance Queries via 2-Hop Labels, 13th ACM-SIAM Symposium on Discrete Algorithms (SODA), pp.937-946, 2002.
DOI : 10.1137/S0097539702403098

A. D. Sarma, S. Holzer, L. Kor, A. Korman, D. Nanongkai et al., Distributed Verification and Hardness of Distributed Approximation, SIAM Journal on Computing, vol.41, issue.5, pp.1235-1265, 2012.
DOI : 10.1137/11085178X

P. Fraigniaud and C. Gavoille, Routing in Trees, 28th International Colloquium on Automata, Languages and Programming (ICALP), pp.757-772, 2001.
DOI : 10.1007/3-540-48224-5_62
URL : https://hal.archives-ouvertes.fr/hal-00307398

P. Fraigniaud and C. Gavoille, A Space Lower Bound for Routing in Trees, 19th Symp. on Theoretical Aspects of Computer Science (STACS), pp.65-75, 2002.
DOI : 10.1007/3-540-45841-7_4
URL : https://hal.archives-ouvertes.fr/hal-00307398

P. Fraigniaud and A. Korman, On randomized representations of graphs using short labels, Proceedings of the twenty-first annual symposium on Parallelism in algorithms and architectures, SPAA '09, pp.131-137, 2009.
DOI : 10.1145/1583991.1584031

P. Fraigniaud, A. Korman, and D. Peleg, Towards a complexity theory for local distributed computing, Journal of the ACM, vol.60, issue.5, p.35, 2013.
DOI : 10.1145/2499228

P. Fraigniaud, S. Rajsbaum, and C. Travers, Locality and Checkability in Wait-Free Computing, Distributed Computing, vol.15, issue.4, pp.223-242, 2013.
DOI : 10.1007/BF01961540
URL : https://hal.archives-ouvertes.fr/hal-00992781

P. Fraigniaud, S. Rajsbaum, and C. Travers, On the Number of Opinions Needed for Fault-Tolerant Run-Time Monitoring in Distributed Systems, 5th International Conference on Runtime Verification (RV), pp.92-107, 2014.
DOI : 10.1007/978-3-319-11164-3_9
URL : https://hal.archives-ouvertes.fr/hal-01102121

C. Gavoille, M. Katz, N. A. Katz, C. Paul, and D. Peleg, Approximate distance labeling schemes, 9th European Symposium on Algorithms (ESA), pp.476-487, 2001.

C. Gavoille and C. Paul, Split Decomposition and Distance Labelling: An Optimal Scheme For Distance Hereditary Graphs, Electronic Notes in Discrete Mathematics, vol.10, pp.117-120, 2001.
DOI : 10.1016/S1571-0653(04)00374-9

C. Gavoille, D. Peleg, S. Perennes, and R. Raz, Distance labeling in graphs, 12th ACM Symposium on Discrete Algorithms (SODA), pp.210-219, 2001.
DOI : 10.1016/j.jalgor.2004.05.002
URL : https://hal.archives-ouvertes.fr/hal-00307381

M. Göös and J. Suomela, Locally checkable proofs, 30th ACM Symp. on Principles of Distributed Computing (PODC), pp.159-168, 2011.

J. E. Hopcroft and R. E. Tarjan, Algorithm 447: efficient algorithms for graph manipulation, Communications of the ACM, vol.16, issue.6, pp.372-378, 1973.
DOI : 10.1145/362248.362272

G. Itkis and L. A. Levin, Fast and lean self-stabilizing asynchronous protocols, Proceedings 35th Annual Symposium on Foundations of Computer Science, pp.226-239, 1994.
DOI : 10.1109/SFCS.1994.365691

S. Kannan, M. Naor, and S. Rudich, Implicit representation of graphs, Proceedings of the twentieth annual ACM symposium on Theory of computing , STOC '88, pp.596-603, 1992.
DOI : 10.1145/62212.62244

H. Kaplan and T. Milo, Short and Simple Labels for Small Distances and Other Functions, 7th Int. Workshop on Algorithms and Data Structures (WADS), pp.246-257, 2001.
DOI : 10.1007/3-540-44634-6_23

M. Katz, N. A. Katz, A. Korman, and D. Peleg, Labeling Schemes for Flow and Connectivity, 13th ACM-SIAM Symposium on Discrete Algorithms (SODA), pp.927-936, 2002.
DOI : 10.1137/S0097539703433912

M. Katz, N. A. Katz, and D. Peleg, Distance labeling schemes for well-separated graph classes, Discrete Applied Mathematics, vol.145, issue.3, pp.384-402, 2005.
DOI : 10.1016/j.dam.2004.03.005

A. Korman, Labeling schemes for vertex connectivity, ACM Transactions on Algorithms, vol.6, issue.2, p.2010

A. Korman and S. Kutten, Distributed verification of minimum spanning trees, Distributed Computing, vol.26, issue.1, pp.253-266, 2007.
DOI : 10.1007/s00446-007-0025-1

A. Korman, S. Kutten, and T. Masuzawa, Fast and compact self stabilizing verification, computation, and fault detection of an MST, 30th Annual ACM Symposium on Principles of Distributed Computing (PODC), pp.311-320, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01240211

A. Korman, D. Peleg, and Y. Rodeh, Constructing Labeling Schemes through Universal Matrices, Algorithmica, vol.51, issue.3, pp.641-652, 2010.
DOI : 10.1007/s00453-008-9226-7

E. Kushilevitz and N. Nisan, Communication complexity, 1997.

C. H. Papadimitriou, Computational Complexity, 1994.

D. Peleg, Proximity-Preserving Labeling Schemes and Their Applications, 25th International Workshop Graph- Theoretic Concepts in Computer Science (WG), pp.30-41, 1999.
DOI : 10.1007/3-540-46784-X_5

D. Peleg, Informative labeling schemes for graphs, Theoretical Computer Science, vol.340, issue.3, pp.577-593, 2005.
DOI : 10.1016/j.tcs.2005.03.015

R. E. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972.
DOI : 10.1137/0201010

M. Thorup, Compact oracles for reachability and approximate distances in planar digraphs, 42nd Symp. on Foundations of Computer Science (FOCS), pp.242-251, 2001.

M. Thorup and U. Zwick, Compact routing schemes, Proceedings of the thirteenth annual ACM symposium on Parallel algorithms and architectures , SPAA '01, pp.1-10, 2001.
DOI : 10.1145/378580.378581

B. Alice, Alice simulates the nodes in V 0 of G(x, x), and Bob simulates the nodes in V 1 of G(y, y). The only communication between Alice and Bob induced by this simulation consists of exchanging the bits that are crossing link

G. Let, G has n nodes, and, by Claim C.2, we have x = y ?? Sym

. Hence, Thus, with probability at least 2/3, both Alice and Bob returns TRUE. Similarly, if x = y, then, with probability at least 2/3, at least one node of G outputs FALSE. Hence, with probability at least 2/3, either Alice, or Bob, or both, returns FALSE. Therefore, the 2-party protocol is correct with probability at least 2/3. In this protocol, Alice and Bob exchange ? bits. If ? = o(log n) then ? = o(log ?) as well since n ? ?, This would be in contradiction with the lower bound in Lemma 3.2. Thus the verification complexity of (p, v) is at least ?(log n)

C. Lemma, 3 For any function k(n), any randomized proof-labeling scheme for (F k , Unif) has verification complexity ?(log k)

C. F. Moreover, C is a cycle, i.e., not satisfying the predicate. Therefore, by Theorem 4.7, the verification complexity of (F, acyclicity) is ?(log log n). Hence, since F ? F con , the verification complexity of, ST ) is ?(log log n)