Theory MuddyChildren
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}.
›