# Asynchronous Muddy Children Puzzle
(work in progress)

Dafina Trufaș Ioan Teodorescu Denisa Diaconescu Traian Șerbănuță University of
Bucharest Runtime Verification, Inc. Vlad Zamfir Independent Researcher

###### Abstract

In this work-in-progress paper we explore using the recently introduced VLSM
formalism to define and reason about the dynamics of agent-based systems. To
this aim we use VLSMs to formally present several possible approaches to
modeling the interactions in the Muddy Children Puzzle as protocols that reach
consensus asynchronously.

##  1 Introduction

Formally modeling and reasoning about distributed systems with faults is a
challenging task [3]. We recently proposed the theory of _Validating Labeled
State transition and Message production systems (VLSMs)_ [10] as a general
approach to modeling and verifying distributed protocols executing in the
presence of faults.

The theory of VLSMs has its roots in the work on verification of the CBC
Casper protocol [11, 6] and follows the correct-by-construction methodology
for design and development. Even though the theory of VLSMs was primarily
designed for applications in faulty distributed systems, and in blockchains in
particular, the framework is general and flexible enough to capture various
types of problems in distributed systems. As an illustration, in this paper we
show how we can use VLSMs to model and solve (an asynchronous variant of) the
epistemic Muddy Children Puzzle [2].

##  2 Classical Muddy Children Puzzle

Let us begin by recalling the statement of the Muddy Children Puzzle and a
classical epistemic logic approach to solving it [2].

There are $n$ children playing together. It happens during their play that $k$
of the children get mud on their foreheads. Their father comes and says: ”At
least one of you has mud on your forehead.” (if $k>1$, thus expresses a fact
known to each of them before he spoke). The father then asks the following
question, repeatedly: ”Does any of you know whether you have mud on your own
forehead?”.

The initial assumptions are expressed in terms of common knowledge. Hence, we
shall assume that it is common knowledge that the father is truthful, that all
the children can and do hear the father, that all the children can and do see
which of the other children besides themselves have muddy foreheads and that
all the children are truthful and intelligent enough to make all the necessary
deductions during the game.

#### The solution

Let’s consider first the situation before the father speaks. We model the
problem by a Kripke structure
$M=(S,\models,\mathcal{K}_{1},\ldots,\mathcal{K}_{n})$ over $\Phi$, where:

  * •

$\Phi=\\{p_{i},\ldots,p_{n},p\\}$ ($p_{i}$ = ”child $i$ has a muddy forehead”
and $p$ = ”at least one child has a muddy forehead”). Note that $p$ could be
obtained as the disjunction of all $p_{i}$’s; however, for simplicity one can
consider it a primitive (albeit non-atomic) predicate.

  * •

$S$ is a set of $2^{n}$ states (corresponding to all the possible
configurations of clean and muddy children, represented as binary tuples)

  * •

$(M,(x_{1},\ldots,x_{n}))\models p_{i}$ iff $x_{i}=1$
$(M,(x_{1},\ldots,x_{n}))\models p$ iff $x_{i}=1$ for some $i$

  * •

$(s,t)\in\mathcal{K}_{i}$ if s and t are identical in all components except
eventually the $i^{th}$ one.

It’s crucial to remark that, in the absence of the father’s initial
announcement, the fact that ”there is at least one muddy child” is not common
knowledge and the state of knowledge never changes, no matter how many rounds
we take into account. Indeed, after the first question, all the children will
certainly answer ”No”, since they all consider possible the situation in which
they themselves do not have mud on their forehead. No information is gained
from this round and the situation remains the same after each of the following
ones, because each child considers possible a state in which they are clean.

Now let’s analyze how the epistemic context changes after the father speaks:
as mentioned above, the common knowledge is now larger (even though in the
case with $k\geq 2$ muddy children, $p$ was already common knowledge), because
of the public nature of the announcement. Let’s consider how the children
reason after all of them answered ”No” in the first round: it is obvious that
all of them eliminate the states containing one muddy child, since the others
could not have all answered ”No” otherwise. Continuing inductively, we obtain
that after $k$ rounds in which all the children answer ”No”, we can eliminate
from the problem graph all the nodes corresponding to states with at most $k$
muddy children. An immediate consequence of this is that after $k-1$ rounds,
it becomes common knowledge that there are at least $k$ muddy children. Hence,
the muddy children, who each only see $k-1$ muddy children will conclude that
they are muddy and answer ”Yes”.

There are multiple formalizations of this puzzle in the literature [9, 5, 7,
8, 4]; indeed it seems that each new formalism reasoning about knowledge
includes a modeling of this puzzle as a basic example of the expressiveness of
the formalism.

##  3 VLSMs – basic notions

We give a high-level presentation of the theory of VLSMs. More details can be
found in [10].

######  Definition 1 (VLSM).

A Validating Labeled State transition and Message production system (VLSM, for
short) is a structure of the form
$\mathcal{V}=(L,S,S_{0},M,M_{0},\tau,\mathit{\beta}),$ where $L$ is a set of
labels, $(S_{0}\subseteq)\ S$ is a non-empty set of (initial) states,
$(M_{0}\subseteq)\ M$ is a set of (initial) messages, $\tau:L\times S\times
M?\to S\times M?$ is a transition function which takes as arguments a label, a
state, and possibly a message, and outputs a state and possibly a message,
while $\mathit{\beta}$ is a validity constraint on the inputs of the
transition function.111For any set $M$ of messages, let
$M?=M\cup\\{\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\}$ be the extension
of $M$ with , where  stands for no-message.

The transition function in a VLSM is total; however, it indirectly becomes a
partial function since the validity constraint can filter out some of its
inputs. The set of labels in a VLSM can be used to model non-determinism: it
is possible to have multiple parallel transitions from a state using the same
input message, each with its own label.

#### Validity.

A transition is called constrained if the validity constraint holds on its
input. We denote a constrained transition
$\tau(l,s,m)=(s^{\prime},m^{\prime})$ by $s\xrightarrow[\ m\ \rightarrow\
m^{\prime}\ ]{l}s^{\prime}.$ A constrained trace is a sequence of constrained
transitions that starts in an initial state. A valid trace is inductively
defined as a constrained trace in which the input of each transition can be
emitted from a valid trace. A state is constrained/valid if there is a
constrained/valid trace leading to it. Similarly, a message is
constrained/valid if it is produced on a constrained/valid trace (we also
consider the no-message to be valid). A transition is called valid if it is a
constrained transition that uses only valid states and messages; thus a valid
trace is a sequence of valid transitions starting in an initial state.

