theory MuddyChildren imports ClockView SPRViewDet begin (*>*)
subsection‹The Muddy Children›
text‹
label{sec:kbps-theory-mc}
first example of a multi-agent broadcast scenario is the classic
children puzzle, one of a class of such puzzles that exemplify
-obvious reasoning about mutual states of knowledge. It goes as 🍋‹‹\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}
puzzle relies essentially on \emph{synchronous public broadcasts}
particular facts \emph{common knowledge}, and that agents are
of the requisite logical inference.
the mother has complete knowledge of the situation, we integrate
behaviour into the environment. Each agent $\mbox{child}_i$
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}
$\hat{\mathbf{K}}_a ‹φ›$ abbreviates $\mathbf{K}_a ‹φ›\ ‹∨›\ \mathbf{K}_a ‹¬φ›$.
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}
model records a child's initial observation of the mother's
and the muddiness of the other children in her initial
state, and these states are not changed by @{term
envTrans"}. The recurring common observation is all of the children's
responses to the mother's questions. Being able to distinguish
observations is crucial to making this a broadcast scenario.
the algorithm for three children and minimising using
's algorithm yields the automaton in Figure~\ref{fig:mc} for \mbox{child}_0$. The initial transitions are labelled with the
observation, i.e., the cleanliness ``C'' or muddiness ``M'' of
other two children. The dashed initial transition covers the case
everyone is clean; in the others the mother has announced that
is dirty. Later transitions simply record the actions
by each of the agents, where ``K'' is the first action in
above KBP, and ``N'' the second. Double-circled states are those
which $\mbox{child}_0$ knows whether she is muddy, and
-circled where she does not.
essence the child counts the number of muddy foreheads she sees and
that many rounds before announcing that she knows.
that a solution to this puzzle is beyond the reach of the clock
as it requires (in general) remembering the sequence of
broadcasts of length proportional to the number of
. We discuss this further in \S\ref{sec:kbps-muddychildren}.
definition
envTrans :: "EnvAct ==> (Agent ==> ChildAct) ==> GlobalState ==> GlobalState" where "envTrans eact aact s ≡ s ( es := envTransES eact aact (es s) )"
(* Common observation: the actions of the agents. *)
definition"envObsC ≡ snd"
definition
envVal :: "GlobalState ==> Proposition ==> bool" where "envVal ≡ λs p. case p of Dirty a ==> (case es s of ((c0, c1, c2), _) ==> (case a of Child0 ==> c0 | Child1 ==> c1 | Child2 ==> c2))"
(* FIXME This is a bit grot, this definition is already made for us in the locale. *)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
