Pré-visualização9 páginas

Process chain A message chain in an execution is a sequence of messages \u3008mik , mik\u22121 , mik\u22122 , . . ., mi1 \u3009 such that for all 0 < j \u2264 k, mij is sent by process ij to process ij\u22121 and receive(mij ) \u227a send(mij\u22121 ). The message chain identifies process chain \u3008i0, i1, . . . , ik\u22122, ik\u22121, ik \u3009. If \u3c6 is false and later P1 knows that P2 knows that . . . Pk knows \u3c6, then there must exist a process chain \u3008i1, i2, . . . ik \u3009. Indistinguishability of cuts (a, c) \u223ci (a\u2032, c \u2032) is expressible in the interleaving model using isomorphism of executions. Let: I x , y , z denote executions or execution prefixes in interleaving model. I xp: projection of execution x on process p. Isomorphism of executions 1 For x and y , relation x[p]y is true iff xp = yp . 2 For x and y and a process group G , relation x[G ]y is true iff, for all p \u2208 G , xp = yp . 3 Let Gi be process group i and let k > 1. Then, x[G0,G1, . . . ,Gk ]z if and only if x[G0,G1, . . . ,Gk\u22121]y and y [Gk ]z. Exercise: Examine isomorphism (items 1,2,3 each) using Kripke structures! A. Kshemkalyani and M. Singhal (Distributed Computing) Reasoning with Knowledge CUP 2008 24 / 29 Distributed Computing: Principles, Algorithms, and Systems Knowledge Transfer (1) Message chain and Process chain A message chain in an execution is a sequence of messages \u3008mik , mik\u22121 , mik\u22122 , . . ., mi1 \u3009 such that for all 0 < j \u2264 k, mij is sent by process ij to process ij\u22121 and receive(mij ) \u227a send(mij\u22121 ). The message chain identifies process chain \u3008i0, i1, . . . , ik\u22122, ik\u22121, ik \u3009. If \u3c6 is false and later P1 knows that P2 knows that . . . Pk knows \u3c6, then there must exist a process chain \u3008i1, i2, . . . ik \u3009. Indistinguishability of cuts (a, c) \u223ci (a\u2032, c \u2032) is expressible in the interleaving model using isomorphism of executions. Let: I x , y , z denote executions or execution prefixes in interleaving model. I xp: projection of execution x on process p. Isomorphism of executions 1 For x and y , relation x[p]y is true iff xp = yp . 2 For x and y and a process group G , relation x[G ]y is true iff, for all p \u2208 G , xp = yp . 3 Let Gi be process group i and let k > 1. Then, x[G0,G1, . . . ,Gk ]z if and only if x[G0,G1, . . . ,Gk\u22121]y and y [Gk ]z. Exercise: Examine isomorphism (items 1,2,3 each) using Kripke structures! A. Kshemkalyani and M. Singhal (Distributed Computing) Reasoning with Knowledge CUP 2008 24 / 29 Distributed Computing: Principles, Algorithms, and Systems Knowledge Transfer (2) Knowledge operator in the interleaving model p knows \u3c6 at execution x if and only if, for all executions y such that x [p]y , \u3c6 is true at y . When a message is received, set of isomorphic executions can only decrease. Knowledge transfer theorem For process groups G1, . . ., Gk , and executions x and y , (KG1KG2 . . .KGk (\u3c6) at x and x [G1, . . .Gk ]y) =\u21d2 KGk (\u3c6) at y . Proof by induction. Trivial for k = 1. k, k > 1: We infer \u2203 some z | x [G1, . . .Gk\u22121]z and z[Gk ]y . From KG1KG2 . . .KGk\u22121 [KGk (\u3c6)] at x , and from the induction hypothesis: infer that KGk\u22121 [KGk (\u3c6)] at z . Hence, KGk (\u3c6) at z . As z[Gk ]y , KGk (\u3c6) at y . I.t.o. Kripke structures, there is a path from state node x = s0 to state node y = sk , via state nodes s1, s2, . . ., sk\u22121, such that the k edges (si , si+1), 0 \u2264 i \u2264 k \u2212 1 are labeled by Gi+1. A. Kshemkalyani and M. Singhal (Distributed Computing) Reasoning with Knowledge CUP 2008 25 / 29 Distributed Computing: Principles, Algorithms, and Systems Knowledge Transfer (2) Knowledge operator in the interleaving model p knows \u3c6 at execution x if and only if, for all executions y such that x [p]y , \u3c6 is true at y . When a message is received, set of isomorphic executions can only decrease. Knowledge transfer theorem For process groups G1, . . ., Gk , and executions x and y , (KG1KG2 . . .KGk (\u3c6) at x and x [G1, . . .Gk ]y) =\u21d2 KGk (\u3c6) at y . Proof by induction. Trivial for k = 1. k, k > 1: We infer \u2203 some z | x [G1, . . .Gk\u22121]z and z[Gk ]y . From KG1KG2 . . .KGk\u22121 [KGk (\u3c6)] at x , and from the induction hypothesis: infer that KGk\u22121 [KGk (\u3c6)] at z . Hence, KGk (\u3c6) at z . As z[Gk ]y , KGk (\u3c6) at y . I.t.o. Kripke structures, there is a path from state node x = s0 to state node y = sk , via state nodes s1, s2, . . ., sk\u22121, such that the k edges (si , si+1), 0 \u2264 i \u2264 k \u2212 1 are labeled by Gi+1. A. Kshemkalyani and M. Singhal (Distributed Computing) Reasoning with Knowledge CUP 2008 25 / 29 Distributed Computing: Principles, Algorithms, and Systems Knowledge Transfer (2) Knowledge operator in the interleaving model p knows \u3c6 at execution x if and only if, for all executions y such that x [p]y , \u3c6 is true at y . When a message is received, set of isomorphic executions can only decrease. Knowledge transfer theorem For process groups G1, . . ., Gk , and executions x and y , (KG1KG2 . . .KGk (\u3c6) at x and x [G1, . . .Gk ]y) =\u21d2 KGk (\u3c6) at y . Proof by induction. Trivial for k = 1. k, k > 1: We infer \u2203 some z | x [G1, . . .Gk\u22121]z and z[Gk ]y . From KG1KG2 . . .KGk\u22121 [KGk (\u3c6)] at x , and from the induction hypothesis: infer that KGk\u22121 [KGk (\u3c6)] at z . Hence, KGk (\u3c6) at z . As z[Gk ]y , KGk (\u3c6) at y . I.t.o. Kripke structures, there is a path from state node x = s0 to state node y = sk , via state nodes s1, s2, . . ., sk\u22121, such that the k edges (si , si+1), 0 \u2264 i \u2264 k \u2212 1 are labeled by Gi+1. A. Kshemkalyani and M. Singhal (Distributed Computing) Reasoning with Knowledge CUP 2008 25 / 29 Distributed Computing: Principles, Algorithms, and Systems Knowledge Transfer (2) Knowledge operator in the interleaving model p knows \u3c6 at execution x if and only if, for all executions y such that x [p]y , \u3c6 is true at y . When a message is received, set of isomorphic executions can only decrease. Knowledge transfer theorem For process groups G1, . . ., Gk , and executions x and y , (KG1KG2 . . .KGk (\u3c6) at x and x [G1, . . .Gk ]y) =\u21d2 KGk (\u3c6) at y . Proof by induction. Trivial for k = 1. k, k > 1: We infer \u2203 some z | x [G1, . . .Gk\u22121]z and z[Gk ]y . From KG1KG2 . . .KGk\u22121 [KGk (\u3c6)] at x , and from the induction hypothesis: infer that KGk\u22121 [KGk (\u3c6)] at z . Hence, KGk (\u3c6) at z . As z[Gk ]y , KGk (\u3c6) at y . I.t.o. Kripke structures, there is a path from state node x = s0 to state node y = sk , via state nodes s1, s2, . . ., sk\u22121, such that the k edges (si , si+1), 0 \u2264 i \u2264 k \u2212 1 are labeled by Gi+1. A. Kshemkalyani and M. Singhal (Distributed Computing) Reasoning with Knowledge CUP 2008 25 / 29 Distributed Computing: Principles, Algorithms, and Systems Knowledge Transfer (2) Knowledge operator in the interleaving model p knows \u3c6 at execution x if and only if, for all executions y such that x [p]y , \u3c6 is true at y . When a message is received, set of isomorphic executions can only decrease. Knowledge transfer theorem For process groups G1, . . ., Gk , and executions x and y , (KG1KG2 . . .KGk (\u3c6) at x and x [G1, . . .Gk ]y) =\u21d2 KGk (\u3c6) at y . Proof by induction. Trivial for k = 1. k, k > 1: We infer \u2203 some z | x [G1, . . .Gk\u22121]z and z[Gk ]y . From KG1KG2 . . .KGk\u22121 [KGk (\u3c6)] at x , and from the induction hypothesis: infer that KGk\u22121 [KGk (\u3c6)] at z . Hence, KGk (\u3c6) at z . As z[Gk ]y , KGk (\u3c6) at y . I.t.o. Kripke structures, there is a path from state node x = s0 to state node y = sk , via state nodes s1, s2, . . ., sk\u22121, such that the k edges (si , si+1), 0 \u2264 i \u2264 k \u2212 1 are labeled by Gi+1. A. Kshemkalyani and M. Singhal (Distributed Computing) Reasoning with Knowledge CUP 2008 25 / 29 Distributed Computing: Principles, Algorithms, and Systems Knowledge Transfer (3) Knowledge gain theorem For processes P1, . . ., Pk , and executions x and y , where x is a prefix of y , let ¬Kk (\u3c6) at x and K1K2 . . .Kk (\u3c6) at y . Then there is a process chain \u3008i1, . . . ik\u22121, ik\u3009 in (x , y). This formalizes