#### Equivocation.

In the literature concerning fault-tolerance in distributed systems,
equivocation models the fact that certain agents can claim to be in different
states to different parties. VLSMs allow modeling such behavior, by specifying
that in a valid trace the valid input messages can be produced on different
(though still valid) traces.

#### Composition.

A single VLSM can represent the local point of view of a component in a
distributed system. We can obtain the global point of view by composing
multiple VLSMs and lifting the local validity constraint of each component.
Designers of systems can impose additional restrictions, which are stronger
than the ones that can be specified locally on individual components because
they can be stated in terms of the global composite state. We capture this
phenomenon by the notion of composition constraint.

######  Definition 2 (Composition).

Let $\\{\mathcal{V}_{i}\\}_{i=1}^{n}$ be an indexed set of VLSMs over the same
set of messages $M$. The constrained composition under a composition
constraint $\varphi$ is the VLSM $\mathcal{V}=\
\Bigr{(}{\sum_{i=1}^{n}}\mathcal{V}_{i}\Bigr{)}\Bigr{|}_{\varphi}=(L,S,S_{0},M,M_{0},\tau,\mathit{\beta}\wedge\varphi)$
where $L$ is the disjoint union of labels, the (initial) states are the
product of (initial) states of the components, the transition function $\tau$
and the constraint predicate $\mathit{\beta}$ are defined component-wise,
while the composition constraint $\varphi\subseteq L\times S\times M?$ is an
additional predicate that filters the inputs for the transition function.

When a composition constraint is trivial, i.e., it is the set $L\times S\times
M?$, we refer to the composition as the free composition and drop the
subscript $\varphi$ in the notation.

#### No Equivocation constraint.

As mentioned above, VLSMs implicitly allow equivocation. Nevertheless, a
truthful behavior of the agents in a composition can still be enforced by
means of a no equivocation constraint, which does not allow receiving in a
(composite) state a message from a component if that component could not have
emitted the message in a trace leading to the current state.

##  4 Asynchronous Muddy Children Puzzle as a VLSM — take 1

We would like to model the Muddy Children Puzzle as a collective effort of a
group of agents (the children) to reach a common goal (knowing whether they
are muddy or not) by exchanging messages which reveal as little as possible of
their personal (initial) knowledge about the problem (a.k.a., which children
they see as muddy). To this aim, there are several characteristics which will
be common to both our presented models:

  * •

Each child needs to know (at all times) which of the other children are muddy
(the child’s initial knowledge);

  * •

Every message needs to have a sender;

  * •

Every message has to report on the epistemic status of its sender at the time
the message was sent;

  * •

Decisions are final: once a child has decided upon their own status
(clean/muddy), they will not receive additional messages, as these would not
bring new knowledge.

In our models we choose to index the children with natural numbers and to
represent a child’s initial knowledge as a set of indices of the muddy
children they see (note that the index of the child cannot appear in this
set). We will also use these indices to identify the sender of a message. For
the epistemic status, we will use three possible values:

  * •

$u$ stands for “child doesn’t known their status”;

  * •

$m$ stands for “child knows they have mud on their forehead”;

  * •

$c$ stands for “child knows they don’t have mud on their forehead”.

For our first modeling attempt, we let the children maintain and communicate a
number reflecting “the round number” (from the original solution) at which
they perceive themselves to be.

Let us start formalizing this setting using VLSMs. We represent each child as
a VLSM of the form
$\mathcal{C}_{i}=(L_{i},S_{i},S_{0,i},M,M_{0,i},\tau_{i},\mathit{\beta}_{i})$.
The states of $\mathcal{C}_{i}$ are either initial states of the form
$\langle\mathit{Obs}\rangle$ where $\mathit{Obs}$ represents the children seen
as muddy by child $i$, or running states of the form
$\langle\mathit{Obs},r,\mathit{status}\rangle$, where additionally $r$ is the
round perceived by child $i$, and $\mathit{status}$ represents the epistemic
status of child $i$.

  * •

$L_{i}=\\{\mathit{init},\mathit{emit},\mathit{receive}\\}$ reflects the three
types of transitions (initialization, corresponding to the father’s
announcement and emitting/receiving messages)

  * •

$M_{i}=\\{\langle j,\,r,\,\mathit{status}\rangle\mid
j\in\\{1,\ldots,n\\},\;r\in\mathbb{N},\;\mathit{status}\in\\{u,m,c\\}\\}$ —
messages also communicate the round number

  * •

$M_{0,i}=\emptyset$

  * •

$S_{i}=\\{\langle\mathit{Obs}\rangle\ |\ \mathit{Obs}\subseteq\\{1,\hbox
to10.00002pt{.\hss.\hss.},n\\}\\}\cup\\{\langle\mathit{Obs},\,s,\,r\rangle\ |\
\mathit{Obs}\subseteq\\{1,\hbox to10.00002pt{.\hss.\hss.},n\\},\
s\in\\{u,m,c\\},\ r\in\mathbb{N}\\}$

  * •

$S_{0,i}=\\{\langle\mathit{Obs}\rangle\ |\ \mathit{Obs}\subseteq\\{1,\hbox
to10.00002pt{.\hss.\hss.},n\\}\\}$,

The invariant we would like to maintain is that a child at round $r$ knows
(from the messages exchanged with its peers) that there are more than $r$
muddy children.

Assuming that such an invariant holds for all accessible states, then when a
child (say $i$) sends a message containing their round number (say $k$) and
the fact that they still cannot determine their status, a child receiving such
a message (say $j$) can derive from it that $i$ knows that there are more than
$k$ muddy children except themselves (since otherwise $i$ would know their
status). Moreover, since the receiving child knows whether the sender is muddy
or not, if $j$ sees $i$ as muddy, $j$ can infer that there are actually more
than $k+1$ muddy children. If the current round of $j$ is smaller than the
number inferred (either $k$, if $i$ is clean, or $k+1$, if $i$ is muddy), then
$j$ can update their current round to that number.

If that happened, say $r$ is the new current round number, if $r$ is less than
the number of muddy children that $j$ sees, then the information provided by
$r$ is not yet useful enough to draw a conclusion about the status, so the
status will stay unknown. However, if $r$ ever becomes equal to the number of
muddy children that $j$ sees, then the child knows that there are more than
$r$ muddy children, and since they can only see $r$ muddy children, they will
conclude they have to be muddy.

