Chapter8
59 pág.

Chapter8


DisciplinaAlgorítimos Distribuídos32 materiais283 seguidores
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