(*<*) (* * Knowledge-based programs. * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com. * License: BSD *) theory MuddyChildren imports ClockView SPRViewDet begin (*>*) subsection‹The Muddy Children› text‹ \label{sec:kbps-theory-mc} Our first example of a multi-agent broadcast scenario is the classic muddy children puzzle, one of a class of such puzzles that exemplify non-obvious reasoning about mutual states of knowledge. It goes as follows \<^citep>‹‹\S1.1, Example~7.2.5› in "FHMV:1995"›: \begin{quotation} $N$ children are playing together, $k$ of whom get mud on their foreheads. Each can see the mud on the others' foreheads but not their own. A parental figure appears and says ``At least one of you has mud on your forehead.'', expressing something already known to each of them if $k > 1$. The parental figure then asks ``Does any of you know whether you have mud on your own forehead?'' over and over. Assuming the children are perceptive, intelligent, truthful and they answer simultaneously, what will happen? \end{quotation} This puzzle relies essentially on \emph{synchronous public broadcasts} making particular facts \emph{common knowledge}, and that agents are capable of the requisite logical inference. As the mother has complete knowledge of the situation, we integrate her behaviour into the environment. Each agent $\mbox{child}_i$ reasons with the following KBP: \begin{center} \begin{tabular}{lll} $\mathbf{do}$\\ & $\gcalt\ \hat{\mathbf{K}}_{\mbox{child}_i} \mbox{muddy}_i$ & $‹→›$ Say ``I know if my forehead is muddy''\\ & $\gcalt\ ‹¬›\hat{\mathbf{K}}_{\mbox{child}_i} \mbox{muddy}_i$ & $‹→›$ Say nothing\\ $\mathbf{od}$\\ \end{tabular} \end{center} where $\hat{\mathbf{K}}_a ‹φ›$ abbreviates $\mathbf{K}_a ‹φ›\ ‹∨›\ \mathbf{K}_a ‹¬φ›$. As this protocol is deterministic, we use the SPR algorithm of \S\ref{sec:kbps-theory-spr-deterministic-protocols}. \begin{wrapfigure}{r}{0.5\textwidth} \vspace{-20pt} \includegraphics[width=0.48\textwidth]{MC} \vspace{-10pt} \caption{The protocol of $\mbox{child}_0$.} \label{fig:mc} \end{wrapfigure} The model records a child's initial observation of the mother's pronouncement and the muddiness of the other children in her initial private state, and these states are not changed by @{term "envTrans"}. The recurring common observation is all of the children's public responses to the mother's questions. Being able to distinguish these observations is crucial to making this a broadcast scenario. Running the algorithm for three children and minimising using Hopcroft's algorithm yields the automaton in Figure~\ref{fig:mc} for $\mbox{child}_0$. The initial transitions are labelled with the initial observation, i.e., the cleanliness ``C'' or muddiness ``M'' of the other two children. The dashed initial transition covers the case where everyone is clean; in the others the mother has announced that someone is dirty. Later transitions simply record the actions performed by each of the agents, where ``K'' is the first action in the above KBP, and ``N'' the second. Double-circled states are those in which $\mbox{child}_0$ knows whether she is muddy, and single-circled where she does not. In essence the child counts the number of muddy foreheads she sees and waits that many rounds before announcing that she knows. Note that a solution to this puzzle is beyond the reach of the clock semantics as it requires (in general) remembering the sequence of previous broadcasts of length proportional to the number of children. We discuss this further in \S\ref{sec:kbps-muddychildren}. › (*<*)