An interesting fact holds for clean children. Note first that they see all the
children who are muddy (say $N$), so for them the number of muddy children
they see is larger by $1$ than the number of muddy children seen by any muddy
child. Hence, they cannot infer their status using the reasoning above,
because for that they would have to receive a message from a muddy child, say
$i$ with an unknown status at round $N-1$, but that is precisely the number of
muddy children that child $i$ sees, so at that round child $i$ would already
be able to infer their status. Let’s assume a child $i$ is clean. If there are
enough muddy children, $i$ can receive a message from a muddy child with round
$N-2$, and update their round to $N-1$ (using the reasoning above) while
maintaining their status as unknown (since the child still sees more muddy
children). Note that $N-1$ is its maximal round according to the invariant
proposed above. But, at the same time, one of the other muddy children, say
$j$ can receive the same message and update their round to $N-1$, which
coincides to the number of muddy children they see, so they would change their
status to knowing that they are muddy. Now if $j$ sends a message with their
new round and status and $i$ receives it, then $i$ would know they must be
clean, but the question is: what would happen with the child’s round? If $i$
keeps the same round (as to not violate the invariant), then they would have
two statuses at the same round. To avoid that, we decide to break the
invariant in this case and let a clean child advance to round $N$ when they
infer they are clean, thus staying in sync with the traditional solution to
the puzzle.

Thus we can rephrase the first invariant as: ”a message $\langle
j,\,r,\,\mathit{status}\rangle$ with status different than clean guarantees
that $j$ knows that there are more than $r$ muddy children”, and add a second
property, saying that a message $\langle j,\,r,\,\mathit{status}\rangle$ with
status different than unknown guarantees that $j$ sees precisely $r$ muddy
children.

In the sequel, we propose a transition function (and constraint predicate) to
help us realize the proposal above.

