(f0) – (f1); (f1) – (f2); (f2) – (f3); (f3) – (f4); (f4) – (f5); (f5) – (f6); (f6) – (f7);

(g0) – (g1); (g1) – (g2); (g2) – (g3); (g3) – (g4); (g4) – (g5); (g5) – (g6); (g6) – (g7);

at (-0.5,0) [$p_3$]{}; at (-0.5,1) [$p_2$]{}; at (-0.5,2) [$p_1$]{};

MSO Logic and Its Fragments
---------------------------

Next, we give an account of *monadic second-order* (MSO) logic and its fragments. Note that we restrict our attention to MSO logic interpreted *over MSCs*. We fix an infinite supply ${\mathcal{V}_{\mathsf{event}}}= \{x,y,\ldots\}$ of first-order variables, which range over events of an MSC, and an infinite supply ${\mathcal{V}_{\mathsf{set}}}= \{X,Y,\ldots\}$ of second-order variables, ranging over sets of events. The syntax of ${\textup{MSO}}$ (we consider that ${P}$ and $\Sigma$ are fixed) is given as follows: $$\begin{aligned}
{\Phi}& ~::=~ p(x) \mid a(x) \mid x = y \mid x {\rightarrow}y \mid x {\lhd}y \mid x \le y \mid x \in X \mid {\Phi}\lor {\Phi}\mid \lnot {\Phi}\mid
\exists x. {\Phi}\mid \exists X. {\Phi}\end{aligned}$$ where $p \in {P}$, $a \in \Sigma$, $x,y \in {\mathcal{V}_{\mathsf{event}}}$, and $X \in {\mathcal{V}_{\mathsf{set}}}$. We use the usual abbreviations to also include implication $\Longrightarrow$, conjunction $\wedge$, and universal quantification $\forall$. Moreover, the relation $x {\leq_{\mathsf{proc}}}y$ can 