An event that is neither a send nor a receive event is called *internal*. Moreover, for all $(p,q) \in {\mathit{Ch}}$ and $(e,f), (e',f') \in {{\lhd}} \cap (E_p
    \times E_q)$, we have $e {\leq_{\mathsf{proc}}}e'$ iff $f {\leq_{\mathsf{proc}}}f'$ (which guarantees a FIFO behavior).

We require that ${{\rightarrow}} \cup {{\lhd}}$ be acyclic (intuitively, messages cannot travel backwards in time). The associated partial order is denoted ${\le} {:=}({{\rightarrow}} \cup {{\lhd}})^*$ with strict part ${<}=({{\rightarrow}} \cup {{\lhd}})^+$. We do not distinguish isomorphic MSCs. Let ${\mathbb{MSC}({P},\Sigma)}$ denote the set of MSCs over ${P}$ and $\Sigma$.

Actually, MSCs are very similar to the space-time diagrams from Lamport’s seminal paper [@Lamport78], and $\le$ is commonly referred to as the *happened-before relation*.

It is worth noting that, when ${P}$ is a singleton, an MSC with events $e_1
\to e_2 \to \ldots \to e_n$ can be identified with the word $\lambda(e_1)\lambda(e_2) \ldots \lambda(e_n) \in \Sigma^\ast$.

= \[draw, fill=white, circle, inner sep=0, minimum size=0.25cm, draw=black\] = \[draw, fill=white, rectangle, inner sep=0, minimum size=0.2cm, draw=black\] = \[draw, fill=white, diamond, inner sep=0, minimum size=0.3cm\]

Consider the MSC from Figure \[fig:msc\] over ${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$}}\}$. We have, for instance, $E_{p_1} 