$\displaystyle\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$
$\displaystyle=\begin{aligned}
(\langle\mathit{Obs},r,\mathit{status}\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}\in\\{m,c\\}\\\
(\langle\mathit{Obs},r^{\prime},c\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=c\\\ &\quad\text{and
}j\notin\mathit{Obs}\text{ and }r^{\prime}=|\mathit{Obs}|\\\
(\langle\mathit{Obs},r^{\prime}-1,m\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=c\\\ &\quad\text{and
}j\notin\mathit{Obs}\text{ and }r^{\prime}=|\mathit{Obs}|+1\\\
(\langle\mathit{Obs},r^{\prime},m\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=m\\\ &\quad\text{and
}j\in\mathit{Obs}\text{ and }r^{\prime}=|\mathit{Obs}|\\\
(\langle\mathit{Obs},r^{\prime}+1,c\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=m\\\ &\quad\text{and
}j\in\mathit{Obs}\text{ and }r^{\prime}=|\mathit{Obs}|-1\\\
(\langle\mathit{Obs},r,\mathit{status}\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=u\\\ &\quad\text{and
}j\in\mathit{Obs}\text{ and }r^{\prime}<r\\\
(\langle\mathit{Obs},r^{\prime}+1,\mathit{status}\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=u\\\ &\quad\text{and
}j\in\mathit{Obs}\text{ and }r\leq r^{\prime}<|\mathit{Obs}|-1\\\
(\langle\mathit{Obs},r^{\prime}+1,m\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=u\\\ &\quad\text{and
}j\in\mathit{Obs}\text{ and }r^{\prime}=|\mathit{Obs}|-1\\\
(\langle\mathit{Obs},r,\mathit{status}\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=u\\\ &\quad\text{and
}j\notin\mathit{Obs}\text{ and }r^{\prime}\leq r\\\
(\langle\mathit{Obs},r^{\prime},\mathit{status}\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=u\\\ &\quad\text{and
}j\notin\mathit{Obs}\text{ and }r<r^{\prime}<|\mathit{Obs}|\\\
(\langle\mathit{Obs},r^{\prime},m\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{if
}\mathit{status}=u\text{ and }\mathit{status}^{\prime}=u\\\ &\quad\text{and
}j\notin\mathit{Obs}\text{ and }r^{\prime}=|\mathit{Obs}|\\\
\langle\mathit{Obs},r,\mathit{status}\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\quad\text{for the
cases not treated above}\end{aligned}$ Figure 1: The transition function for
the $\mathit{receive}$ label

Init

From the initial state, each child takes one (silent) transition, analyzing
their current knowledge and initializing the dynamic part of the state
accordingly.

  * •

The round number is initialized with 0

  * •

If the set of muddy children the child sees is empty, then the knowledge flag
is set to muddy (since at least one must be muddy); otherwise to unknown

$\tau_{i}(\mathit{init},\langle\mathit{Obs}\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})=(\langle\mathit{Obs},0,u\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$, if
$\mathit{Obs}\neq\emptyset$
$\tau_{i}(\mathit{init},\langle\mathit{Obs}\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})=(\langle\mathit{Obs},0,m\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$, if
$\mathit{Obs}=\emptyset$
$\beta_{i}(\mathit{init},\langle\mathit{Obs}\rangle,m)=(m=\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

Emit

From any non-initial state, a child can emit a message consisting of their
identifier, current round number and epistemic status, without changing state.

$\tau_{i}(\mathit{emit},\langle\mathit{Obs},r,\mathit{status}\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})=(\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
i,\,r,\,\mathit{status}\rangle)$
$\beta_{i}(\mathit{emit},\langle\mathit{Obs},r,\mathit{status}\rangle,m)=(m=\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

Receive

To update their state, whenever receiving a message $\langle
j,r^{\prime},\mathit{status}^{\prime}\rangle$ in a state
$\langle\mathit{Obs},r,\mathit{status}\rangle$, the child does the following:

  * •

If their current $\mathit{status}$ is not $u$, they ignore the message
(decisions are final).

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r,\mathit{status}\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$, if
$\mathit{status}\in\\{m,c\\}$

  * •

Otherwise:

    * –

If message status ($\mathit{status}^{\prime}$) is $c$, and $j$ is not known to
be muddy ($j\not\in\mathit{Obs}$), then from the property above $r^{\prime}$
must represent the actual number of muddy children. Hence:

      * *

If $r^{\prime}=|\mathit{Obs}|$, then child $i$ can update their round to the
received message’s round and then conclude that they are clean.

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r^{\prime},c\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

      * *

If $r^{\prime}=|\mathit{Obs}|+1$, then child $i$ can update their round to the
round before received message’s round and then conclude that they are muddy.

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r^{\prime}-1,m\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

    * –

If message status ($\mathit{status}^{\prime}$) is $m$ then it must be that $j$
is known as muddy ($j\in\mathit{Obs}$); then, from the property above,
$r^{\prime}+1$ must represent the actual number of muddy children. Hence:

      * *

If $r^{\prime}=|\mathit{Obs}|$, then child $i$ can update their round to the
received message’s round and then conclude that they are muddy.

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r^{\prime},m\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

      * *

If $r^{\prime}=|\mathit{Obs}|-1$, then child $i$ can update their round to
round after the received message’s round and then conclude that they are
clean.

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r^{\prime}+1,c\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

    * –

If message status ($\mathit{status}^{\prime}$) is $u$, and $j$ is known as
muddy ($j\in\mathit{Obs}$), then $i$ can infer that $j$ knows that there are
more than $r^{\prime}$ muddy children, and therefore infers that there are
more than $r^{\prime}+1$ muddy children. Hence:

      * *

If $r^{\prime}<r$, then child $i$ can ignore the message (it brings nothing
new).

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r,\mathit{status}\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

      * *

If $r\leq r^{\prime}<|\mathit{Obs}|-1$, then child $i$ can update their round
to $r^{\prime}+1$, but their status will remain unknown (they already know
there are at least $|\mathit{Obs}|$ muddy children).

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r^{\prime}+1,\mathit{status}\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

      * *

If $r^{\prime}=|\mathit{Obs}|-1$, then child $j$ sees at least
$|\mathit{Obs}|$ muddy children. Since the sender is known as muddy, there are
at least $|\mathit{Obs}|+1$ muddy children. On the other hand, child $i$ knows
there are at most $|\mathit{Obs}|+1$ muddy children. Combining the two
inequalities, we get that there are precisely $|\mathit{Obs}|+1$ muddy
children, so child $i$ can advance to round $r^{\prime}+1$ and knows they are
muddy.
$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r^{\prime}+1,m\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

    * –

If message status ($\mathit{status}^{\prime}$) is unknown, and $j$ is not
known as muddy ($j\notin\mathit{Obs}$), then $i$ can infer that $j$ knows that
there are more than $r^{\prime}$ muddy children, and therefore infers (only)
that there are more than $r^{\prime}$ muddy children. Hence:

      * *

If $r^{\prime}\leq r$, then child $i$ can ignore the message.

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r,\mathit{status}\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

      * *

If $r<r^{\prime}<|\mathit{Obs}|$, then child $i$ can update its round to
$r^{\prime}$, but its status will remain unknown (it already knows there are
at least $|\mathit{Obs}|$ muddy children).

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r^{\prime},\mathit{status}\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

      * *

If $r^{\prime}=|\mathit{Obs}|$, we reason analogous to the similar above case:
child $j$ knows that there are at least $|\mathit{Obs}|+1$ muddy children and.
Adding the fact that child $i$ knows there are at most $|\mathit{Obs}|+1$
muddy children, we get that there are precisely $|\mathit{Obs}|+1$ muddy
children, so child $i$ knows they are muddy.

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},r,\mathit{status}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$ =
$(\langle\mathit{Obs},r^{\prime},m\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

#### Composition.

Note that the notion of VLSM composition in general allows arbitrary initial
states for the components. However, in this setting, we need to ensure that
the sets of children known by each child to be muddy are consistent. Formally,
given a child-state $s$, let $\mathit{Obs}(s)$ be the observation-set
associated to $s$. Then, for any composite state
$\sigma=\langle\sigma_{1},\ldots,\sigma_{n}\rangle$, let
$\mathbf{consistent}(\sigma)$ be the predicate defined by

  * •

$M\neq\emptyset$ (there should be at least one muddy child)

  * •

$\mathit{Obs}(\sigma_{i})=M\setminus\\{i\\}$, for any $i$ (each child sees all
other muddy children)

where $M=\bigcup_{i=1}^{n}{\mathit{Obs}(\sigma_{i})}$.

Finally, the game flow can be formalized as a constrained VLSM composition.

$\mathcal{M}uddy\mathcal{P}uzzle=\Bigr{(}\mathcal{C}_{1}+\ldots+\mathcal{C}_{n}\Bigr{)}\Bigr{|}_{\varphi}$

where $\varphi$ specifies the following composition constraint:

init

At the first transition from an initial state we check that the observation
sets corresponding to each component are consistent

$\varphi((i,\mathit{init}),(\langle\mathit{Obs}_{1}\rangle,\ldots,\langle\mathit{Obs}_{n}\rangle),m)=\mathbf{consistent}(\langle\mathit{Obs}_{1}\rangle,\ldots,\langle\mathit{Obs}_{n}\rangle)$

receive

We must enforce a no-equivocation constraint to ensure the truthfulness of the
participants

$\varphi(\langle
i,\mathit{receive}\rangle,\langle\sigma_{1},\ldots,\sigma_{n}\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)=({\it\mathit{status}}^{\prime}=\mathit{status}_{j}\wedge
r^{\prime}=r_{j})\vee(\mathit{status}^{\prime}=u\wedge r^{\prime}<r_{j})$,
where $\sigma_{j}=\langle\mathit{Obs},r_{j},\mathit{status}_{j}\rangle$.

###  4.1 Correctness of the protocol

In the following, we give a justification of the fact that the above described
protocol is correct in the sense that it converges to a solution. The valid
states of the protocol ($S_{V}$) correspond to the composite states which are
VLSM-valid in the constrained composition described above. We define the set
of non-initial valid states $S_{V}^{\ast}=S_{V}\setminus S_{0}$ and the set of
final states $S_{F}=\\{\langle\sigma_{i}\ldots\sigma_{n}\rangle\in
S_{V}\mid\forall i\in\\{1,\ldots,n\\},\mathit{status}(\sigma_{i})\neq u\\}$.

It can be easily checked that the consistency predicate holds for any
$\sigma\in S_{V}^{*}$:

######  Remark 1.

For each $\sigma\in S_{V}^{*}$, $\mathbf{consistent}(\sigma)$ holds.

Another VLSM-related property, which we state without proof is the fact that
the constraint for $\mathit{receive}$ transitions is indeed a no-equivocation
constraint:

######  Remark 2 (No Equivocation).

For any valid trace $tr$ leading from an initial state $\sigma_{0}$ to a state
$\sigma\in S_{v}^{\ast}$ and for any input message $m$ which is valid for
$\sigma$ there exists a valid trace starting in $\sigma_{0}$, of length less
than that of $tr$ which emits $m$.

Let us now show that the invariant that we stated about the dynamics of the
protocol is indeed preserved during a (valid) protocol run.

######  Lemma 1 (Invariant Preservation).

For any $\sigma\in S_{V}$, if $\sigma\not\in S_{0}$, then:

For any component $i$ of $\sigma$ of the form
$\sigma_{i}=\langle\mathit{Obs}_{i},r_{i},\mathit{status}_{i}\rangle$:

  * •

If $\mathit{status}_{i}=u$, then $r_{i}<|\mathit{Obs}_{i}|$ (and
$|\mathit{Obs}_{i}|\leq N$)

  * •

If $\mathit{status}_{i}=m$, then $r_{i}=N-1=|\mathit{Obs}_{i}|$

  * •

If $\mathit{status}_{i}=c$, then $r_{i}=N=|\mathit{Obs}_{i}|$

###### Proof.

Note that it is common knowledge that $|\mathit{Obs}_{i}|\leq
N\leq|\mathit{Obs}_{i}|+1$ for any $i$.

We prove the invariant by induction on the length of a valid trace leading to
$\sigma$. The property trivially holds for $\sigma\in S_{0}$. For the
induction case, we consider the final (valid) transition leading to $\sigma$,
say $\sigma^{\prime}\xrightarrow[\ m\ \rightarrow\ m^{\prime}\
]{(i,l)}\sigma$, and we assume that the invariant holds for $\sigma^{\prime}$.
We proceed by case analysis on the label of the transition.

$l=\mathit{init}$:

This transition obviously preserves the invariant, because of the father’s
statement.

$l=\mathit{emit}$:

In case of a $\mathit{emit}$ transition, the conclusion is also immediate,
since the state remains unchanged.

$l=\mathit{receive}$:

From Remark 2 there is a composite valid state from which the input message
can be emitted which has the same observation sets as $\sigma^{\prime}$ (since
they both are reachable from the same initial state) and for which we can
apply the induction hypothesis and thus assume that the invariant holds.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,m\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$: the message is ignored and
the state remains unchanged, so the conclusion is immediate.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,c\rangle,\langle
j,\,r^{\prime},\,\mathit{status}^{\prime}\rangle)$: we proceed analogous to
the previous case.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,c\rangle)$ and $j\notin\mathit{Obs}_{i}$ and
$r^{\prime}=|\mathit{Obs}_{i}|$:
By applying the induction hypothesis to the state from which the message is
obtained, we have $r^{\prime}=N=|\mathit{Obs}_{j}|$.
The resulting state $\langle\mathit{Obs}_{i},r^{\prime},c\rangle$ preserves
the invariant, because $r^{\prime}=N=|\mathit{Obs}_{i}|$.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,c\rangle)$ and $j\notin\mathit{Obs}_{i}$ and
$r^{\prime}=|\mathit{Obs}_{i}|+1$:
By applying the induction hypothesis to the state from which the message is
obtained, we have $r^{\prime}=N=|\mathit{Obs}_{j}|$.
The resulting state $\langle\mathit{Obs}_{i},r^{\prime}-1,m\rangle$ preserves
the invariant, because $r^{\prime}-1=N-1=|\mathit{Obs}_{i}|$.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,m\rangle)$ and $j\in\mathit{Obs}_{i}$ and
$r^{\prime}=|\mathit{Obs}_{i}|$:
By applying the induction hypothesis to the state from which the message is
obtained, we have $r^{\prime}=N-1=|\mathit{Obs}_{j}|$.
The resulting state $\langle\mathit{Obs}_{i},r^{\prime},m\rangle$ preserves
the invariant, because $r^{\prime}=N-1=|\mathit{Obs}_{i}|$.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,m\rangle)$ and $j\in\mathit{Obs}_{i}$ and
$r^{\prime}=|\mathit{Obs}_{i}|-1$:
By applying the induction hypothesis to the state from which the message is
obtained, we have $r^{\prime}=N-1=|\mathit{Obs}_{j}|$.
The resulting state $\langle\mathit{Obs}_{i},r^{\prime}+1,c\rangle$ preserves
the invariant, because $r^{\prime}+1=N=|\mathit{Obs}_{i}|$.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,u\rangle)$ and $j\in\mathit{Obs}_{i}$ and $r^{\prime}<r$:
The state after applying the transition remains unchanged, so the conclusion
is immediate.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,u\rangle)$ and $j\in\mathit{Obs}_{i}$ and $r\leq
r^{\prime}<|\mathit{Obs}_{i}|-1$:
The resulting state $\langle\mathit{Obs}_{i},r^{\prime}+1,u\rangle$ obviously
preserves the invariant, since $r^{\prime}+1<|\mathit{Obs}_{i}|$.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,u\rangle)$ and $j\in\mathit{Obs}_{i}$ and
$r^{\prime}=|\mathit{Obs}_{i}|-1$:
We have $r^{\prime}+1=|\mathit{Obs}_{i}|\geq N-1$, so $r^{\prime}\geq N-2$.
On the other hand, applying the induction hypothesis, we have that
$r^{\prime}<|\mathit{Obs}_{j}|$ and since child $j$ is muddy,
$|\mathit{Obs}_{j}|=N-1$, and combining these we get
$r^{\prime}<|\mathit{Obs}_{j}|=N-1$, which implies $r^{\prime}\leq N-2$.
We can conclude that $r^{\prime}=N-2$, so the resulting state
$\langle\mathit{Obs}_{i},r^{\prime}+1,m\rangle$ preserves the invariant,
because $r^{\prime}+1=|\mathit{Obs}_{i}|=N-1$.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,u\rangle)$ and $j\notin\mathit{Obs}_{i}$ and $r^{\prime}<=r$:
The state after applying the transition remains unchanged, so the conclusion
is immediate.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,u\rangle)$ and $j\notin\mathit{Obs}$ and
$r<r^{\prime}<|\mathit{Obs}_{i}|$:
The resulting state
$\langle\mathit{Obs}_{i},r^{\prime},\mathit{status}\rangle$ preserves the
invariant, since $r^{\prime}<|\mathit{Obs}_{i}|$.

  * •

$\tau_{i}(\mathit{receive},\langle\mathit{Obs}_{i},r,u\rangle,\langle
j,\,r^{\prime},\,u\rangle)$ and $j\notin\mathit{Obs}_{i}$ and
$r^{\prime}=|\mathit{Obs}_{i}|$:
By applying the induction hypothesis to the state from which the message is
obtained, we have $r^{\prime}<|\mathit{Obs}_{j}|$ and since child $j$ is
clean, $|\mathit{Obs}_{j}|=N$ so we get $r^{\prime}<N$ and combining this with
the last condition in the transition, we immediately obtain that
$|\mathit{Obs}_{i}|<N$.
But since it is common knowledge that $|\mathit{Obs}_{i}|\geq N-1$ it must be
that $|\mathit{Obs}_{i}|=N-1$. We can conclude that
$r^{\prime}=|\mathit{Obs}_{i}|=N-1$, so the resulting state
$\langle\mathit{Obs}_{i},r^{\prime},m\rangle$ preserves the invariant.

  * •

For all the cases not treated above, the child’s $\beta$ predicate does not
hold, so there cannot be any transition.

∎

######  Theorem 1.

From any initial consistent state, there is a path leading to a final state in
which each child’s status is consistent with the instance of the problem.

###### Proof sketch.

The result can be obtained from the following properties:

Progress

From any valid non-final state $\sigma$, there is a valid transition leading
to a state $\sigma^{\prime}$ on some component $i$, such that
$round(\sigma^{\prime}_{i})>round(\sigma_{i})$, where we let
$round(\langle\mathit{Obs}\rangle)$ be $-1$.

If there are any component initial states left, we advance one of them. If
there are any children which already know their status, we advance to the
final state any of the others (there must be at least one child with unknown
status since the state is not final). If no child knows their status yet, then
there must be at least two muddy children. Then take the one among them with
minimum round number (if their round numbers are equal, take any of them) and
receive the message corresponding to the current state of the other. This will
surely increase their current round number.

Invariant Preservation

The invariant from Lemma 1 holds.

In particular, if a final state is reached, each child’s status will be
consistent with the current instance of the problem.

Termination

No child can increase their round number past the number of muddy children
they see.

Easy to prove by induction and analysis on the cases of the transition
function.

∎

###  4.2 Possible optimization

If we analyze the dynamics of the solution proposed above, we notice that the
only relevant exchange of messages happens in the final stages of the
protocol. Indeed, assuming a child sees $n$ muddy children, they know that any
other child sees at least $n-1$ muddy children; therefore no message it would
send with round less than $n-1$ can help any other child determine their
status. Hence, the child can ”jump” during the initialization phase directly
to the round $n-1$. Formally, we add a new label jump and replace the Init
transition with the following:

> From any state with status unknown, a child can take one (silent) transition
> ”jumping” to a future state it knows it can reach based on existing
> knowledge, where the round number becomes the number preceding the number of
> muddy children the child sees and the child’s knowledge flag remains
> unknown.
>
>
> $\tau_{i}(\mathit{jump},\langle\mathit{Obs},r,\mathit{status}\rangle,m)=(\langle\mathit{Obs},|\mathit{Obs}|-1,u\rangle,\leavevmode\hbox
> to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
> 2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
> }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
> }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
> }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
> to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
> {{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
> }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
> }{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
> } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
> {}{}\pgfsys@beginscope\pgfsys@invoke{
> }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
> }{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
> } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
> {}{}\pgfsys@beginscope\pgfsys@invoke{
> }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
> }{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
> } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
> \pgfsys@invoke{\lxSVG@closescope
> }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
> }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$
>
> $\beta_{i}(\mathit{jump},\langle\mathit{Obs},r,\mathit{status}\rangle,m)=(\mathit{status}=u)\wedge(m=\leavevmode\hbox
> to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
> 2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
> }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
> }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
> }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
> to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
> {{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
> }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
> }{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
> } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
> {}{}\pgfsys@beginscope\pgfsys@invoke{
> }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
> }{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
> } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
> {}{}\pgfsys@beginscope\pgfsys@invoke{
> }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
> }{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
> } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
> \pgfsys@invoke{\lxSVG@closescope
> }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
> }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})\wedge(r<|\mathit{Obs}|-1)$

