about $p$. Thus, it is defined by ${\Phi}^{\mathsf{gossip}}_{p,q} = \forall x\forall
  y.\bigl((\mathit{latest}_p(x,y) \wedge q(y)) \implies \bigvee_{a \in \Sigma}
  (a(x) \wedge a(y))\bigr) \in {\textup{FO}}^3[\le]$. For example, for ${P}=\{p_1,p_2,p_3\}$ and $\Sigma = \{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] circle (2.8pt);
\end{tikzpicture}
},{\resizebox{!}{1.4ex}{$\diamond$}}\}$, the MSC $M$ from Figure \[fig:msc\] is contained in ${\mathbb{L}}({\Phi}^{\mathsf{gossip}}_{p_1,p_3})$. In particular, $M,[x \mapsto e_5, y
  \mapsto g_5] \models \mathit{latest}_{p_1}(x,y)$ and $\lambda(e_5) =
  \lambda(g_5) = {
\begin{tikzpicture}
\filldraw[fill=white,draw=black] circle (2.8pt);
\end{tikzpicture}
}$.

Communicating Finite-State Machines
-----------------------------------

In a communicating finite-state machine, each process $p \in {P}$ can perform internal actions of the form ${\langlea\rangle}$, where $a \in \Sigma$, or send/receive messages from a finite set of messages ${\mathit{Msg}}$. A send action ${\langlea,!_{q}{m}\rangle}$ of process $p$ writes message ${m}\in {\mathit{Msg}}$ to channel $(p,q)$, and performs $a \in \Sigma$. A receive action ${\langlea,?_{q}{m}\rangle}$ reads message ${m}$ from channel $(q,p)$. Accordingly, we let ${\mathit{Act}_{p}({\mathit{Msg}})} {:=}\{{\langlea\rangle} \mid a \in \Sigma\} \cup
\{{\langlea,!_{q}{m}\rangle} \mid a \in \Sigma$, $m \in {\mathit{Msg}}$, $q \in {P}\setminus\{p\}\} \cup
\{{\langlea,?_{q}{m}\rangle} \mid a \in \Sigma$, $m \in {\mathit{Msg}}$, $q \in {P}\setminus\{p\}\}$ denote the set of possible actions of process $p$.

A *communicating finite-state machine (CFM)* over ${P}$ and $\Sigma$ is a tuple $(({\mathcal{A}}_p)_{p \in {P}},{\mathit{Msg}},{\mathit{Acc}})$ consisting of a 