$M=(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ with nonempty finite set of nodes $E$, edge relations ${{\rightarrow}},{{\lhd}} \subseteq E \times E$, and node-labeling functions ${\mathit{loc}}\colon E \to {P}$ and $\lambda\colon E \to \Sigma$. An example MSC is depicted in Figure \[fig:msc\]. A node $e \in E$ is an *event* that is executed by process ${\mathit{loc}}(e) \in {P}$. In particular, $E_p {:=}\{e \in E \mid {\mathit{loc}}(e) = p\}$ is the set of events located on $p$. The label $\lambda(e) \in \Sigma$ may provide more information about $e$ such as the message that is sent/received at $e$ or “enter critical section” or “output some value”.

Edges describe causal dependencies between events:

-   The relation ${\rightarrow}$ contains *process edges*. They connect successive events executed by the same process. That is, we actually have ${\to} \subseteq \bigcup_{p \in {P}} (E_p \times E_p)$. Every process $p$ is sequential so that ${\to} \cap (E_p \times E_p)$ must be the direct-successor relation of some total order on $E_p$. We let ${{\leq_{\mathsf{proc}}}} {:=}{\to^\ast}$ and ${{<_{\mathsf{proc}}}} {:=}{\to^+}$.

-   The relation ${\lhd}$ contains *message edges*. If $e {\lhd}f$, then $e$ is a *send event* and $f$ is the corresponding *receive event*. In particular, $({\mathit{loc}}(e),{\mathit{loc}}(f)) \in {\mathit{Ch}}$. Each event is part of at most one message edge. 