After such a jump one can find a very short path to a solution:

  1. 1.

a child sends a message after the jump with the unknown status

  2. 2.

another (muddy) child receives that message and discovers they are muddy and
sends a message with this discovery

  3. 3.

all other children (including the first) receive this second message and
discover their status

###  4.3 Discussion

The above proposed solution seems to satisfy our initial guidelines for a good
asynchronous solution. Nevertheless, it is far from being perfect, as
illustrated by the following example.

######  Example 1 (Information leak).

Assume there are $5$ children, $4$ of whom are muddy and one is not. Then a
muddy child (say, child $1$) can discover that they are muddy by only
exchanging messages with the clean child (say, child $5$) with the following
scenario:

  1. 1.

$1$ at round $0$ sends message $m^{1}_{0}$ that they do not know

  2. 2.

$5$ at round $0$ receives message $m^{1}_{0}$, advances to round $1$, and
sends message $m^{5}_{1}$ that they do not know

  3. 3.

$1$ at round $0$ receives the message $m^{5}_{1}$, advances to round $1$, and
sends message $m^{1}_{1}$ that they do not know

  4. 4.

$5$ at round $1$ receives message $m^{1}_{1}$, advances to round $2$, and
sends message $m^{5}_{2}$ that they do not know

  5. 5.

