Local Certification of Reachability

Local Certification of Reachability Oliver Bachtler, Tim Bergner, and Sven O. Krumke Department of Mathematics TU Kaiserslautern International Network Optimization Conference, 2022 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information My kingdom should be cubic. BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information My kingdom should be cubic. BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information Looks good. BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information This is wrong, notify the king! BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information I also want my kingdom to be bipartite. BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information I also want my kingdom to be bipartite. BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information Is this really bipartite? BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information Don’t forget your orders! BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 Motivation In essence: want to verify that a graph has a certain property. But: we only see a local view around every vertex. ⇒limited information Order has been established! BA B A B A AB A B A B Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 18 The Setting ▶Gis a class of graphs (all undirected graphs). ▶F⊆ G is a subset of Gsatisfying a certain property (cubic,bipartite). ▶Each vertex of a graph has an identity, which are ▶distinct or ▶identical, in which case the graph is anonymous. ▶Vertices also have labels, which contain problem-specific information. Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 4 / 18 The Setting ▶Gis a class of graphs (all undirected graphs). ▶F⊆ G is a subset of Gsatisfying a certain property (cubic,bipartite). ▶Each vertex of a graph has an identity, which are ▶distinct or ▶identical, in which case the graph is anonymous. ▶Vertices also have labels, which contain problem-specific information. Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 4 / 18 The Setting ▶Gis a class of graphs (all undirected graphs). ▶F⊆ G is a subset of Gsatisfying a certain property (cubic,bipartite). ▶Each vertex of a graph has an identity, which are ▶distinct or ▶identical, in which case the graph is anonymous. ▶Vertices also have labels, which contain problem-specific information. Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 4 / 18 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 5 / 18 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 5 / 18 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 5 / 18 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 5 / 18 Provers Definition (Prover) ▶Aprover (for F) is a function Pthat maps G∈ F to a proof for G. ▶The size of Pis the maximum size of any proof it assigns to F. Definition (Proof) ▶Aproof for a graph Gis a function P:V(G)→ {0,1}∗that assigns a binary certificate to each vertex of G. ▶The size of a proof is the length of its longest certificate. 0 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 5 / 18 Verifiers Definition (Verifier) ▶Averifier V(for G) is a function that maps triples (G,P,v)to {0,1} and satisfies V(G,P,v) = V(G[N[v]],P[N[v]],v)for all G,P,v. ▶Vaccepts a proof Pat v∈V(G)if V(G,P,v) = 1. ▶Vaccepts a proof Pfor a graph Gif it accepts at all v∈V(G)and ▶Vrejects the proof otherwise. 0 1 0 1 00 1 0 1 01 1 1 01 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 6 / 18 Verifiers Definition (Verifier) ▶Averifier V(for G) is a function that maps triples (G,P,v)to {0,1} and satisfies V(G,P,v) = V(G[N[v]],P[N[v]],v)for all G,P,v. ▶Vaccepts a proof Pat v∈V(G)if V(G,P,v) = 1. ▶Vaccepts a proof Pfor a graph Gif it accepts at all v∈V(G)and ▶Vrejects the proof otherwise. 0 1 0 1 00 1 0 1 01 1 1 01 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 6 / 18 Verifiers Definition (Verifier) ▶Averifier V(for G) is a function that maps triples (G,P,v)to {0,1} and satisfies V(G,P,v) = V(G[N[v]],P[N[v]],v)for all G,P,v. ▶Vaccepts a proof Pat v∈V(G)if V(G,P,v) = 1. ▶Vaccepts a proof Pfor a graph Gif it accepts at all v∈V(G)and ▶Vrejects the proof otherwise. 0 1 0 1 00 1 0 1 01 1 1 01 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 6 / 18 Proof Labelling Schemes Definition (Proof Labelling Scheme) ▶A pair π= (P,V)is a proof labelling scheme for F ⊆ G if ▶Vaccepts P(G)for all G∈ F. ▶Vrejects any graph not in F. ▶The size of πis the size of its prover. 0 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 7 / 18 Proof Labelling Schemes Definition (Proof Labelling Scheme) ▶A pair π= (P,V)is a proof labelling scheme for F ⊆ G if ▶Vaccepts P(G)for all G∈ F. ▶Vrejects any graph not in F. ▶The size of πis the size of its prover. 0 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 7 / 18 Proof Labelling Schemes Definition (Proof Labelling Scheme) ▶A pair π= (P,V)is a proof labelling scheme for F ⊆ G if ▶Vaccepts P(G)for all G∈ F. ▶Vrejects any graph not in F. ▶The size of πis the size of its prover. 0 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 7 / 18 Proof Labelling Schemes Definition (Proof Labelling Scheme) ▶A pair π= (P,V)is a proof labelling scheme for F ⊆ G if ▶Vaccepts P(G)for all G∈ F. ▶Vrejects any graph not in F. ▶The size of πis the size of its prover. 0 1 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 7 / 18 Examples (taken from Göös, Suomela 2016) Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 8 / 18 Back to the Motivation. Example (Cubic Graphs) ▶No proof needed: prover assigns every vertex an empty certificate. ▶The verifier at vchecks that vhas degree 3. ▶Accepts exactly the cubic graphs. ⇒A proof labelling scheme of size 0 exists for cubic graphs. Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 9 / 18 Back to the Motivation. Example (Cubic Graphs) ▶No proof needed: prover assigns every vertex an empty certificate. ▶The verifier at vchecks that vhas degree 3. ▶Accepts exactly the cubic graphs. ⇒A proof labelling scheme of size 0 exists for cubic graphs. Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 9 / 18 Back to the Motivation. Example (Cubic Graphs) ▶No proof needed: prover assigns every vertex an empty certificate. ▶The verifier at vchecks that vhas degree 3. ▶Accepts exactly the cubic graphs. ⇒A proof labelling scheme of size 0 exists for cubic graphs. Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 9 / 18 Back to the Motivation. Example (Cubic Graphs) ▶No proof needed: prover assigns every vertex an empty certificate. ▶The verifier at vchecks that vhas degree 3. ▶Accepts exactly the cubic graphs. ⇒A proof labelling scheme of size 0 exists for cubic graphs. Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 9 / 18 More Examples: Reachability Definition (st-Reachability) In the directed st-reachability problem ▶Gis the class of all directed graphs with a vertex sand t. ▶Fcontains those graphs in which tis reachable from s. stst Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 11 / 18 More Examples: Reachability Definition (st-Reachability) In the directed st-reachability problem ▶Gis the class of all directed graphs with a vertex sand t. ▶Fcontains those graphs in which tis reachable from s. stst Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 11 / 18 More Examples: Reachability Definition (st-Reachability) In the directed st-reachability problem ▶Gis the class of all directed graphs with a vertex sand t. ▶Fcontains those graphs in which tis reachable from s. stst Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 11 / 18 More Examples: Reachability Example (st-Reachability) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-reachability. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 12 / 18 More Examples: Reachability Example (st-Reachability) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-reachability. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 12 / 18 More Examples: Reachability Example (st-Reachability) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-reachability. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 12 / 18 More Examples: Reachability Example (st-Reachability) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-reachability. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 12 / 18 More Examples: Reachability Example (st-Reachability) ▶Use proof to specify a shortest path: prover assigns either 0 or 1 to each vertex to indicate whether it is on a fixed shortest path. ▶The verifier at vchecks that vhas two neighbours with proof 1 if it has proof 1 (or one if v=sor v=t). ▶Accepts exactly the graphs where tis reachable from s. ⇒A proof labelling scheme of size 1 exists for st-reachability. t s 1 1 1 1 0 0 0 0 1 1 1 0 0 0 1 0 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 12 / 18 More Examples: Reachability Example (Directed st-Reachability) ▶Use proof to specify a shortest path: prover assigns each vertex on a fixed shortest path a pointer to its successor. ▶The verifier at vchecks that if vhas a pointer, then one of its predecessors points to it (unless v=sor v=t). ▶Accepts exactly the directed graphs where tis reachable from s. ⇒A proof labelling scheme of size log(∆) exists for dir. st-reachability. t s 1 1 1 1 1 0 0 0 1 1 1 ε ε ε εε Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 13 / 18 More Examples: Reachability Example (Directed st-Reachability) ▶Use proof to specify a shortest path: prover assigns each vertex on a fixed shortest path a pointer to its successor. ▶The verifier at vchecks that if vhas a pointer, then one of its predecessors points to it (unless v=sor v=t). ▶Accepts exactly the directed graphs where tis reachable from s. ⇒A proof labelling scheme of size log(∆) exists for dir. st-reachability. t s 1 1 1 1 1 0 0 0 1 1 1 ε ε ε εε Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 13 / 18 More Examples: Reachability Example (Directed st-Reachability) ▶Use proof to specify a shortest path: prover assigns each vertex on a fixed shortest path a pointer to its successor. ▶The verifier at vchecks that if vhas a pointer, then one of its predecessors points to it (unless v=sor v=t). ▶Accepts exactly the directed graphs where tis reachable from s. ⇒A proof labelling scheme of size log(∆) exists for dir. st-reachability. t s 1 1 1 1 1 0 0 0 1 1 1 ε ε ε ε ε Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 13 / 18 How Difficult is Verifying Reachability? Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 14 / 18 Literature A. Korman, S. Kutten and D. Peleg Proof labeling schemes Distributed Computing, vol. 22, pp. 215–233, 2010. M. Göös and J. Suomela Locally Checkable Proofs in Distributed Computing Theory of Computing, vol. 12, no. 19, pp. 1–33, 2016. K. Foerster, T. Luedi, J. Seidel and R. Wattenhofer Local checkability, no strings attached: (A)cyclicity, reachability, loop free updates in SDNs Theoretical Computer Science, vol. 709, pp. 48–63, 2018. A. Korman and S. Kutten Distributed Verification of Minimum Spanning Trees PODC, 2006. L. Feuilloley et al. Compact Distributed Certification of Planar Graphs Algorithmica, vol. 83, no. 7, pp. 2215–2244, 2021. Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 15 / 18 Directed is Harder Than Undirected Reachability Goal: we want to prove that Theorem No proof labelling scheme of size o(log(∆)) exists for directed st-reachability on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 16 / 18 Directed is Harder Than Undirected Reachability Goal: we want to prove that Theorem No proof labelling scheme of size o(log(∆)) exists for directed st-reachability on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 16 / 18 Directed is Harder Than Undirected Reachability Goal: we want to prove that Theorem No proof labelling scheme of size o(log(∆)) exists for directed st-reachability on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 16 / 18 Directed is Harder Than Undirected Reachability Goal: we want to prove that Theorem No proof labelling scheme of size o(log(∆)) exists for directed st-reachability on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 16 / 18 Directed is Harder Than Undirected Reachability Goal: we want to prove that Theorem No proof labelling scheme of size o(log(∆)) exists for directed st-reachability on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 16 / 18 Directed is Harder Than Undirected Reachability Goal: we want to prove that Theorem No proof labelling scheme of size o(log(∆)) exists for directed st-reachability on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 16 / 18 Directed is Harder Than Undirected Reachability Goal: we want to prove that Theorem No proof labelling scheme of size o(log(∆)) exists for directed st-reachability on anonymous graphs. Idea: st u v st u v ab ab ab ab ab ab u v u v ab ab u v u v Result: forbids Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 16 / 18 Proof Sketch st Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 17 / 18 Proof Sketch Plan: add back-edges to forbid pairs forbidden st Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 17 / 18 Proof Sketch Goal: iteratively forbid more and more pairs forbidden st Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 17 / 18 Proof Sketch Goal: iteratively forbid more and more pairs forbidden st Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 17 / 18 Proof Sketch Want: same coloured forward-edges connected by back-edges and forbidden st Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 17 / 18 Proof Sketch How: use the Pigeon Hole Principle st Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 17 / 18 Proof Sketch Result: pair forbidden in all grey areas st Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 17 / 18 Proof Sketch Now: plug in recursively to forbid more pairs st Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 17 / 18 Summary We have: ▶formally defined proof labelling schemes, ▶illustrated these on several examples, and ▶showed that Θ(log(∆)) are needed to certify directed st-reachability. Contact: [email protected] Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 18 / 18 Almost all Other Examples Example (Universal Proof Labelling Scheme) ▶Assume we can decide for a graph G∈ G whether G∈ F. ▶Use proof to specify the graph: prover assigns the adjacency matrix A and the corresponding row to each vertex. ▶The verifier at vchecks that its neighbourhood is correct and that the graph given by Ais in F. ▶Accepts exactly the graphs in F. ⇒There exists a universal proof labelling scheme of size O(n2). A,7 A,1 A,8 A,2 A,9 A,3 A,10 A,4 A,11 A,5 A,12A,6 A,7 A,1 A,8 A,2 A,9 A,3 A,10 A,4 A,11 A,5 A,12A,6 Bachtler, Bergner, Krumke (TUK) Certifying Reachability INOC 2022 1 / 1