we have ${\mathit{target}}(\rho(e)) = {\mathit{source}}(\rho(f))$,

4.  for all internal events $e \in E$, $\rho(e)$ is an internal transition, and

5.  for all message edges $e{\lhd}f$, $\rho(e)$ and $\rho(f)$ are respectively send and receive transitions such that ${\mathit{msg}}(\rho(e)) = {\mathit{msg}}(\rho(f))$, ${\mathit{receiver}}(\rho(e)) = {\mathit{loc}}(f)$, and ${\mathit{sender}}(\rho(f)) = {\mathit{loc}}(e)$.

To determine whether $\rho$ is accepting, we collect the last state $s_p$ of every process $p$. If $E_p \neq \emptyset$, we let $s_p = {\mathit{target}}(\rho(e))$, where $e$ is the last event of $E_p$. Otherwise, $s_p = {\iota}_p$. We say that $\rho$ is *accepting* if $(s_p)_{p \in {P}} \in {\mathit{Acc}}$.

The *language* ${\mathbb{L}}({\mathcal{A}})$ of ${\mathcal{A}}$ is the set of MSCs $M$ such that there exists an accepting run of ${\mathcal{A}}$ on $M$. Moreover, ${{\mathcal{L}}(\textup{CFM})}{:=}\{{\mathbb{L}}({\mathcal{A}}) \mid {\mathcal{A}}$ is a CFM$\}$. Recall that, for these definitions, we have fixed ${P}$ and $\Sigma$.

One of our main results states that CFMs and ${\textup{EMSO}}$ logic are expressively equivalent. This solves a problem that was stated as open in [@GKM07]:

\[thm:main\] ${\mathcal{L}}({\textup{EMSO}}[{\rightarrow},{\lhd},\le]) = {{\mathcal{L}}(\textup{CFM})}$.

It is standard to prove ${{\mathcal{L}}(\textup{CFM})}\subseteq {\mathcal{L}}({\textup{EMSO}}[{\rightarrow},{\lhd}])$: The formula guesses an assignment of transitions to events in terms of existentially quantified second-order variables (one for each transition) and then checks, in its first-order kernel, that the 