[FrontPage] [TitleIndex] [WordIndex

Note: You are looking at a static copy of the former PineWiki site, used for class notes by James Aspnes from 2003 to 2012. Many mathematical formulas are broken, and there are likely to be other bugs as well. These will most likely not be fixed. You may be able to find more up-to-date versions of some of these notes at http://www.cs.yale.edu/homes/aspnes/#classes.

For more up-to-date notes see http://www.cs.yale.edu/homes/aspnes/classes/465/notes.pdf.

1. Knowledge

Let's suppose we have a collection of predicates (e.g. p) for describing states of the system, and that we have a modal operator Ki such that Ki p means that process i "knows" that p is true. Exactly what it means that process i knows that p is true is a bit up for grabs, but a reasonable interpretation is that p is true in every execution consistent with what p saw directly. Alternatively, we could give a set of axioms for what i knows, like the traditional axiom system that modal logicians call S5:

Any propositional tautology is true.

(Ki p /\ Ki (p => q)) => Ki q. (Modus ponens applies to what I know.)


Ki p => p. (I know only true things.)


Ki => Ki Ki p. (I know what I know.)


¬Ki p => Ki ¬Ki p. (I know what I don't know.)

and inference rules:


From p and p => q infer q.


From p infer Ki p. (Note that this does not mean that process i knows everything that is true, just that if we can prove from whatever our initial position of ignorance that p is true, so can process p.)

S5 was invented to talk about necessity rather than knowledge (ultimately in order to clarify ontological proofs of the existence of God!), but it works for knowlege too. Note that we can add a superscript to Ki to get Kit, what i knows at time t. In this case we probably also want to add an axiom Kit p => Kit+a p so that i doesn't forget anything.

(Some philosophers like to drop some of these axioms or add others. See Fagin and Halpern, Reasoning about knowledge and probability, JACM 41(2):340-367, 1994 for an extensive discussion of appropriate axiom systems for distributed systems; this is also where the above description of S5 is taken from.)

If processes are honest and sufficiently talkative, then we can add an axiom that says that if i sends j a message at round t that is delivered in round t+1 (in a synchronous system), then Kjt p => Kit+1 p. This can generate complicated chains of knowledge, e.g. K1 K2 ¬K1 p "Process 1 knows that process 2 knows that process 1 doesn't know p." Many algorithms can be analyzed by looking at how such chains of knowledge evolve over time.

2. Common knowledge

Let E p = K1 p /\ K2 p /\ K3 p ... Kn p be the statement "everybody knows p." Define Ek p = p if k = 0 and E Ek-1 p for k > 0. Finally, define Cp as the infinite AND of Ek p for all k, i.e.

If "C p" holds, then the processes are said to have common knowledge of p. The notion of common knowledge was developed by the philosopher David_Lewis, but is known in ComputerScience mostly because of the work of Halpern and Moses (PODC 1984 applying it to the CoordinatedAttack problem.

3. Common knowledge and coordinated attack

Basic idea:


2014-06-17 11:58