\rrbracket_{M}}$ but $(e_2,e_6) \not\in {\llbracket {{\xrightarrow{{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}}}}} \rrbracket_{M}}$.

We use the usual abbreviations for sentences and event formulas such as implication and conjunction. Moreover, ${\mathit{true}}{:=}p \vee \neg p$ (for some arbitrary process $p \in {P}$) and ${\mathit{false}}{:=}\neg{\mathit{true}}$. Finally, we define the event formula ${\mathop{\langle \pi \rangle}} {:=}{\mathop{\langle \pi \rangle} {{\mathit{true}}}}$, and the path formulas ${{\xrightarrow{+}}} {:=}{{\xrightarrow{{\mathit{true}}}}}$ and ${{\xrightarrow{\ast}}} {:=}{{\xrightarrow{+}}} \cup
{\{{\mathit{true}}\}?}$.

Note that there are some redundancies in the logic. For example (letting $\equiv$ denote logical equivalence), ${{\rightarrow}} \equiv {{\xrightarrow{{\mathit{false}}}}}$, $\pi_1 \cap \pi_2 \equiv {{({{\pi}^{\mathsf{c}}}_1 \cup {{\pi}^{\mathsf{c}}}_2)}^{\mathsf{c}}}$, and ${\mathsf{Loop}(\pi)} \equiv {\mathop{\langle {\{{\mathit{true}}\}?} \cap \pi \rangle}}$. Some of them are necessary to define certain subclasses of ${{\textup{PDL}_{\mathsf{sf}}}}$. For every $R \subseteq
\{{\mathsf{Loop}},\cup,\cap,{\mathsf{c}}\}$, we let ${{\textup{PDL}_{\mathsf{sf}}}}[R]$ denote the fragment of ${{\textup{PDL}_{\mathsf{sf}}}}$ that does not make use of $\{{\mathsf{Loop}},\cup,\cap,{\mathsf{c}}\} \setminus
R$. In particular, ${{\textup{PDL}_{\mathsf{sf}}}}= {{\textup{PDL}_{\mathsf{sf}}}}[{\mathsf{Loop}},\cup,\cap,{\mathsf{c}}]$. Note that, syntactically, ${{\xrightarrow{\ast}}}$ is not contained in ${{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}$ since union is not permitted.

Note that ${{\textup{PDL}_{\mathsf{sf}}}}[\cup]$ over MSCs is analogous to Conditional XPath over trees [@Marx05].[^2] However, while Marx showed that Conditional XPath is expressively complete for FO logic over ordered unranked trees, our expressive completeness result over MSCs crucially relies on the ${\mathsf{Loop}}$ modality.

Main Results
------------

Let ${\textup{FO}}^3[{\rightarrow},{\lhd},\le]$ be the 