{:=}\{ (e,f) \in E \times E \mid e {<_{\mathsf{proc}}}f \textup{ and } \forall g \in E\textup{: } e {<_{\mathsf{proc}}}g {<_{\mathsf{proc}}}f \implies M,g \models \varphi\}
}
\\
\multicolumn{2}{l}{
{\llbracket {{\xleftarrow{\varphi}}} \rrbracket_{M}} {:=}\{ (e,f) \in E \times E \mid f {<_{\mathsf{proc}}}e \textup{ and } \forall g \in E\textup{: } f {<_{\mathsf{proc}}}g {<_{\mathsf{proc}}}e \implies M,g \models \varphi\}
}
\\
\multicolumn{2}{l}{
{\llbracket {\pi_1 \cdot \pi_2} \rrbracket_{M}} {:=}\{ (e,g) \in E \times E \mid \exists f \in E:
                        (e,f)\in{\llbracket {\pi_1} \rrbracket_{M}} \land (f,g)\in{\llbracket {\pi_2} \rrbracket_{M}} \}
}
\\
{\llbracket {\pi_1 \cup \pi_2} \rrbracket_{M}} {:=}{\llbracket {\pi_1} \rrbracket_{M}} \cup {\llbracket {\pi_2} \rrbracket_{M}} &
{\llbracket {{{\pi}^{\mathsf{c}}}} \rrbracket_{M}} {:=}(E \times E) \setminus {\llbracket {\pi} \rrbracket_{M}}\\
{\llbracket {\pi_1 \cap \pi_2} \rrbracket_{M}} {:=}{\llbracket {\pi_1} \rrbracket_{M}} \cap {\llbracket {\pi_2} \rrbracket_{M}}\\[0.5ex]
\hline
\end{array}$

The usual temporal logic modalities can be expressed easily. For instance, ${\mathop{\langle {\rightarrow}\rangle} {\varphi}}$ means that the *next* event on the same process satisfies $\varphi$, and ${\mathop{\langle {\xrightarrow{\varphi}} \rangle} {\psi}}$ corresponds to the *strict until* $\mathsf{X}(\varphi\mathbin{\mathsf{U}}\psi$). The corresponding past modalities can be written similarly.

Consider again the MSC $M$ from Figure \[fig:msc\] and the path formula $\pi = {\lhd}^{-1}_{p_1,p_3} {{\rightarrow}} {{\lhd}_{p_1,p_2}} {{\rightarrow}} {{\lhd}_{p_2,p_3}} {{\rightarrow}}$. We have $M,g_5 \models {\mathsf{Loop}(\pi)}$. Moreover, $(e_2,e_5) \in {\llbracket {{\xrightarrow{{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}}}}} 