$1$ at round $1$ receives the message $m^{5}_{2}$, advances to round $2$, and
sends message $m^{1}_{2}$ that they do not know

  6. 6.

$5$ at round $2$ receives message $m^{1}_{2}$, advances to round $3$, and
sends message $m^{5}_{3}$ that they do not know

  7. 7.

$1$ at round $2$ receives the message $m^{5}_{3}$, advances to round $3$ which
equals the number of muddy children they see and changes their status to
knowing they are muddy (and sends message $m^{1}_{3}$ with status muddy)

Moreover, once $1$ knows they are muddy and sends a message about it, upon
receiving that message all the other children will know their status.

There are at least two issues about the above example: (1) that a muddy child
needs no information from other muddy children to discover that they are
muddy; and (2) that once a child knows their status, all other children
immediately know their status, even if they have not taken part in the
conversation so far.

It thus seems that, although sharing the perceived round as part of the
message helps with making the discovery process asynchronous, it also alters
it more than expected in terms of what becomes inferable during an exchange of
information. The following section proposes a solution we believe to be closer
to the original formulation and intended dynamics, while staying asynchronous.

##  5 Solving the puzzle by extracting information from messages

To alleviate the issues identified with the solution in Section 4, we propose
a new solution, which follows more closely an epistemic logic point of view,
in the sense that the messages exchanged between children only carry
information that the child has previously seen. This guarantees that deduction
can only be done according to information that is (was) publicly available.

To do that, we define the child $i$ as the following VLSM, resembling the
previous encoding, but using message histories (lists of messages previously
received) instead of round numbers:

  * •

$L_{i}=\\{\mathit{init},\mathit{emit},\mathit{receive}\\}$

  * •

