from some event on process $p$ to some event on process $q$. Formally, we let ${\mathsf{Comp}({\rightarrow})}={\mathsf{Comp}({\leftarrow})}={\mathsf{Comp}({\xrightarrow{\varphi}})}={\mathsf{Comp}({\xleftarrow{\varphi}})}={\mathsf{Comp}({\{\varphi\}?})}={\mathsf{id}}$, where ${\mathsf{id}}=\{(p,p)\mid p\in{P}\}$; ${\mathsf{Comp}({\lhd}_{p,q})}={\mathsf{Comp}({\lhd}_{q,p}^{-1})}=\{(p,q)\}$; ${\mathsf{Comp}({\mathsf{jump}_{p,r}})}=\{(p,r)\}$; and ${\mathsf{Comp}(\pi_1\cdot\pi_2)}={\mathsf{Comp}(\pi_2)}\circ{\mathsf{Comp}(\pi_1)}=\{(p,r)\mid \exists q:
(p,q)\in{\mathsf{Comp}(\pi_1)}, (q,r)\in{\mathsf{Comp}(\pi_2)}\}$.

Notice that, for all path formulas $\pi \in {{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$, the relation ${\mathsf{Comp}(\pi)}$ is either empty or a singleton $\{(p,q)\}$ or the identity ${\mathsf{id}}$. Moreover, $M,e,f\models\pi$ implies $({\mathit{loc}}(e),{\mathit{loc}}(f))\in{\mathsf{Comp}(\pi)}$. Therefore, all events in ${\llbracket {\pi} \rrbracket}(e)$ are on the same process, and if this set is nonempty (i.e., if $M,e\models{\mathop{\langle \pi \rangle}}$), then ${\min {\llbracket {\pi} \rrbracket} (e)}$ and ${\max {\llbracket {\pi} \rrbracket} (e)}$ are well-defined.

Consider the MSC from Figure \[fig:msc\] and $\pi = {{\xrightarrow{+}}}{{\lhd}_{p_1,p_2}}{{\rightarrow}}{{\lhd}_{p_2,p_3}}{{\rightarrow}}$. We have ${\mathsf{Comp}(\pi)} = \{(p_1,p_3)\}$. Moreover, ${\min {\llbracket {\pi} \rrbracket} (e_2)} = g_4$ and ${\max {\llbracket {\pi} \rrbracket} (e_2)} = g_5$.

We say that $\pi \in {{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ is *monotone* if, for all MSCs $M$ and events $e,f$ such that $M,e \models {\mathop{\langle \pi \rangle}}$, $M,f \models {\mathop{\langle \pi \rangle}}$, and $e {\leq_{\mathsf{proc}}}f$, we have ${\min {\llbracket {\pi} \rrbracket} (e)} {\leq_{\mathsf{proc}}}{\min {\llbracket {\pi} \rrbracket} (f)}$ and ${\max {\llbracket {\pi} \rrbracket} (e)} {\leq_{\mathsf{proc}}}{\max {\llbracket {\pi} \rrbracket} (f)}$. Lemmas \[lem:min-conc\] and \[lem:monotone\] are shown by simultaneous induction.

\[lem:min-conc\] Let $\pi_1,\pi_2 \in {{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ be path formulas. For all MSCs $M$ and events $e$ 