$M=\\{\langle j,\,s,\,h\rangle\ |\ j\in\\{1,\hbox
to10.00002pt{.\hss.\hss.},n\\},\ s\in\\{u,m,c\\},\ h\in M^{*}\\}$

  * •

$M_{0,i}=\emptyset$

  * •

$S_{i}=\\{\langle\mathit{Obs}\rangle\ |\ \mathit{Obs}\subseteq\\{1,\hbox
to10.00002pt{.\hss.\hss.},n\\}\\}\cup\\{\langle\mathit{Obs},\,s,\,h\rangle\ |\
\mathit{Obs}\subseteq\\{1,\hbox to10.00002pt{.\hss.\hss.},n\\},\
s\in\\{u,m,c\\},\ h\in M^{*}\\}$

  * •

$S_{0,i}=\\{\langle\mathit{Obs}\rangle\ |\ \mathit{Obs}\subseteq\\{1,\hbox
to10.00002pt{.\hss.\hss.},n\\}\\}$,

Let us now describe the dynamics of a child’s interaction with the others.

Init

The initialization phase will remain basically the same as for the previous
solution, except that, instead of round $0$, now the children will have the
empty history:

$\tau_{i}(\mathit{init},\langle\mathit{Obs}\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})=\left\\{\begin{array}[]{rl}(\langle\mathit{Obs},\,u,\,[]\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\mbox{ if
}\mathit{Obs}\neq\emptyset\\\
(\langle\mathit{Obs},\,m,\,[]\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\mbox{ if
}\mathit{Obs}=\emptyset\\\ \end{array}\right.$
$\beta_{i}(\mathit{init},\langle\mathit{Obs}\rangle,\mathit{msg})=(\mathit{msg}=\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

Emit

Similarly, the emit phase is basically the same, except that, instead of
sending their round number, the children will now send their current history:

$\tau_{i}(\mathit{emit},\langle\mathit{Obs},\,s,\,h\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})=(\langle\mathit{Obs},s,h\rangle,\
\langle i,\,s,\,h\rangle)$
$\beta_{i}(\mathit{emit},\langle\mathit{Obs},\,s,\,h\rangle,\mathit{msg})=(\mathit{msg}=\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$

Receive

Upon receiving a message (in a not yet known status) the child will aggregate
the message received with the information they already had (append it to its
history) and compute its new status based on its $\mathit{Obs}$ervation set
and its new history.

$\tau_{i}(\mathit{receive},\langle\mathit{Obs},\,s,\,h\rangle,\langle
j,\,s_{j},\,h_{j}\rangle)=$

$\left\\{\begin{array}[]{rl}(\langle\mathit{Obs},\,s,\,h\rangle,\leavevmode\hbox
to5.24pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
2.47626pt\lower-0.76909pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\mbox{ if
}s\in\\{c,m\\}\\\
(\langle\mathit{Obs},\,\mathit{compute}(\mathit{Obs},h\,++\,[\langle
j,s_{j},h_{j}\rangle]),\,h\,++\,[\langle
j,\,s_{j},\,h_{j}\rangle]\rangle,\leavevmode\hbox to5.24pt{\vbox
to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 2.47626pt\lower-0.76909pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{1.5pt}{1.70717pt}\pgfsys@curveto{1.5pt}{2.5356pt}{0.82843pt}{3.20717pt}{0.0pt}{3.20717pt}\pgfsys@curveto{-0.82843pt}{3.20717pt}{-1.5pt}{2.5356pt}{-1.5pt}{1.70717pt}\pgfsys@curveto{-1.5pt}{0.87874pt}{-0.82843pt}{0.20717pt}{0.0pt}{0.20717pt}\pgfsys@curveto{0.82843pt}{0.20717pt}{1.5pt}{0.87874pt}{1.5pt}{1.70717pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{1.70717pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{3.98343pt}\pgfsys@lineto{2.56064pt}{-0.56909pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-2.27626pt}{-0.56909pt}\pgfsys@lineto{2.56064pt}{3.98343pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}),&\mbox{ if }s=u\\\
\end{array}\right.$

// we compute the new status
$\mathit{compute}(\mathit{Obs},h)=\left\\{\begin{array}[]{rl}m,&\mbox{ if
}\min_{k\in\mathit{Obs}}|\mathit{groupSimilar}_{i}(\mathit{unknown}_{k}(\mathit{flatten}(h)))|\geq|\mathit{Obs}|\\\
c,&\mbox{ if the first rule didn't apply and
}|\mathit{muddy}(\mathit{flatten}(h))|=|\mathit{Obs}|\\\ u,&\mbox{
otherwise}\end{array}\right.$

// we unfold all the messages contained (in depth) in the history
$\mathit{flatten}(h\,++\,[\langle
j,\,s_{j},\,h_{j}\rangle])=\mathit{flatten}(h)\ \cup\ \mathit{flatten}(h_{j})\
\cup\ \\{\langle j,\,s_{j},\,h_{j}\rangle\\}\ \cup\ \mathit{extra}(\langle
j,\,s_{j},\,h_{j}\rangle)$

// we extract extra information from a message about messages which could have
been emitted by its sender (e.g. in all prefixes of the history in which the
sender didn’t know their status)
$\mathit{extra}(\langle j,\,s_{j},\,h_{j}\rangle)=\\{\langle
j,u,h_{j}^{\prime}\rangle\ |\ h_{j}^{\prime}\ \triangleleft\ h_{j}\\}$222We
denote by $h_{1}\triangleleft h_{2}$ the fact that $h_{1}$ is a strict prefix
of $h_{2}$.

// we select messages belonging to a given child and having an unknown status
$\mathit{unknown}_{k}(h)=\\{m\mid m\in h\wedge m=\langle
k,u,h^{\prime}\rangle\mbox{ for some h'}\\}$

// we group messages that carry the same information relative to child $i$
$\mathit{groupSimilar}_{i}(h)=h\setminus\\{\langle j,\ u,\
h^{\prime}\,++\,[\langle i,\\_,\\_\rangle]\rangle\mbox{ for some h'}\\}$

// we construct the set of all children who know they are muddy in a history
$\mathit{muddy}(h)=\\{j\mid\langle j,m,h_{j}\rangle\in h\\}$

Finally, the game can be formalized as a constrained VLSM composition.

$\mathcal{M}uddy\mathcal{P}uzzle=\Bigr{(}\mathcal{C}_{1}+\mathcal{C}_{2}+\mathcal{C}_{3}\Bigr{)}\Bigr{|}_{\varphi}$

where

// consistency
$\varphi((i,\mathit{init}),(\langle\mathit{Obs}_{1}\rangle,\langle\mathit{Obs}_{2}\rangle,\langle\mathit{Obs}_{3}\rangle),m)=\mathbf{consistent}(\langle\mathit{Obs}_{1}\rangle,\langle\mathit{Obs}_{2}\rangle,\langle\mathit{Obs}_{3}\rangle)$,

// no equivocation
$\varphi((i,\mathit{receive}),\langle\sigma_{1},\sigma_{2},\sigma_{3}\rangle,\langle
j,s_{j},h_{j}\rangle)=$

$(s_{j}=\mathit{status}(\sigma_{j})\ \wedge\
h_{j}=\mathit{history}(\sigma_{j}))\ \vee\ (s_{j}=u\ \wedge\
h_{j}\triangleleft\ \mathit{history}(\sigma_{j})),$

where for a state $\sigma=\langle\mathit{Obs},s,h\rangle$, we define
$\mathit{status}(\sigma)=s$ and $\mathit{history}(\sigma)=h$.

It is relatively easy to see that the kind of reasoning described in the
(counter-)Example 1 is no longer possible, because after the first exchange of
messages, child $1$ cannot really infer anything, because all they see is a
message from child $5$ containing a message from themselves.

We argue that the information contained in a message represents the epistemic
knowledge of its sender about the status of the other children at the time the
message was sent, thus making this solution much closer to the standard
solution (using synchronous rounds and public announcements).

First, let $N$ be the total number of muddy children, and let us observe that
if a child knows $N$, then they also know their status (by comparing $N$ with
the number of muddy visible children). On the other hand, telling the others
that they know $N$ (without actually telling them the value) is no different
than telling them that their status can be inferred. Let $K_{1},\ldots,K_{n}$
be the epistemic operators assigned to each child, with the intuitive meaning
of $K_{i}\psi$ that $i$ can infer that $\psi$ holds, based on the commonly
available information, and on the private information that $i$ has. Let also
$q_{1},\ldots,q_{n}$ be primitive propositions, $q_{i}$ meaning that $i$ knows
the value of $N$.

Then, we can recursively encode a message $m$ as a formula $E(m)$, as follows:

$E(\langle
j,s_{j},h_{j}\rangle)=\left\\{\begin{array}[]{lc}(K_{j}\bigwedge_{m\in
h_{j}}E(m))\wedge K_{j}\left(\bigwedge_{m\in h_{j}}E(m)\rightarrow
q_{j}\right)&\mbox{ if }s_{j}\neq u\\\ (K_{j}\bigwedge_{m\in
h_{j}}E(m))\wedge\neg K_{j}\left(\bigwedge_{m\in h_{j}}E(m)\rightarrow
q_{j}\right)&\mbox{ if }s_{j}=u\\\ \end{array}\right.$

One important observation is that the formulas corresponding to all additional
messages introduced by flatten(h) are directly deducible from the formulas of
$h$.

#### Discussion.

Our preliminary exploration of the interactions possible within the model
seems to hint that a solution is reachable from any initial state for the case
of three children. Nevertheless, our current definition of groupSimilar was
engineered for the case of three children and we know it doesn’t scale to more
children as-is. We believe that for the general case it should be replaced by
factoring the messages through an equivalence relation grouping messages which
carry the similar amount of information as perceived by the child receiving
these messages.

##  6 Conclusion and Future Work

In this paper we have shown that compositions of VLSMs seem like a useful tool
to model the dynamics of distributed agents, allowing independent description
of their behavior, but also enabling the specification of global constraints
(e.g., truthfulness, fairness, etc.).

Regarding the models proposed for the Muddy Children Puzzle, for the first
model we were able to show that it achieves the goal of converging towards a
solution, but also showed that it might leak more information than intended
through communication. We believe the second model to be promising and more
faithful to our modeling goals and plan to further explore its possible
generalizations to an arbitrary number of children.

## References

  * [1]
  * [2] R. Fagin, J.Y. Halpern, Y. Moses & M. Vardi (2004): _Reasoning About Knowledge_.  A Bradford Book, MIT Press, 10.7551/mitpress/5803.001.0001.
  * [3] Pedro Fonseca, Kaiyuan Zhang, Xi Wang & Arvind Krishnamurthy (2017): _An Empirical Study on the Correctness of Formally Verified Distributed Systems_.  In: European Conference on Computer Systems, pp. 328–343, 10.1145/3064176.3064183.
  * [4] Jelle Gerbrandy & Willem Groeneveld (1997): _Reasoning about information change_.  Journal of logic, language and information 6, pp. 147–169, 10.1023/A:1008222603071.
  * [5] Nina Gierasimczuk & Jakub Szymanik (2011): _A note on a generalization of the muddy children puzzle_.  In: Proceedings of the 13th Conference on Theoretical Aspects of Rationality and Knowledge, pp. 257–264, 10.1145/2000378.2000409.
  * [6] Elaine Li, Traian Florin Șerbănuță, Denisa Diaconescu, Vlad Zamfir & Grigore Ro¸su (2020): _Formalizing Correct-By-Construction Casper in Coq_.  In: International Conference on Blockchain and Cryptocurrency, pp. 1–3, 10.1109/ICBC48266.2020.9169468.
  * [7] Minghui Ma, Alessandra Palmigiano & Mehrnoosh Sadrzadeh (2014): _Algebraic Semantics and Model Completeness for Intuitionistic Public Announcement Logic_.  Annals of Pure and Applied Logic 165(4), pp. 963–995, 10.1016/j.apal.2013.11.004.
  * [8] Daniel Miedema & Malvin Gattinger (2023): _Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic_.  arXiv preprint arXiv:2307.05067, 10.48550/arXiv.2307.05067.
  * [9] Hans Van Ditmarsch, Wiebe van Der Hoek & Barteld Kooi (2007): _Dynamic epistemic logic_.  337, Springer Science & Business Media, 10.1007/978-1-4020-5839-4.
  * [10] V. Zamfir, M. Calancea, D. Diaconescu, W. Kołowski, B. Moore, K. Palmskog, T.F. Șerbănuță, M. Stay, D. Trufaș & J. Tušil (2022): _Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems_.  arXiv:2202.12662v3, 10.48550/ARXIV.2202.12662.
  * [11] Vlad Zamfir, Nate Rush, Aditya Asgaonkar & Georgios Piliouras (2019): _Introducing the “Minimal CBC Casper” Family of Consensus Protocols_.  https://github.com/cbc-casper/cbc-casper-paper.