---
abstract: 'Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport’s happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.'
author:
- Benedikt Bollig
- Marie Fortin
- Paul Gastin
bibliography:
- 'lit.bib'
title: 'It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with “Happened Before”'
---

Introduction
============

First-order (FO) logic can be considered, in many ways, a reference specification language. It plays a key role in automated theorem proving and formal verification. In particular, FO logic over finite or infinite words is central in the verification of reactive systems. When a word is understood as a total order that reflects a chronological succession of events, it represents an execution of a sequential system. Apart from being a natural concept in itself, FO logic over words enjoys manifold characterizations. It defines exactly the star-free languages and coincides with recognizability by aperiodic monoids or natural subclasses of finite (B[ü]{}chi, respectively) automata (cf.[@DiGa08Thomas; @Tho97handbook] for overviews). Moreover, linear-time temporal logics are usually measured against their expressive power with respect to FO logic. For example, LTL is considered the yardstick temporal logic not least due to Kamp’s famous theorem, stating that LTL and FO logic are expressively equivalent [@Kamp68].

While FO logic on words is well understood, a lot remains to be said once concurrency enters into the picture. When several processes communicate through, say, unbounded first-in first-out (FIFO) channels, events are only partially ordered and a behavior, which is referred to as a *message sequence chart (MSC)*, reflects Lamport’s happened-before relation: an event $e$ happens before an event $f$ if, and only if, there is a “message flow” path from $e$ to $f$ [@Lamport78]. *Communicating finite-state machines* (CFMs) [@Brand1983] are to MSCs what finite automata are to words: a canonical model of finite-state processes that communicate through unbounded FIFO channels. Therefore, the FO logic of MSCs can be considered a canonical specification language for such systems. Unfortunately, its study turned out to be difficult, since algebraic and automata-theoretic approaches that work for words, trees, or Mazurkiewicz traces do not carry over. In particular, until now, the following central problem remained open:

Partial answers were given for CFMs with bounded channel capacity [@HenriksenJournal; @Kuske01; @GKM06] and for fragments of FO that restrict the logic to bounded-degree predicates [@BolligJournal] or to two variables [@BFG-stacs18].

In this paper, we answer the general question positively. To do so, we make a detour through a variant of propositional dynamic logic (PDL) with loop and converse [@FisL79; @Streett81]. Actually, we introduce *star-free* PDL, which serves as an interface between FO logic and CFMs. That is, there are two main tasks to accomplish:

-   Translate every FO sentence into a star-free PDL sentence.

-   Translate every star-free PDL sentence into a CFM.

Both parts constitute results of own interest. In particular, step (i) implies that, over MSCs, FO logic has the three-variable property, i.e., every FO sentence over MSCs can be rewritten into one that uses only three different variable names. Note that this is already interesting in the special case of words, where it follows from Kamp’s theorem [@Kamp68]. It is also noteworthy that star-free PDL is a *two-dimensional* temporal logic in the sense of Gabbay et al. [@Gabbay1981; @gabbay1994temporal]. Since every star-free PDL sentence is equivalent to some FO sentence, we actually provide a (higher-dimensional) temporal logic over MSCs that is expressively complete for FO logic.[^1] While step (i) is based on purely logical considerations, step (ii) builds on new automata constructions that allow us to cope with the loop operator of PDL.

Combining (i) and (ii) yields the translation from FO logic to CFMs. It follows that CFMs are expressively equivalent to *existential* MSO logic. Moreover, we can derive self-contained proofs of several results on channel-bounded CFMs whose original proofs refer to involved constructions for Mazurkiewicz traces (cf. Section \[sec:concl\]).

##### Related Work.

Let us give a brief account of what was already known on the relation between logic and CFMs. In the 60s, B[ü]{}chi, Elgot, and Trakhtenbrot proved that finite automata over words are expressively equivalent to monadic second-order logic [@Buechi:60; @Elgot1961; @Trakhtenbrot62]. Note that finite automata correspond to the special case of CFMs with a single process.

This classical result has been generalized to CFMs with bounded channels: Over *universally* bounded MSCs (where all possible linear extensions meet a given channel bound), deterministic CFMs are expressively equivalent to MSO logic [@HenriksenJournal; @Kuske01]. Over *existentially* bounded MSCs (some linear extension meets the channel bound), CFMs are still expressively equivalent to MSO logic [@GKM06], but inherently nondeterministic [@GKM07]. The proofs of these characterizations reduce message-passing systems to finite-state shared-memory systems so that deep results from Mazurkiewicz trace theory [@DiekertRozenberg95] can be applied.

This generic approach is no longer applicable when the restriction on the channel capacity is dropped. Actually, in general, CFMs do not capture MSO logic [@BolligJournal]. On the other hand, they are expressively equivalent to existential MSO logic when we discard the happened-before relation [@BolligJournal] or when restricting to two first-order variables [@BFG-stacs18]. Both results rely on normal forms of FO logic, due to Hanf [@Hanf1965] and Scott [@GradelO99], respectively. However, MSCs with the happened-before relation are structures of *unbounded* degree (while Hanf’s normal form requires structures of bounded degree), and we consider FO logic with *arbitrarily* many variables (while Scott’s normal form only applies to two-variable logic). That is, neither approach is applicable in our case.

Finally, there exists a translation of a loop-free PDL into CFMs [@BKM-lmcs10]. As our star-free PDL has a loop operator, we cannot exploit [@BKM-lmcs10] either.

##### Outline.

In Section \[sec:prel\], we recall basic notions such as MSCs, FO logic, and CFMs. Moreover, we state one of our main results: the translation of FO formulas into CFMs. Section \[sec:pdl\] presents star-free PDL and proves that it captures FO logic. In Section \[sec:pdl-cfm\], we establish the translation of star-free PDL into CFMs. We conclude in Section \[sec:concl\] mentioning applications of our results.

Preliminaries {#sec:prel}
=============

We consider message-passing systems in which processes communicate through unbounded FIFO channels. We fix a nonempty finite set of *processes* ${P}$ and a nonempty finite set of *labels* $\Sigma$. For all $p,q \in {P}$ such that $p \neq q$, there is a channel $(p,q)$ that allows $p$ to send messages to $q$. The set of channels is denoted ${\mathit{Ch}}$.

In the following, we define message sequence charts, which represent executions of a message-passing system, and logics to reason about them. Then, we recall the definition of communicating finite-state machines and state one of our main results.

Message Sequence Charts
-----------------------

A *message sequence chart (MSC)* (over ${P}$ and $\Sigma$) is a graph $M=(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ with nonempty finite set of nodes $E$, edge relations ${{\rightarrow}},{{\lhd}} \subseteq E \times E$, and node-labeling functions ${\mathit{loc}}\colon E \to {P}$ and $\lambda\colon E \to \Sigma$. An example MSC is depicted in Figure \[fig:msc\]. A node $e \in E$ is an *event* that is executed by process ${\mathit{loc}}(e) \in {P}$. In particular, $E_p {:=}\{e \in E \mid {\mathit{loc}}(e) = p\}$ is the set of events located on $p$. The label $\lambda(e) \in \Sigma$ may provide more information about $e$ such as the message that is sent/received at $e$ or “enter critical section” or “output some value”.

Edges describe causal dependencies between events:

-   The relation ${\rightarrow}$ contains *process edges*. They connect successive events executed by the same process. That is, we actually have ${\to} \subseteq \bigcup_{p \in {P}} (E_p \times E_p)$. Every process $p$ is sequential so that ${\to} \cap (E_p \times E_p)$ must be the direct-successor relation of some total order on $E_p$. We let ${{\leq_{\mathsf{proc}}}} {:=}{\to^\ast}$ and ${{<_{\mathsf{proc}}}} {:=}{\to^+}$.

-   The relation ${\lhd}$ contains *message edges*. If $e {\lhd}f$, then $e$ is a *send event* and $f$ is the corresponding *receive event*. In particular, $({\mathit{loc}}(e),{\mathit{loc}}(f)) \in {\mathit{Ch}}$. Each event is part of at most one message edge. An event that is neither a send nor a receive event is called *internal*. Moreover, for all $(p,q) \in {\mathit{Ch}}$ and $(e,f), (e',f') \in {{\lhd}} \cap (E_p
    \times E_q)$, we have $e {\leq_{\mathsf{proc}}}e'$ iff $f {\leq_{\mathsf{proc}}}f'$ (which guarantees a FIFO behavior).

We require that ${{\rightarrow}} \cup {{\lhd}}$ be acyclic (intuitively, messages cannot travel backwards in time). The associated partial order is denoted ${\le} {:=}({{\rightarrow}} \cup {{\lhd}})^*$ with strict part ${<}=({{\rightarrow}} \cup {{\lhd}})^+$. We do not distinguish isomorphic MSCs. Let ${\mathbb{MSC}({P},\Sigma)}$ denote the set of MSCs over ${P}$ and $\Sigma$.

Actually, MSCs are very similar to the space-time diagrams from Lamport’s seminal paper [@Lamport78], and $\le$ is commonly referred to as the *happened-before relation*.

It is worth noting that, when ${P}$ is a singleton, an MSC with events $e_1
\to e_2 \to \ldots \to e_n$ can be identified with the word $\lambda(e_1)\lambda(e_2) \ldots \lambda(e_n) \in \Sigma^\ast$.

= \[draw, fill=white, circle, inner sep=0, minimum size=0.25cm, draw=black\] = \[draw, fill=white, rectangle, inner sep=0, minimum size=0.2cm, draw=black\] = \[draw, fill=white, diamond, inner sep=0, minimum size=0.3cm\]

Consider the MSC from Figure \[fig:msc\] over ${P}=\{p_1,p_2,p_3\}$ and $\Sigma = \{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] circle (2.8pt);
\end{tikzpicture}
},{\resizebox{!}{1.4ex}{$\diamond$}}\}$. We have, for instance, $E_{p_1} =
  \{e_0,\ldots,e_7\}$. The process relation is given by $e_i \to e_{i+1}$, $f_i
  \to f_{i+1}$, and $g_i \to g_{i+1}$ for all $i \in \{0,\ldots,6\}$. Concerning the message relation, we have $e_1 {\lhd}f_0$, $e_4 {\lhd}g_5$, etc. Moreover, $e_2 \le f_3$, but neither $e_2 \le f_1$ nor $f_1 \le
  e_2$.

(e0) at (0.25,2) ; (f0) at (0.25,0) ; (e0) – (f0);

(e1) at (1.125,2) ; (g0) at (1.125,1) ; (e1) – (g0);

(e2) at (2,2) ; (f1) at (2,0) ; (e2) – (f1);

(g1) at (3,1) ; (f2) at (3.75,0) ; (g1) – (f2);

(e3) at (4,2) ; (g2) at (4,1) ; (e3) – (g2);

(g3) at (5,1) ; (f3) at (5.5,0) ; (g3) – (f3);

(e4) at (5,2) ; (f5) at (8.75,0) ; (e4) – (f5);

(e5) at (6,2) ; (g4) at (6,1) ; (e5) – (g4);

(g5) at (7.5,1) ; (f4) at (7.5,0) ; (g5) – (f4);

(e6) at (9,2) ; (f6) at (10.5,0) ; (e6) – (f6);

(e7) at (11,2) ; (g6) at (11,1) ; (e7) – (g6);

(g7) at (12,1) ; (f7) at (12,0) ; (g7) – (f7);

(e0) – (e1); (e1) – (e2); (e2) – (e3); (e3) – (e4); (e4) – (e5); (e5) – (e6); (e6) – (e7);

(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 be defined by $x \le y \wedge \bigvee_{p \in {P}} p(x) \wedge p(y)$. We write ${\mathsf{Free}}(\Phi)$ the set of free variables of $\Phi$.

Let $M = (E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ be an MSC. An *interpretation* (for $M$) is a mapping $\nu\colon {\mathcal{V}_{\mathsf{event}}}\cup {\mathcal{V}_{\mathsf{set}}}\to E \cup 2^E$ assigning to each $x \in {\mathcal{V}_{\mathsf{event}}}$ an event $\nu(x) \in E$, and to each $X \in {\mathcal{V}_{\mathsf{set}}}$ a set of events $\nu(X) \subseteq E$. We write $M,\nu \models {\Phi}$ if $M$ satisfies ${\Phi}$ when the free variables of ${\Phi}$ are interpreted according to $\nu$. Hereby, satisfaction is defined in the usual manner. In fact, whether $M,\nu \models {\Phi}$ holds or not only depends on the interpretation of variables that occur free in ${\Phi}$. Thus, we may restrict $\nu$ to any set of variables that contains at least all free variables. For example, for ${\Phi}(x,y) = (x {\lhd}y)$, we have $M,[x \mapsto e, y \mapsto f] \models {\Phi}(x,y)$ iff $e {\lhd}f$. For a *sentence* ${\Phi}\in {\textup{MSO}}$ (without free variables), we define ${\mathbb{L}}({\Phi}) {:=}\{M \in {\mathbb{MSC}({P},\Sigma)} \mid M \models {\Phi}\}$.

We say that two formulas ${\Phi}$ and ${\Phi}'$ are *equivalent*, written ${\Phi}\equiv {\Phi}'$, if, for all MSCs $M = (E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ and interpretations $\nu \colon {\mathcal{V}_{\mathsf{event}}}\cup {\mathcal{V}_{\mathsf{set}}}\to E \cup 2^E$, we have $M,\nu \models {\Phi}$ iff $M,\nu \models {\Phi}'$.

Let us identify two important fragments of MSO logic: *First-order* () formulas do not make use of second-order quantification (however, they may contain formulas $x \in X$). Moreover, *existential* MSO (${\textup{EMSO}}$) formulas are of the form $\exists X_1 \ldots \exists X_n.{\Phi}$ with ${\Phi}\in {\textup{FO}}$.

Let ${\mathcal{F}}$ be ${\textup{MSO}}$ or ${\textup{EMSO}}$ or ${\textup{FO}}$ and let $R
\subseteq\{{\rightarrow},{\lhd},\le\}$. We obtain the logic ${\mathcal{F}}[{R}]$ by restricting ${\mathcal{F}}$ to formulas that do not make use of $\{{\rightarrow},{\lhd},\le\}
\setminus {R}$. Note that ${\mathcal{F}}= {\mathcal{F}}[{\rightarrow},{\lhd},\le]$. Moreover, we let ${\mathcal{L}}({\mathcal{F}}[R]) {:=}\{{\mathbb{L}}({\Phi}) \mid {\Phi}\in {\mathcal{F}}[R]$ is a sentence$\}$.

Since the reflexive transitive closure of an MSO-definable binary relation is MSO-definable, ${\textup{MSO}}$ and ${\textup{MSO}}[{\rightarrow},{\lhd}]$ have the same expressive power: ${\mathcal{L}}({\textup{MSO}}[{\rightarrow},{\lhd},\leq])={\mathcal{L}}({\textup{MSO}}[{\rightarrow},{\lhd}])$. However, ${\textup{MSO}}[\le]$ (without the message relation) is strictly weaker than ${\textup{MSO}}$ [@BolligJournal].

We give an FO formula that allows us to recover, at some event $f$, the most recent event $e$ that happened in the past on, say, process $p$. More precisely, we define the predicate $\mathit{latest}_p(x,y)$ as $x \le y \wedge
  p(x) \wedge \forall z\bigl((z \le y \wedge p(z)) \implies z \le x\bigr)$. The “gossip language” says that process $q$ always maintains the latest information that it can have about $p$. Thus, it is defined by ${\Phi}^{\mathsf{gossip}}_{p,q} = \forall x\forall
  y.\bigl((\mathit{latest}_p(x,y) \wedge q(y)) \implies \bigvee_{a \in \Sigma}
  (a(x) \wedge a(y))\bigr) \in {\textup{FO}}^3[\le]$. For example, for ${P}=\{p_1,p_2,p_3\}$ and $\Sigma = \{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] circle (2.8pt);
\end{tikzpicture}
},{\resizebox{!}{1.4ex}{$\diamond$}}\}$, the MSC $M$ from Figure \[fig:msc\] is contained in ${\mathbb{L}}({\Phi}^{\mathsf{gossip}}_{p_1,p_3})$. In particular, $M,[x \mapsto e_5, y
  \mapsto g_5] \models \mathit{latest}_{p_1}(x,y)$ and $\lambda(e_5) =
  \lambda(g_5) = {
\begin{tikzpicture}
\filldraw[fill=white,draw=black] circle (2.8pt);
\end{tikzpicture}
}$.

Communicating Finite-State Machines
-----------------------------------

In a communicating finite-state machine, each process $p \in {P}$ can perform internal actions of the form ${\langlea\rangle}$, where $a \in \Sigma$, or send/receive messages from a finite set of messages ${\mathit{Msg}}$. A send action ${\langlea,!_{q}{m}\rangle}$ of process $p$ writes message ${m}\in {\mathit{Msg}}$ to channel $(p,q)$, and performs $a \in \Sigma$. A receive action ${\langlea,?_{q}{m}\rangle}$ reads message ${m}$ from channel $(q,p)$. Accordingly, we let ${\mathit{Act}_{p}({\mathit{Msg}})} {:=}\{{\langlea\rangle} \mid a \in \Sigma\} \cup
\{{\langlea,!_{q}{m}\rangle} \mid a \in \Sigma$, $m \in {\mathit{Msg}}$, $q \in {P}\setminus\{p\}\} \cup
\{{\langlea,?_{q}{m}\rangle} \mid a \in \Sigma$, $m \in {\mathit{Msg}}$, $q \in {P}\setminus\{p\}\}$ denote the set of possible actions of process $p$.

A *communicating finite-state machine (CFM)* over ${P}$ and $\Sigma$ is a tuple $(({\mathcal{A}}_p)_{p \in {P}},{\mathit{Msg}},{\mathit{Acc}})$ consisting of a finite set of messages ${\mathit{Msg}}$ and a finite-state transition system ${\mathcal{A}}_p=(S_p,{\iota}_p,\Delta_p)$ for each process $p$, with finite set of states $S_p$, initial state ${\iota}_p \in S_p$, and transition relation $\Delta_p \subseteq S_p \times {\mathit{Act}_{p}({\mathit{Msg}})} \times S_p$. Moreover, we have an acceptance condition ${\mathit{Acc}}\subseteq \prod_{p \in {P}} S_p$.

Given a transition $t = (s,{\alpha},s') \in \Delta_p$, we let ${\mathit{source}}(t) = s$ and ${\mathit{target}}(t) = s'$ denote the source and target states of $t$. In addition, if ${\alpha}= {\langlea\rangle}$, then $t$ is an *internal transition* and we let ${\mathit{label}}(t) = a$. If ${\alpha}= {\langlea,!_{q}{m}\rangle}$, then $t$ is a *send transition* and we let ${\mathit{label}}(t) = a$, ${\mathit{msg}}(t) = {m}$, and ${\mathit{receiver}}(t) = q$. Finally, if ${\alpha}= {\langlea,?_{q}{m}\rangle}$, then $t$ is a *receive transition* with ${\mathit{label}}(t) = a$, ${\mathit{msg}}(t) = {m}$, and ${\mathit{sender}}(t) = q$.

A *run* $\rho$ of ${\mathcal{A}}$ on an MSC $M = (E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda) \in {\mathbb{MSC}({P},\Sigma)}$ is a mapping associating with each event $e \in E_p$ a transition $\rho(e) \in \Delta_p$, and satisfying the following conditions:

1.  for all events $e \in E$, we have ${\mathit{label}}(\rho(e)) = \lambda(e)$,

2.  for all ${\rightarrow}$-minimal events $e \in E$, we have ${\mathit{source}}(\rho(e))={\iota}_{p}$, where $p = {\mathit{loc}}(e)$,

3.  for all process edges $(e,f) \in {{\rightarrow}}$, 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 assignment is indeed an (accepting) run. As, moreover, the class ${{\mathcal{L}}(\textup{CFM})}$ is closed under projection, the proof of Theorem \[thm:main\] comes down to the proposition below (whose proof is spread over Sections \[sec:pdl\] and \[sec:pdl-cfm\]). Note that the translation from ${{\textup{FO}}[{\rightarrow},{\lhd},\le]}$ to CFMs is inherently non-elementary, already when $|{P}| = 1$ [@phd-stockmeyer].

\[prop:fo-cfm\] ${\mathcal{L}}({\textup{FO}}[{\rightarrow},{\lhd},\le]) \subseteq {{\mathcal{L}}(\textup{CFM})}$.

Star-Free Propositional Dynamic Logic {#sec:pdl}
=====================================

In this section, we introduce a star-free version of propositional dynamic logic and show that it is expressively equivalent to ${\textup{FO}}[{\rightarrow},{\lhd},\leq]$. This is the second main result of the paper. Then, in Section \[sec:pdl-cfm\], we show how to translate star-free PDL formulas into CFMs.

Syntax and Semantics
--------------------

Originally, propositional dynamic logic (PDL) has been used to reason about program schemas and transition systems [@FisL79]. Since then, PDL and its extension with intersection and converse have developed a rich theory with applications in artificial intelligence and verification [@HalpernM92; @GiacomoL94; @LangeLutzJSL05; @Lange06; @Goeller2009]. It has also been applied in the context of MSCs [@BKM-lmcs10; @Mennicke13].

Here, we introduce a *star-free* version of PDL, denoted ${{\textup{PDL}_{\mathsf{sf}}}}$. It will serve as an “interface” between FO logic and CFMs. The syntax of ${{\textup{PDL}_{\mathsf{sf}}}}$ and its fragment ${{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}$ is given by the following grammar:

where $p,r \in {P}$, $q \in {P}\setminus \{p\}$, and $a \in \Sigma$. We refer to ${\xi}$ as a *sentence*, to $\varphi$ as an *event formula*, and to $\pi$ as a *path formula*. We name the logic star-free because we use the operators $(\cup,\cap,{\mathsf{c}},\cdot)$ of star-free regular expressions instead of the regular-expression operators $(\cup,\cdot,\ast)$ of classical PDL. However, the formula ${\xrightarrow{\varphi}}$, whose semantics is explained below, can be seen as a restricted use of the construct $\pi^\ast$.

A sentence ${\xi}$ is evaluated wrt. an MSC $M =
(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$. An event formula $\varphi$ is evaluated wrt. $M$ and an event $e \in E$. Finally, a path formula $\pi$ is evaluated over *two* events. In other words, it defines a binary relation ${\llbracket {\pi} \rrbracket_{M}} \subseteq E \times E$. We often write $M,e,f \models \pi$ to denote $(e,f) \in {\llbracket {\pi} \rrbracket_{M}}$. Moreover, for $e \in E$, we let ${\llbracket {\pi} \rrbracket_{M}}(e) {:=}\{f \in E \mid (e,f) \in {\llbracket {\pi} \rrbracket_{M}}\}$. When $M$ is clear from the context, we may write ${\llbracket {\pi} \rrbracket}$ instead of ${\llbracket {\pi} \rrbracket_{M}}$. The semantics of sentences, event formulas, and path formulas is given in Table \[table:sem-PDL\].

$\begin{array}{ll}
\hline
\multicolumn{2}{l}{
M \models {\mathop{\mathsf{E}\vphantom{a}}\nolimits}\varphi \textup{ if } M,e \models \varphi \text{ for some event } e\in E}
\\
M \models \neg{\xi}\textup{ if } M \not\models {\xi}&
M \models {\xi}_1 \vee {\xi}_2 \textup{ if } M \models {\xi}_1 \textup{ or } M \models {\xi}_2\\[0.5ex]
\hline
M,e \models p \textup{ if } {\mathit{loc}}(e) = p &
M,e \models {\mathop{\langle \pi \rangle} {\varphi}} \textup{ if } \exists f \in {\llbracket {\pi} \rrbracket_{M}} (e): M,f \models \varphi
\\
M,e \models a \textup{ if } \lambda(e) = a &
M,e \models {\mathsf{Loop}(\pi)} \textup{ if } (e,e) \in {\llbracket {\pi} \rrbracket_{M}}
\\
M,e \models \neg\varphi \textup{ if } M,e \not\models \varphi &
M,e \models \varphi_1 \vee \varphi_2 \textup{ if } M,e \models \varphi_1 \textup{ or } M,e \models \varphi_2\\[0.5ex]
\hline
{\llbracket {{\rightarrow}} \rrbracket_{M}} {:=}\{ (e,f) \in E \times E \mid e \to f \}~~~~ &
{\llbracket {{\lhd}_{p,q}} \rrbracket_{M}} {:=}\{ (e,f) \in E_p \times E_q \mid e {\lhd}f \}
\\
{\llbracket {{\leftarrow}} \rrbracket_{M}} {:=}\{ (f,e) \in E \times E \mid e {\rightarrow}f \} &
{\llbracket {{\lhd}_{p,q}^{-1}} \rrbracket_{M}} {:=}\{ (f,e) \in E_q \times E_p \mid e {\lhd}f \}
\\
{\llbracket {{\mathsf{jump}_{p,r}}} \rrbracket_{M}} {:=}E_p \times E_r &
{\llbracket {{\{\varphi\}?}} \rrbracket_{M}} {:=}\{ (e,e) \mid e \in E : M,e \models \varphi \}
\\
\multicolumn{2}{l}{
{\llbracket {{\xrightarrow{\varphi}}} \rrbracket_{M}} {:=}\{ (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}
}}}}} \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 set of formulas from ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ that use at most three different first-order variables (however, a variable can be quantified and reused several times in a formula). The main result of this section is that, for formulas with zero or one free variable, the logics ${\textup{FO}}[{\rightarrow},{\lhd},\le]$, ${\textup{FO}}^3[{\rightarrow},{\lhd},\le]$, ${{{\textup{PDL}_{\mathsf{sf}}}}}$, and ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ are expressively equivalent.

Consider ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ formulas $\Phi_0$, $\Phi_1(x)$ and $\Phi_2(x,y)$ with respectively zero, one, and two free variables (hence, $\Phi_0$ is a sentence). Consider also some ${{{\textup{PDL}_{\mathsf{sf}}}}}$ sentence ${\xi}$, event formula $\varphi$, and path formula $\pi$. The respective formulas are equivalent, written $\Phi_0\equiv{\xi}$, $\Phi_1(x)\equiv\varphi$, and $\Phi_2(x,y)\equiv\pi$, if, for all MSCs $M$ and all events $e,f$ in $M$, we have $$\begin{aligned}
  M &\models \Phi_0 && \text{iff} & M &\models {\xi}\\
  M,[x\mapsto e] &\models \Phi_1(x) && \text{iff} & M,e &\models \varphi \\
  M,[x \mapsto e, y \mapsto f] &\models \Phi_2(x,y) && \text{iff} & M,e,f &\models \pi\end{aligned}$$

We start with a simple observation, which can be shown easily by induction:

\[prop:pdl-fo3\] Every ${{{\textup{PDL}_{\mathsf{sf}}}}}$ formula is equivalent to some ${\textup{FO}}^3[{\rightarrow},{\lhd},\le]$ formula. More precisely, for every ${{{\textup{PDL}_{\mathsf{sf}}}}}$ sentence ${\xi}$, event formula $\varphi$, and path formula $\pi$, there exist some ${\textup{FO}}^3[{\rightarrow},{\lhd},\le]$ sentence $\widetilde{{\xi}}$, formula ${\widetilde{\varphi}}(x)$ with one free variable, and formula ${\widetilde{\pi}}(x,y)$ with two free variables, respectively, such that, ${\xi}\equiv\widetilde{{\xi}}$, $\varphi\equiv{\widetilde{\varphi}}(x)$, and $\pi\equiv{\widetilde{\pi}}(x,y)$.

The main result is a *strong* converse of Proposition \[prop:pdl-fo3\]:

\[thm:FO-to-PDLm-main\] Every ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ formula with at most two free variables is equivalent to some ${{{\textup{PDL}_{\mathsf{sf}}}}}$ formula. More precisely, for every ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ sentence $\Phi_0$, formula $\Phi_1(x)$ with one free variable, and formula $\Phi_2(x,y)$ with two free variables, there exist some ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ sentence ${\xi}$, ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ event formula $\varphi$, and ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ path formulas $\pi_{ij}$, respectively, such that, $\Phi_0\equiv{\xi}$, $\Phi_1(x)\equiv\varphi$, and $\Phi_2(x,y)\equiv\bigcup_i\bigcap_j\pi_{ij}$.

From Theorem \[thm:FO-to-PDLm-main\] and Proposition \[prop:pdl-fo3\], we deduce that ${\textup{FO}}$ has the three variable property:

\[thm:fo3\] ${\mathcal{L}}({\textup{FO}}[{\rightarrow},{\lhd},\le]) = {\mathcal{L}}({\textup{FO}}^3[{\rightarrow},{\lhd},\le])$.

From ${\textup{FO}}$ to $\boldsymbol{{{{\textup{PDL}_{\mathsf{sf}}}}}}$ {#sec:fo-pdl}
-----------------------------------------------------------------------

In the remainder of this section, we give the translation from ${\textup{FO}}$ to ${{{\textup{PDL}_{\mathsf{sf}}}}}$. We start with some basic properties of ${{{\textup{PDL}_{\mathsf{sf}}}}}$. First, the converse of a ${{{\textup{PDL}_{\mathsf{sf}}}}}$ formula is definable in ${{{\textup{PDL}_{\mathsf{sf}}}}}$ (easy induction on $\pi$).

\[lem:inverse\] Let $R \subseteq \{{\mathsf{Loop}},\cup,\cap,{\mathsf{c}}\}$ and $\pi \in {\textup{PDL}_{\mathsf{sf}}}[R]$ be a path formula. There exists $\pi^{-1} \in {\textup{PDL}_{\mathsf{sf}}}[R]$ such that, for all MSCs $M$, ${\llbracket {\pi^{-1}} \rrbracket_{M}} = {\llbracket {\pi} \rrbracket_{M}}^{-1} = \{(f,e) \mid (e,f) \in {\llbracket {\pi} \rrbracket_{M}}\}$.

Given a ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ path formula $\pi$, we denote by ${\mathsf{Comp}(\pi)}$ the set of pairs $(p,q) \in {P}\times {P}$ such that there may be a $\pi$-path 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$ such that $M,e\models{\mathop{\langle \pi_1 \cdot \pi_2 \rangle}}$, we have $$\begin{aligned}
    {\min {\llbracket {\pi_1 \cdot \pi_2} \rrbracket} (e)} & = {\min {\llbracket {\pi_2} \rrbracket} ({\min {\llbracket {\pi_1 \cdot {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)})} \text{ and }
      \\
    {\max {\llbracket {\pi_1 \cdot \pi_2} \rrbracket} (e)} & = {\max {\llbracket {\pi_2} \rrbracket} ({\max {\llbracket {\pi_1 \cdot {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)})} \, .
  \end{aligned}$$

\[lem:monotone\] All ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ path formulas are monotone.

We first show that Lemma \[lem:min-conc\] holds when $\pi_2$ is monotone. We then use this to prove by induction that all ${\textup{PDL}_{\mathsf{sf}}}$ formulas are monotone (Lemma \[lem:monotone\]). Therefore, we deduce that Lemma \[lem:min-conc\] is always true.

Let $\pi_1,\pi_2 \in {{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ be path formulas such that $\pi_2$ is monotone. Let $M$ be an MSCs and $e$ be some event in $M$ such that $M,e\models{\mathop{\langle \pi_1\pi_2 \rangle}}$. The proof is illustrated in Figure \[fig:min-conc\]. We let $g = {\min {\llbracket {\pi_1 \pi_2} \rrbracket} (e)}$. Since $M,e,g \models \pi_1\pi_2$, there exists $f$ such that $M,e,f \models \pi_1$, and $M,f,g \models \pi_2$. In particular, $M,e,f \models \pi_1 {\{{\mathop{\langle \pi_2 \rangle}}\}?}$, so $f' =
  {\min {\llbracket {\pi_1 {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)}$ is well-defined and $f'
  {\leq_{\mathsf{proc}}}f$. Since $\pi_2$ is monotone, ${\min {\llbracket {\pi_2} \rrbracket} (f')} {\leq_{\mathsf{proc}}}{\min {\llbracket {\pi_2} \rrbracket} (f)} {\leq_{\mathsf{proc}}}g$. Also, $M,e,{\min {\llbracket {\pi_2} \rrbracket} (f')} \models \pi_1\pi_2$. Hence $g {\leq_{\mathsf{proc}}}{\min {\llbracket {\pi_2} \rrbracket} (f')}$. Therefore, $g = {\min {\llbracket {\pi_2} \rrbracket} (f')}$.

The proof that ${\max {\llbracket {\pi_1 \pi_2} \rrbracket} (e)} =
  {\max {\llbracket {\pi_2} \rrbracket} ({\max {\llbracket {\pi_1 {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)})}$ is similar.

\(e) at (0,0) ; (f) at (1,1) ; (fp) at (-1,1) ; (gp) at (-1.1,2) ; (g) at (0,2) ; (leproc) at (0,1) [${\leq_{\mathsf{proc}}}$]{}; at (-0.5,1.95) [${\leq_{\mathsf{proc}}}$]{};

\(e) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[right\] [$\pi_1$]{} (f) (e) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[left\] [$\pi_1$]{} (fp) (f) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[right\] [$\pi_2$]{} (g) (fp) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[left\] [$\pi_2$]{} (gp);

We turn now to the proof of Lemma \[lem:monotone\]. Actually, we prove a slightly stronger statement. We show by induction on $\pi$ that, for all ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ event formulas $\psi$, the path formula $\pi \cdot {\{\psi\}?}$ is monotone.

Let $e,f$ be events such that $e{\leq_{\mathsf{proc}}}f$, $M,e\models\pi\cdot{\{\psi\}?}$ and $M,f\models\pi\cdot{\{\psi\}?}$. Let $e' = {\min {\llbracket {\pi\cdot{\{\psi\}?}} \rrbracket} (e)}$ and $f' = {\min {\llbracket {\pi\cdot{\{\psi\}?}} \rrbracket} (f)}$. We show that $e'{\leq_{\mathsf{proc}}}f'$. The proof that ${\max {\llbracket {\pi\cdot{\{\psi\}?}} \rrbracket} (e)}{\leq_{\mathsf{proc}}}{\max {\llbracket {\pi\cdot{\{\psi\}?}} \rrbracket} (e)}$ is similar. We start with the base cases.

If $\pi = {\{\varphi\}?}$, we have $e' = e {\leq_{\mathsf{proc}}}f = f'$. The result is also trivial for $\pi={{\rightarrow}}$ or $\pi={{\leftarrow}}$. It follows from the fact that channels are FIFO for $\pi={{\lhd}_{p,q}}$ or $\pi={{\lhd}_{p,q}^{-1}}$. When $\pi={\mathsf{jump}_{p,q}}$ we have $e'=f'$. Suppose that $\pi={{\xrightarrow{\varphi}}}$. It is easy to see that either $e'{\leq_{\mathsf{proc}}}f{<_{\mathsf{proc}}}f'$ or $e'=f'$. Similarly, when $\pi={{\xleftarrow{\varphi}}}$ we have either $e'{<_{\mathsf{proc}}}e{\leq_{\mathsf{proc}}}f'$ or $e'=f'$.

The proof for $\pi=\pi_1\cdot\pi_2$ is illustrated in Figure \[fig:monotone\].

\(e) at (0,0) ; (f) at (2,0) ; (leproc) at (1,0) [${\leq_{\mathsf{proc}}}$]{};

(epp) at (-0.5,1) ; (fpp) at (1.5,1) ; (leproc) at (0.5,1) [${\leq_{\mathsf{proc}}}$]{};

(ep) at (-0.5,2) ; (fp) at (1.5,2) ; (leproc) at (0.5,2) [${\leq_{\mathsf{proc}}}$]{};

\(e) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[left\] [$\pi_1$]{} (epp) (f) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[right\] [$\pi_1$]{} (fpp) (epp) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[left\] [$\pi_2$]{} (ep) (fpp) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[right\] [$\pi_2$]{} (fp);

By induction, the path formula $\pi_2\cdot{\{\psi\}?}$ is monotone. So we can apply the special case of Lemma \[lem:min-conc\] proved above to the product $\pi_1\cdot(\pi_2\cdot{\{\psi\}?})$. Let $e''={\min {\llbracket {\pi_1\cdot{\{{\mathop{\langle \pi_2 \rangle} {\psi}}\}?}} \rrbracket} (e)}$ and $f''={\min {\llbracket {\pi_1\cdot{\{{\mathop{\langle \pi_2 \rangle} {\psi}}\}?}} \rrbracket} (f)}$. We have $e'={\min {\llbracket {\pi_2\cdot{\{\psi\}?}} \rrbracket} (e'')}$ and $f'={\min {\llbracket {\pi_2\cdot{\{\psi\}?}} \rrbracket} (f'')}$. Again by induction, the path formula $\pi_1 \cdot {\{{\mathop{\langle \pi_2 \rangle} {\psi}}\}?}$ is monotone and we obtain $e''{\leq_{\mathsf{proc}}}f''$. We get $e'{\leq_{\mathsf{proc}}}f'$ since $\pi_2\cdot{\{\psi\}?}$ is monotone.

The following crucial lemma states that, for all path formulas $\pi \in {{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ and events $e$ in some MSC, ${\llbracket {\pi} \rrbracket} (e)$ contains precisely the events that lie in the interval between ${\min {\llbracket {\pi} \rrbracket} (e)}$ and ${\max {\llbracket {\pi} \rrbracket} (e)}$ and that satisfy ${\mathop{\langle \pi^{-1} \rangle}}$.

\[lem:image\] Let $\pi$ be a ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ path formula. For all MSCs $M$ and events $e$ such that $M,e\models{\mathop{\langle \pi \rangle}}$, we have $${\llbracket {\pi} \rrbracket} (e) = \{ f \in E \mid {\min {\llbracket {\pi} \rrbracket} (e)} {\leq_{\mathsf{proc}}}f {\leq_{\mathsf{proc}}}{\max {\llbracket {\pi} \rrbracket} (e)} \land M,f \models {\mathop{\langle \pi^{-1} \rangle}} \} \, .$$

The left-to-right inclusion is trivial. We prove the right-to-left inclusion by induction on $\pi$. The base cases are immediate.

Assume that $\pi = \pi_1 \cdot \pi_2$. For illustration, consider Figure \[fig:image\]. We let $f_1 = {\min {\llbracket {\pi_1 {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)}$, $f_2 = {\min {\llbracket {\pi_2} \rrbracket} (f_1)}$, $g_1 = {\max {\llbracket {\pi_1 {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)}$, and $g_2 = {\max {\llbracket {\pi_2} \rrbracket} (g_1)}$. By Lemma \[lem:min-conc\], we have $f_2={\min {\llbracket {\pi_1\pi_2} \rrbracket} (e)}$ and $g_2={\max {\llbracket {\pi_1\pi_2} \rrbracket} (e)}$. Let $h_2 \in E$ such that $f_2 {\leq_{\mathsf{proc}}}h_2 {\leq_{\mathsf{proc}}}g_2$ and $M,h_2 \models {\mathop{\langle (\pi_1\pi_2)^{-1} \rangle}}$. If $h_2 {\leq_{\mathsf{proc}}}{\max {\llbracket {\pi_2} \rrbracket} (f_1)}$, then by induction hypothesis, $M,f_1,h_2 \models \pi_2$, and we obtain $M,e,h_2 \models \pi_1\pi_2$. Similarly, if ${\min {\llbracket {\pi_2} \rrbracket} (g_1)} {\leq_{\mathsf{proc}}}h_2$, then $M,g_1,h_2 \models \pi_2$ and $M,e,h_2 \models \pi_1\pi_2$. So assume ${\max {\llbracket {\pi_2} \rrbracket} (f_1)} {<_{\mathsf{proc}}}h_2 {<_{\mathsf{proc}}}{\min {\llbracket {\pi_2} \rrbracket} (g_1)}$. Since $M,h_2 \models {\mathop{\langle \pi_2^{-1}\pi_1^{-1} \rangle}}$, there exists $h_1$ such that $M,h_1,h_2 \models \pi_2$ and $M,h_1 \models {\mathop{\langle \pi_1^{-1} \rangle}}$. Moreover, ${\min {\llbracket {\pi_2} \rrbracket} (h_1)} {\leq_{\mathsf{proc}}}h_2 {<_{\mathsf{proc}}}{\min {\llbracket {\pi_2} \rrbracket} (g_1)}$, hence $h_1 {\leq_{\mathsf{proc}}}g_1$ by Lemma \[lem:monotone\] (notice that $g_1$ and $h_1$ must be on the same process). Similarly, ${\max {\llbracket {\pi_2} \rrbracket} (f_1)} {<_{\mathsf{proc}}}h_2 {\leq_{\mathsf{proc}}}{\max {\llbracket {\pi_2} \rrbracket} (h_1)}$, hence $f_1 {\leq_{\mathsf{proc}}}h_1$. We then have $f_1 {\leq_{\mathsf{proc}}}h_1 {\leq_{\mathsf{proc}}}g_1$, and $M,h_1 \models {\mathop{\langle \pi_1^{-1} \rangle}}$. By induction hypothesis, $M,e,h_1 \models \pi_1$. Hence, $M,e,h_2 \models \pi_1\pi_2$.

\(e) at (0,0) ; (h1) at (0,2) ; (h2) at (0,4) ; (f1) at (-3,2) ; (g1) at (3,2) ;

(f2) at (-5.5,4) ; (g2) at (5.5,4) ;

(max) at (-2.5,4) ; (min) at (2.5,4) ;

(leproc) at (-1.5,2) [${\leq_{\mathsf{proc}}}$]{}; (leproc) at (1.5,2) [${\leq_{\mathsf{proc}}}$]{}; (leproc) at (-1,4) [${<_{\mathsf{proc}}}$]{}; (leproc) at (1,4) [${<_{\mathsf{proc}}}$]{}; (leproc) at (-4,4) [${\leq_{\mathsf{proc}}}$]{}; (leproc) at (4,4) [${\leq_{\mathsf{proc}}}$]{};

\(e) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2,bend left=0\] node\[left\] [$\pi_1$   ]{} (f1) (e) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2,bend left=-0\] node\[right\] [   $\pi_1$]{} (g1) (h1) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2,bend left=0\] node\[right\] [ $\pi_1^{-1}$]{} (e) (h2) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2,bend left=0\] node\[right\] [ $\pi_2^{-1}$]{} (h1) (f1) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2,bend left=0\] node\[right\] [ $\pi_2$]{} (max) (g1) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2,bend left=0\] node\[left\] [$\pi_2$  ]{} (min) (f1) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2,bend left=0\] node\[left\] [$\pi_2$  ]{} (f2) (g1) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2,bend left=0\] node\[right\] [  $\pi_2$]{} (g2);

Using Lemma \[lem:image\], we can give a characterization of ${\llbracket {{{\pi}^{\mathsf{c}}}} \rrbracket} (e)$ (when $\pi \in {{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$) that also relies on intervals delimited by ${\min {\llbracket {\pi} \rrbracket} (e)}$ and ${\max {\llbracket {\pi} \rrbracket} (e)}$. More precisely, ${\llbracket {{{\pi}^{\mathsf{c}}}} \rrbracket} (e)$ is the union of the following sets (see Figure \[fig:charcompl\]): (i) the interval of all events to the left of ${\min {\llbracket {\pi} \rrbracket} (e)}$, (ii) the interval of all events to the right of ${\max {\llbracket {\pi} \rrbracket} (e)}$, (iii) the set of events located between ${\min {\llbracket {\pi} \rrbracket} (e)}$ and ${\max {\llbracket {\pi} \rrbracket} (e)}$ and satisfying $\lnot {\mathop{\langle \pi^{-1} \rangle}}$, (iv) all events located on other processes than ${\min {\llbracket {\pi} \rrbracket} (e)}$ and ${\max {\llbracket {\pi} \rrbracket} (e)}$.

\(e) at (3,-2) ;

iin [0,1,3,6]{} [ (ei) at (1.3\*i,0) ; ]{} (e) edge\[decorate,decoration=[snake,post length=0.7mm,amplitude=0.4mm]{}\] node\[below left\] [${{\mathsf{min}~} {\pi}}$]{} (e0) (e) edge\[decorate,decoration=[snake,post length=0.7mm,amplitude=0.4mm]{}\] node\[below right\] [${{\mathsf{max}~} {\pi}}$]{} (e6) ;

iin [-1,2,4,5,7,8]{} [ (ei) at (1.3\*i,0) ; ]{} i\[evaluate=ias using int(i+1)\] in [-1,...,7]{} [ (ei) – (e) ; ]{}

[background]{} at (e-1) ;

at (e2) ; ($(e4)+(-0.4,0.4)$) rectangle ($(e5)+(0.4,-0.4)$) ; ;

($(e7)+(-0.4,0.4)$) rectangle ($(e8)+(0.4,-0.4)$) ; ;

This description of ${\llbracket {{{\pi}^{\mathsf{c}}}} \rrbracket} (e)$ can be used to rewrite ${{\pi}^{\mathsf{c}}}$ as a union of ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ formulas. In a first step, we show that, if $\pi$ is a ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ formula, then the relation $\{(e,{\min {\llbracket {\pi} \rrbracket} (e)})\}$ can also be expressed in ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ (and similarly for $\max$).

Let $R = \emptyset$ or $R = \{{\mathsf{Loop}}\}$. For every path formula $\pi \in {{\textup{PDL}_{\mathsf{sf}}}}[R]$, there exist ${{\textup{PDL}_{\mathsf{sf}}}}[R]$ path formulas ${{\mathsf{min}~} {\pi}}$ and ${{\mathsf{max}~} {\pi}}$ such that $M,e,f \models {{\mathsf{min}~} {\pi}}$ iff $f = {\min {\llbracket {\pi} \rrbracket} (e)}$, and $M,e,f \models {{\mathsf{max}~} {\pi}}$ iff $f = {\max {\llbracket {\pi} \rrbracket} (e)}$.

We construct, by induction on $\pi$, formulas ${{\mathsf{min}~} {(\pi \cdot{\{\psi\}?})}}$ for all ${{\textup{PDL}_{\mathsf{sf}}}}[R]$ event formulas $\psi$. For $\pi \in \{ {{\rightarrow}}, {{\leftarrow}}, {{\lhd}_{p,q}}, {{\lhd}^{-1}_{p,q}},
  {\{\varphi\}?}\}$, we let ${{\mathsf{min}~} {(\pi \cdot{\{\psi\}?})}} = \pi \cdot{\{\psi\}?}$. Then, $$\begin{aligned}
    {{\mathsf{min}~} {({{\xrightarrow{\varphi}}} \cdot{\{\psi\}?})}}
    & = {{\xrightarrow{\varphi \land \lnot \psi}}} \cdot{\{\psi\}?} \\
    {{\mathsf{min}~} {({{\xleftarrow{\varphi}}} \cdot{\{\psi\}?})}}
    & = {{\xleftarrow{\varphi}}}\cdot {\{\psi \land (\lnot \varphi \lor \lnot
      {\mathop{\langle {\xleftarrow{\varphi}} \rangle} {\psi}}) \}?} \\
    {{\mathsf{min}~} {({\mathsf{jump}_{p,q}} \cdot{\{\psi\}?})}}
    & = {\mathsf{jump}_{p,q}} \cdot{\{\psi \land \lnot {\mathop{\langle {\xleftarrow{+}}\rangle} {\psi}}\}?} \\
    {{\mathsf{min}~} {(\pi_1\cdot\pi_2 \cdot{\{\psi\}?})}}
    & = {{\mathsf{min}~} {(\pi_1 \cdot{\{{\mathop{\langle \pi_2 \rangle} {\psi}}\}?})}}
      \cdot {{\mathsf{min}~} {(\pi_2 \cdot{\{\psi\}?})}} \, .
  \end{aligned}$$ The construction of ${{\mathsf{max}~} {\pi}}$ is similar.

We are now ready to prove that any boolean combination of ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ formulas is equivalent to a positive one, i.e., one that does not use complement.

\[lem:closure-complement\] For all path formulas $\pi \in {{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$, there exist ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ path formulas $(\pi_i)_{1 \le i \le |{P}|^2+3}$ such that ${{\pi}^{\mathsf{c}}} \equiv \bigcup_{1 \le i \le |{P}|^2+3} \pi_i$.

We show ${{\pi}^{\mathsf{c}}} \equiv \sigma$, where $$\sigma = ({{\mathsf{min}~} {\pi}} \cdot {{\xleftarrow{+}}}) \cup ({{\mathsf{max}~} {\pi}} \cdot {{\xrightarrow{+}}}) 
  \cup ( \pi \cdot {{\xrightarrow{+}}} \cdot {\{\neg{\mathop{\langle \pi^{-1} \rangle}}\}?}) 
  \cup \bigcup_{(p,q) \in {P}^2} {\{\lnot{\mathop{\langle \pi \rangle} {q}}\}?} \cdot {\mathsf{jump}_{p,q}} \,.$$

Let $M = (E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ be an MSC and $e,f \in E$. We write $p = {\mathit{loc}}(e)$, $q = {\mathit{loc}}(f)$. Let us show that $M,e,f \models \pi^c$ iff $M,e,f \models \sigma$. If $M,e \models \lnot{\mathop{\langle \pi \rangle} {q}}$, then both $M,e,f \models {{\pi}^{\mathsf{c}}}$ and $M,e,f \models \sigma$ hold. In the following, we assume that $M,e \models {\mathop{\langle \pi \rangle} {q}}$, and thus that ${\min {\llbracket {\pi} \rrbracket} (e)}$ and ${\max {\llbracket {\pi} \rrbracket} (e)}$ are well-defined and on process $q$. Again, if $f {<_{\mathsf{proc}}}{\min {\llbracket {\pi} \rrbracket} (e)}$ or ${\max {\llbracket {\pi} \rrbracket} (e)} {<_{\mathsf{proc}}}f$, then both $M,e,f \models {{\pi}^{\mathsf{c}}}$ and $M,e,f \models \sigma$ hold. And if ${\min {\llbracket {\pi} \rrbracket} (e)} {\leq_{\mathsf{proc}}}f {\leq_{\mathsf{proc}}}{\max {\llbracket {\pi} \rrbracket} (e)}$, then, by Lemma \[lem:image\], we have $M,e,f \models \pi^c$ iff $M,f \models \lnot{\mathop{\langle \pi^{-1} \rangle}}$, iff $M,e,f \models \sigma$.

The rest of this section is dedicated to the proof of Theorem \[thm:FO-to-PDLm-main\], stating that every ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ formula with at most two free variables can be translated into an equivalent ${{{\textup{PDL}_{\mathsf{sf}}}}}$ formula. As we proceed by induction, we actually need a more general statement, which takes into account arbitrarily many free variables:

\[thm:FO-to-PDLm\] Every formula $\Phi\in {{\textup{FO}}[{\rightarrow},{\lhd},\le]}$ with at least one free variable is equivalent to a boolean combination of formulas of the form ${\widetilde{\pi}}(x,y)$, where $\pi \in {{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}$ and $x,y \in {\mathsf{Free}}(\Phi)$.

In the following, we will simply write $\pi(x,y)$ for ${\widetilde{\pi}}(x,y)$, where ${\widetilde{\pi}}(x,y)$ is the ${\textup{FO}}$ formula equivalent to $\pi$ as defined in Proposition \[prop:pdl-fo3\]. The proof is by induction. For convenience, we assume that $\Phi$ is in prenex normal form. If $\Phi$ is quantifier free, then it is a boolean combination of atomic formulas. For $x,y \in {\mathcal{V}_{\mathsf{event}}}$, atomic formulas are translated as follows: $$\begin{array}{rclcrclcrcl}
        p(x) & \equiv & {\{p\}?} (x,x)
        & \qquad\qquad & x {\rightarrow}y & \equiv & {{\rightarrow}}(x,y)
        & & x = y & \equiv & {\{{\mathit{true}}\}?}(x,y)\\[1.5ex]
        a(x) & \equiv & {\{a\}?} (x,x)
        & & x {\lhd}y & \equiv &
        \displaystyle \bigvee_{(p,q) \in {\mathit{Ch}}} {{\lhd}_{p,q}}(x,y)
      \end{array}$$ Moreover, $x \le y$ is equivalent to the disjunction of the formulas $\bigl(\pi \cdot {{\lhd}_{p_1,p_2}} \cdot {{\xrightarrow{+}}} \cdot {{\lhd}_{p_2,p_3}}
        \cdots {{\xrightarrow{+}}} \cdot {{\lhd}_{p_{m-1},p_{m}}} \cdot \pi'\bigr)(x,y)$, where $1 \le m \le |{P}|$, $p_1,\ldots,p_m \in {P}$ are such that $p_i 
\neq p_{j}$ for all $1\leq i<j\leq m$, and $\pi,\pi' \in \{{\xrightarrow{+}},{\{{\mathit{true}}\}?}\}$.

#### Universal quantification.

We have $\forall x.\Psi \equiv 
  \neg\exists x.\neg\Psi$. Since we allow boolean combinations, dealing with negation is trivial. Hence, this case reduces to existential quantification.

#### Existential quantification.

Suppose that $\Phi = \exists x.\Psi$. If $x$ is not free in $\Psi$, then $\Phi\equiv\Psi$ and we are done by induction. Otherwise, assume that ${\mathsf{Free}}(\Psi)=\{x_1,\ldots,x_n\}$ with $n>1$ and that $x=x_n$. By induction, $\Psi$ is equivalent to a boolean combination of formulas of the form $\pi(y,z)$ with $y,z\in{\mathsf{Free}}(\Psi)$. We transform it into a finite disjunction of formulas of the form $\bigwedge_{j} \pi_{j}(y_{j},z_{j})$, where $y_j = x_{i_1}$ and $z_j =
  x_{i_2}$ for some $i_1 \le i_2$. To do so, we first eliminate negation using Lemma \[lem:closure-complement\]. The resulting positive boolean combination is then brought into disjunctive normal form. Note that this latter step may cause an exponential blow-up so that the overall construction is nonelementary (which is unavoidable [@phd-stockmeyer]). Finally, the variable ordering can be guaranteed by replacing $\pi_j$ with $\pi_j^{-1}$ whenever needed.

Now, $\Phi=\exists x_n.\Psi$ is equivalent to a finite disjunction of formulas of the form $$\bigwedge_{j \in I} \pi_{j} (y_{j},z_{j})
      ~\land~ {  \begin{array}[t]{@{}c@{}}
  \underbrace{\exists x_n. \Bigl(\bigwedge_{j \in J} \pi_{j} (y_{j},x_n) \land
      \bigwedge_{j \in J'} \pi_{j} (x_n,x_n)\Bigr)}\\
  =: \Upsilon
  \end{array}
}$$ for three finite, pairwise disjoint index sets $I,J,J'$ such that $y_j \in
  \{x_1,\ldots,x_{n-1}\}$ for all $j \in I \cup J$, and $z_j \in
  \{x_1,\ldots,x_{n-1}\}$ for all $j \in I$. Notice that ${\mathsf{Free}}(\Upsilon)\subseteq\{x_1,\ldots,x_{n-1}\}$. If $J = \emptyset$, then[^3] $$\Upsilon \equiv \bigvee_{p,q \in P}
  \Big( {\mathsf{jump}_{p,q}} \cdot {\{\bigwedge_{j \in J'} {\mathsf{Loop}(\pi_{j})}\}?}
  \cdot {\mathsf{jump}_{q,p}}\Big) (x_1,x_1) \, .$$ So assume $J \neq \emptyset$. Set $$\Upsilon' {:=}\bigvee_{k,\ell \in J}
      \left(\begin{array}{rl}
      & \bigwedge_{j \in J} (({{\mathsf{min}~} {\pi_{j}}}) \cdot {{\xrightarrow{\ast}}} \cdot
      ({{\mathsf{min}~} {\pi_{k}}})^{-1}) (y_{j},y_{k})
      \\ \land & \bigwedge_{j \in J} (({{\mathsf{max}~} {\pi_{\ell}}}) \cdot {{\xrightarrow{\ast}}}
      \cdot ({{\mathsf{max}~} {\pi_{j}}})^{-1}) (y_{\ell},y_{j})\\
      \land &
      (\pi_{k} \cdot {\{\psi\}?} \cdot \pi_{\ell}^{-1}) (y_{k},y_{\ell})
      \end{array}\right)$$ where $ \psi = \bigwedge_{j \in J} {\mathop{\langle \pi_{j}^{-1} \rangle}}
  \land \bigwedge_{j \in J'} {\mathsf{Loop}(\pi_{j})}$. We have ${\mathsf{Free}}(\Upsilon')={\mathsf{Free}}(\Upsilon)\subseteq\{x_1,\ldots,x_{n-1}\}$.

\[claim:fo-pdl\] We have $\Upsilon \equiv \Upsilon'$.

Intuitively, by Lemma \[lem:image\], we know that $\Upsilon$ holds iff the intersection of the intervals $[{\min {\llbracket {\pi_j} \rrbracket} (y_j)}, {\max {\llbracket {\pi_j} \rrbracket} (y_j)}]$ contains some event satisfying $\psi$. The formula $\Upsilon'$ identifies some $\pi_k$ such that ${\min {\llbracket {\pi_k} \rrbracket} (y_k)}$ is maximal (first line), some $\pi_\ell$ such that ${\max {\llbracket {\pi_\ell} \rrbracket} (y_\ell)}$ is minimal (second line), and tests that there exists an event $x_n$ satisfying $\psi$ between the two (third line). This is illustrated in Figure \[fig:fo-pdl\].

(xj) at (0,-1) ; (xj1) at (-1.5,0) ; (xj2) at (1,0) ; (xj) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[left,pos=0.4,xshift=-2pt\] [${{\mathsf{min}~} {\pi_j}}$]{} (xj1) (xj) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[right,pos=0.4,xshift=5pt\] [${{\mathsf{max}~} {\pi_j}}$]{} (xj2) ; (xj1) – (xj2);

\(xl) at (-1.5,1) ; (xl1) at (-1,0) ; (xl2) at (0.5,0) ; (xl) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[left,pos=0.5\] [${{\mathsf{min}~} {\pi_\ell}}$]{} (xl1) (xl) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[right,pos=0.1,xshift=5pt\] [${{\mathsf{max}~} {\pi_\ell}}$]{} (xl2) ;

(xk) at (1.5,1) ; (xk1) at (-0.5,0) ; (xk2) at (2,0) ; (xk) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[left,pos=0.1,yshift=5pt\] [${{\mathsf{min}~} {\pi_k}}$]{} (xk1) (xk) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[right\] [${{\mathsf{max}~} {\pi_k}}$]{} (xk2) ;

(xk1) edge\[thick\] node\[below\] [$x_n$]{} (xl2);

We give now the formal proof of Claim \[claim:fo-pdl\]. Assume $M,\nu \models \Upsilon$. There exists $e \in E$ such that for all $j \in J$, $M,\nu(y_{j}),e \models \pi_{j}$, and for all $j \in J'$, $M,e \models {\mathsf{Loop}(\pi_j)}$. In particular, all ${\min {\llbracket {\pi_{j}} \rrbracket} (\nu(y_{j}))}$ and ${\max {\llbracket {\pi_{j}} \rrbracket} (\nu(y_{j}))}$ for $j \in J$ are well-defined and on process ${\mathsf{proc}}(e)$. Let $k \in J$ such that ${\min {\llbracket {\pi_{k}} \rrbracket} (\nu(y_{k}))}$ is maximal, i.e., ${\min {\llbracket {\pi_{j}} \rrbracket} (\nu(y_{j}))} {\leq_{\mathsf{proc}}}{\min {\llbracket {\pi_{k}} \rrbracket} (\nu(y_{k}))}$ for all $j \in J$. Then, for all $j \in J$, we have $M,\nu(y_{j}),\nu(y_{k}) \models
  ({{\mathsf{min}~} {\pi_{j}}}) \cdot {{\xrightarrow{\ast}}} \cdot ({{\mathsf{min}~} {\pi_{k}}})^{-1}$. Similarly, let $\ell \in J$ such that ${\max {\llbracket {\pi_{\ell}} \rrbracket} (\nu(y_{\ell}))}$ is minimal. Then, for all $j \in J$, $M,\nu(y_{\ell}),\nu(y_{j})
  \models ({{\mathsf{max}~} {\pi_{\ell}}}) \cdot {{\xrightarrow{\ast}}} \cdot
  ({{\mathsf{max}~} {\pi_{j}}})^{-1}$. In addition, we have $M,e \models \psi$, $M,\nu(y_{k}),e \models \pi_{k}$, and $M,e,\nu(y_{\ell}), \models \pi_{\ell}^{-1}$, hence $M,\nu(y_{k}),\nu(y_{\ell}) \models
  \pi_{k} \cdot {\{\psi\}?} \cdot \pi_{\ell}^{-1}$. So we have $M,\nu \models \Upsilon'$.

Conversely, assume $M,\nu \models \Upsilon'$. Let $k,\ell \in J$ such that the corresponding sub-formula is satisfied. There exists $e \in E$ such that $M,\nu(y_{k}),e \models \pi_{k}$, $M,e \models \psi$, and $M,e,\nu(y_{\ell}) \models \pi_{\ell}^{-1}$. Note that we have ${\min {\llbracket {\pi_{k}} \rrbracket} (\nu(y_{k}))} {\leq_{\mathsf{proc}}}e {\leq_{\mathsf{proc}}}{\max {\llbracket {\pi_{\ell}} \rrbracket} (\nu(y_{\ell}))}$. For all $j \in J'$, we have $M,e \models {\mathsf{Loop}(\pi_{j})}$, i.e., $M,\nu[x \mapsto e] \models \pi_{j}(x_{n},x_n)$. Now, let $j \in J$. We have $M,\nu(y_{j}),\nu(y_{k}) \models
  ({{\mathsf{min}~} {\pi_{j}}}) \cdot {{\xrightarrow{\ast}}} \cdot ({{\mathsf{min}~} {\pi_{k}}})^{-1}$, hence ${\min {\llbracket {\pi_{j}} \rrbracket} (\nu(y_{j}))} {\leq_{\mathsf{proc}}}{\min {\llbracket {\pi_{k}} \rrbracket} (\nu(y_{k}))} {\leq_{\mathsf{proc}}}e$. Similarly, $M,\nu(y_{\ell}),\nu(y_{j}) \models ({{\mathsf{max}~} {\pi_{\ell}}}) \cdot
  {{\xrightarrow{\ast}}} \cdot ({{\mathsf{max}~} {\pi_{j}}})^{-1}$, hence $e {\leq_{\mathsf{proc}}}{\max {\llbracket {\pi_{\ell}} \rrbracket} (\nu(y_{\ell}))} {\leq_{\mathsf{proc}}}{\max {\llbracket {\pi_{j}} \rrbracket} (\nu(y_{j}))}$. In addition, since $M,e \models \psi$, we have $M,e \models {\mathop{\langle \pi_{j}^{-1} \rangle}}$. Applying Lemma \[lem:image\], we get $M,\nu(y_{j}),e \models \pi_{j}$, i.e., $M,\nu[x \mapsto e] \models \pi_j(y_j,x_n)$. Hence, $M,\nu \models \Upsilon$. This concludes the proof of Claim \[claim:fo-pdl\].

Thus, $\Upsilon$ is equivalent to some positive combination of formulas $\pi(x,y)$ with $\pi \in {{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ and $x,y\in\{x_1,\ldots,x_{n-1}\}={\mathsf{Free}}(\Phi)$, therefore, so is $\Phi$. Note that the two formulas $\bigl(({{\mathsf{min}~} {\pi_{j}}}) \cdot {{\xrightarrow{\ast}}} \cdot
  ({{\mathsf{min}~} {\pi_{k}}})^{-1}\bigr) (y_{j},y_{k})$ and $\bigl(({{\mathsf{max}~} {\pi_{\ell}}}) \cdot {{\xrightarrow{\ast}}}
  \cdot ({{\mathsf{max}~} {\pi_{j}}})^{-1}\bigr) (y_{\ell},y_{j})$ are not ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ formulas (since ${\xrightarrow{\ast}}$ is not). However, they are disjunctions of ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ formulas, for instance, $\bigl(({{\mathsf{min}~} {\pi_{j}}}) \cdot {{\xrightarrow{\ast}}} \cdot
  ({{\mathsf{min}~} {\pi_{k}}})^{-1}\bigr) (y_{j},y_{k}) \equiv
  \bigl(({{\mathsf{min}~} {\pi_{j}}}) \cdot ({{\mathsf{min}~} {\pi_{k}}})^{-1}\bigr) (y_{j},y_{k})
  \lor \bigl(({{\mathsf{min}~} {\pi_{j}}}) \cdot {{\xrightarrow{+}}} \cdot
  ({{\mathsf{min}~} {\pi_{k}}})^{-1}\bigr) (y_{j},y_{k})$.

We are now able to prove the main result relating ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ and ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$.

Let $\Phi_2(x_1,x_2)$ be an ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ formula with two free variables. We apply Proposition \[thm:FO-to-PDLm\] to $\Phi_2(x_1,x_2)$ and obtain a boolean combination of path formulas $\pi(y,z)$ with $y,z\in\{x_1,x_2\}$. First, we bring it into a positive boolean combination using Lemma \[lem:closure-complement\]. Next, we replace formulas $\pi(x_1,x_1)$ with $\bigvee_{p,q} ({\{{\mathsf{Loop}(\pi)}\}?}\cdot{\mathsf{jump}_{p,q}})(x_1,x_2)$. Similarly, $\pi(x_2,x_2)$ is replaced with $\bigvee_{p,q}
  ({\mathsf{jump}_{p,q}}\cdot{\{{\mathsf{Loop}(\pi)}\}?})(x_1,x_2)$. Also, $\pi(x_2,x_1)$ is replaced with $\pi^{-1}(x_1,x_2)$. Finally, we transform it into disjunctive normal form: we obtain $\Phi_1(x_1,x_2)\equiv\bigvee_{i}\bigwedge_{j} 
  \pi_{ij}(x_1,x_2)$, which concludes the proof in the case of two free variables.

Next, let $\Phi_1(x)$ be an ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ formula with one free variable. As above, applying Proposition \[thm:FO-to-PDLm\] to $\Phi_1(x)$ and then Lemma \[lem:closure-complement\], we obtain ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ path formulas $\pi_{ij}$ such that $\Phi_1(x) \equiv  \bigvee_i \bigwedge_j \pi_{ij}(x,x)$. Now, $M,[x \mapsto e] \models \pi_{ij}(x,x)$ iff $M,e \models {\mathsf{Loop}(\pi_{ij})}$. Hence, $\Phi(x) \equiv \bigvee_i \bigwedge_j {\mathsf{Loop}(\pi_{ij})}$.

Finally, an ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ sentence $\Phi_0$ is a boolean combination of formulas of the form $\exists x.\Phi_1(x)$. Applying the theorem to $\Phi_1(x)$, we obtain an equivalent ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ event formula $\varphi$. Then, we take ${\xi}={\mathop{\mathsf{E}\vphantom{a}}\nolimits}\varphi$, which is trivially equivalent to $\exists x.\Phi_1(x)$.

From $\boldsymbol{{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ to CFMs {#sec:pdl-cfm}
===========================================================================

In the inductive translation of ${{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}$ formulas into CFMs, *event* formulas will be evaluated by *MSC transducers*. An MSC transducer for a formula $\varphi$ produces a truth value at every event on the given MSC. More precisely, it outputs $1$ when $\varphi$ holds, and $0$ otherwise. We will first introduce MSC transducers formally and then go into the actual translation.

Letter-to-letter MSC Transducers
--------------------------------

Let $\Gamma$ be a nonempty finite output alphabet. A *(nondeterministic) letter-to-letter MSC transducer* (or simply, *transducer*) ${\mathcal{A}}$ over ${P}$ and from $\Sigma$ to $\Gamma$ is a CFM over ${P}$ and $\Sigma \times \Gamma$. The transducer ${\mathcal{A}}$ accepts the relation ${\llbracket {\mathcal{A}}\rrbracket} = \{\bigl((E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda),(E,{\rightarrow},{\lhd},{\mathit{loc}},\gamma)\bigr)
\mid {(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda\times\gamma)} \in {\mathbb{L}}({\mathcal{A}})\}$. Transducers are closed under product and composition, using standard constructions:

Let ${\mathcal{A}}$ be a transducer from $\Sigma$ to $\Gamma$, and ${\mathcal{A}}'$ a transducer from $\Sigma$ to $\Gamma'$. There exists a transducer ${\mathcal{A}}\times {\mathcal{A}}'$ from $\Sigma$ to $\Gamma \times \Gamma'$ such that $$\begin{aligned}
    {\llbracket {\mathcal{A}}\times {\mathcal{A}}' \rrbracket}
    & = \big\{
      \big((E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda),
      (E,{\rightarrow},{\lhd},{\mathit{loc}},\gamma \times \gamma')\big)
      \mid {} \\
    & \hspace{5em}
      \big((E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda),(E,{\rightarrow},{\lhd},{\mathit{loc}},\gamma)\big)
      \in {\llbracket {\mathcal{A}}\rrbracket}, \\
    & \hspace{5em}
      \big((E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda),(E,{\rightarrow},{\lhd},{\mathit{loc}},\gamma')\big)
      \in {\llbracket {\mathcal{A}}' \rrbracket}
      \big\} \, .
  \end{aligned}$$

Let ${\mathcal{A}}$ be a transducer from $\Sigma$ to $\Gamma$, and ${\mathcal{A}}'$ a transducer from $\Gamma$ to $\Gamma'$. There exists a transducer ${\mathcal{A}}' \circ {\mathcal{A}}$ from $\Sigma$ to $\Gamma'$ such that $${\llbracket {\mathcal{A}}' \circ {\mathcal{A}}\rrbracket} = {\llbracket {\mathcal{A}}' \rrbracket} \circ {\llbracket {\mathcal{A}}\rrbracket} =
    \{ (M,M'') \mid \exists M' \in {\mathbb{MSC}({P},\Gamma)} :
    (M,M') \in {\llbracket {\mathcal{A}}\rrbracket}, (M',M'') \in {\llbracket {\mathcal{A}}' \rrbracket} \} \, .$$

Translation of $\boldsymbol{{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ Event Formulas into CFMs
------------------------------------------------------------------------------------------------------

For a ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ event formula $\varphi$ and an MSC $M = (E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ over ${P}$ and $\Sigma$, we define an MSC ${{M}_{\varphi}} = (E,{\rightarrow},{\lhd},{\mathit{loc}},\gamma)$ over ${P}$ and $\{0,1\}$, by setting $\gamma(e) = 1$ if $M,e \models \varphi$, and $\gamma(e) = 0$ otherwise. Our goal is to construct a transducer ${{\mathcal{A}}_{\varphi}}$ such that ${\llbracket {{\mathcal{A}}_{\varphi}} \rrbracket} = \{(M,{{M}_{\varphi}}) \mid M \in {\mathbb{MSC}({P},\Sigma)}\}$.

We start with the case of formulas from ${\textup{PDL}_{\mathsf{sf}}}[\emptyset]$, i.e., without ${\mathsf{Loop}}$.

\[lem:trad-loop-free\] Let $\varphi$ be a ${\textup{PDL}_{\mathsf{sf}}}[\emptyset]$ event formula. There exists a transducer ${{\mathcal{A}}_{\varphi}}$ such that ${\llbracket {{\mathcal{A}}_{\varphi}} \rrbracket} = \{(M,{{M}_{\varphi}}) \mid M \in {\mathbb{MSC}({P},\Sigma)}\}$.

Any ${{{\textup{PDL}_{\mathsf{sf}}}}}[\emptyset]$ event formula is equivalent to some formula $\varphi$ over the syntax $$\varphi ::= p \mid a \mid \varphi \lor \varphi \mid \lnot \varphi \mid
    {\mathop{\langle {\lhd}_{p,q} \rangle} {\varphi}} \mid {\mathop{\langle {\lhd}_{p,q}^{-1} \rangle} {\varphi}}
    \mid {\mathop{\langle {\xrightarrow{\varphi}} \rangle} {\varphi}}
    \mid {\mathop{\langle {\xleftarrow{\varphi}} \rangle} {\varphi}}
    \mid {\mathop{\langle {\mathsf{jump}_{p,q}} \rangle} {\varphi}}$$ Indeed, we have ${\mathop{\langle \pi_1 \cdot \pi_2 \rangle} {\varphi}} \equiv
  {\mathop{\langle \pi_1 \rangle} {({\mathop{\langle \pi_2 \rangle} {\varphi}})}}$, and ${\mathop{\langle {\{\varphi\}?} \rangle} {\psi}} \equiv \varphi \land \psi$. Notice that ${{\rightarrow}}\equiv{{\xrightarrow{{\mathit{false}}}}}$ and ${{\leftarrow}}\equiv{{\xleftarrow{{\mathit{false}}}}}$.

It is easy to define ${\mathcal{A}}_\varphi$ for formulas $\varphi = p$, with $p \in P$, or $\varphi = a$, with $a \in \Sigma$. We also use below simple transducers over $P$ from $\{0,1\}^2$ or $\{0,1\}$ to $\{0,1\}$. For instance, the transducer ${\mathcal{B}}_{\neg}$ from $\{0,1\}$ to $\{0,1\}$ outputs the negation of the bit read and ${\mathcal{B}}_{\vee}$ from $\{0,1\}^{2}$ to $\{0,1\}$ outputs the disjunction of the two bits read. The transducer ${\mathcal{B}}_{{\lhd}_{p,q}}$ from $\{0,1\}$ to $\{0,1\}$ outputs 1 at an event $e$ iff $e$ is a send event from $p$ to $q$ and the corresponding receive event $f$ is labeled 1. To do so, at each send event $e$ from $p$ to $q$, the transducer guesses whether the corresponding receive event $f$ is labeled $0$ or 1, outputs its guess and sends it on the message from $e$ to $f$. At the receive event $f$ the transducer checks that the guess was correct. The run is accepting if all guesses were correct. The deterministic transducer ${\mathcal{B}}_{\mathsf{YS}}$ from $\{0,1\}^{2}$ to $\{0,1\}$ corresponds to the *strict since* modality. On each process, it runs the automaton given in Figure \[fig:YS\]: it outputs 1 at some event $e$ if there is $g{<_{\mathsf{proc}}}e$ where the second bit is 1 and for all $g{<_{\mathsf{proc}}}f{<_{\mathsf{proc}}}e$ the first bit at $f$ is 1. Similarly, we can construct the nondeterministic transducer ${\mathcal{B}}_{\mathsf{XU}}$ for the *strict until*. Finally, it is easy to construct a transducer ${\mathcal{B}}_{{\mathsf{jump}_{p,q}}}$ which outputs 0 on all events of processes $r\neq p$ and outputs 1 (resp. 0) on all events of process $p$ iff some event (resp. no event) of process $q$ is labeled 1.

![Transducer for strict since. In a transition $a/b$, the input is $a$ and the output is $b$. Write and receive actions are omitted.[]{data-label="fig:YS"}](gpicture-pics.pdf)

We then let $$\begin{aligned}
    {\mathcal{A}}_{\varphi_1 \lor \varphi_2}
    & = {\mathcal{B}}_{\lor} \circ ({\mathcal{A}}_{\varphi_1} \times {\mathcal{A}}_{\varphi_2})
    & {\mathcal{A}}_{\lnot \varphi}
    & = {\mathcal{B}}_{\neg} \circ {\mathcal{A}}_{\varphi} \\
    {\mathcal{A}}_{{\mathop{\langle {\lhd}_{p,q} \rangle} {\varphi}}}
    & = {\mathcal{B}}_{{\lhd}_{p,q}} \circ {\mathcal{A}}_{\varphi}
    & {\mathcal{A}}_{{\mathop{\langle {\lhd}_{p,q}^{-1} \rangle} {\varphi}}}
    & = {\mathcal{B}}_{{\lhd}_{p,q}^{-1}} \circ {\mathcal{A}}_{\varphi} \\
    {\mathcal{A}}_{{\mathop{\langle {\xrightarrow{\varphi_1}} \rangle} {\varphi_2}}}
    & = {\mathcal{B}}_{\mathsf{XU}}
      \circ ({\mathcal{A}}_{\varphi_1} \times {\mathcal{A}}_{\varphi_2})
    & {\mathcal{A}}_{{\mathop{\langle {\mathsf{jump}_{p,q}} \rangle} {\varphi}}}
    & = {\mathcal{B}}_{{\mathsf{jump}_{p,q}}} \circ {\mathcal{A}}_{\varphi}\\
    {\mathcal{A}}_{{\mathop{\langle {\xleftarrow{\varphi_1}} \rangle} {\varphi_2}}}
    & = {\mathcal{B}}_{\mathsf{YS}}
      \circ ({\mathcal{A}}_{\varphi_1} \times {\mathcal{A}}_{\varphi_2}) \, . && \qedhere
  \end{aligned}$$

Next, we look at a single loop where the path $\pi \in {\textup{PDL}_{\mathsf{sf}}}[\emptyset]$ is of the form ${{\mathsf{min}~} {\pi'}}$ or ${{\mathsf{max}~} {\pi'}}$. This case will be simpler than general loop formulas, because of the fact that ${\llbracket {{{\mathsf{min}~} {\pi'}}} \rrbracket}(e)$ is always either empty or a singleton. Recall that, in addition, ${{\mathsf{min}~} {\pi'}}$ is monotone.

\[lem:det-loop\] Let $\pi$ be a ${{\textup{PDL}_{\mathsf{sf}}}}[\emptyset]$ path formula of the form $\pi = {{\mathsf{min}~} {\pi'}}$ or $\pi = {{\mathsf{max}~} {\pi'}}$, and let $\varphi = {\mathsf{Loop}(\pi)}$. There exists a transducer ${{\mathcal{A}}_{\varphi}}$ such that ${\llbracket {{\mathcal{A}}_{\varphi}} \rrbracket} =
  \{(M,{{M}_{\varphi}}) \mid M \in {\mathbb{MSC}({P},\Sigma)}\}$.

We can assume that ${\mathsf{Comp}(\pi)} \subseteq {\mathsf{id}}$. We define ${{\mathcal{A}}_{\varphi}}$ as the composition of three transducers that will guess and check the evaluation of $\varphi$. More precisely, ${{\mathcal{A}}_{\varphi}}$ will be obtained as an inverse projection $\alpha^{-1}$, followed by the intersection with an MSC language $K$, followed by a projection $\beta$.

We first enrich the labeling of the MSC with a color from $\Theta =
  \{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] circle (2.8pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] circle (2.8pt);
\end{tikzpicture}
}\}$. Intuitively, colors ${
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}$ and ${
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}$ will correspond to a guess that the formula $\varphi$ is satisfied, and colors ${
\begin{tikzpicture}
\filldraw[fill=white,draw=black] circle (2.8pt);
\end{tikzpicture}
}$ and ${
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] circle (2.8pt);
\end{tikzpicture}
}$ to a guess that the formula is not satisfied. Consider the projection $\alpha\colon{\mathbb{MSC}({P},\Sigma\times\Theta)}\to{\mathbb{MSC}({P},\Sigma)}$ which erases the color from the labeling. The inverse projection $\alpha^{-1}$ can be realized with a transducer ${\mathcal{A}}$, i.e., ${\llbracket {\mathcal{A}}\rrbracket}=\{(\alpha(M'),M')\mid M'\in{\mathbb{MSC}({P},\Sigma\times\Theta)}\}$.

Define the projection $\beta\colon{\mathbb{MSC}({P},\Sigma\times\Theta)}\to{\mathbb{MSC}({P},\{0,1\})}$ by $\beta((E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda\times\theta))=(E,{\rightarrow},{\lhd},{\mathit{loc}},\gamma)$, where $\gamma(e)=1$ if $\theta(e)\in\{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$, and $\gamma(e)=0$ otherwise. The projection $\beta$ can be realized with a transducer ${\mathcal{A}}''$: we have ${\llbracket {\mathcal{A}}'' \rrbracket}=\{(M',\beta(M'))\mid M'\in{\mathbb{MSC}({P},\Sigma\times\Theta)}\}$.

Finally, consider the language $K\subseteq{\mathbb{MSC}({P},\Sigma\times\Theta)}$ of MSCs $M'=(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda\times\theta)$ satisfying the following two conditions:

1.  Colors ${
    \begin{tikzpicture}
    \filldraw[fill=white,draw=black] rectangle (5pt,5pt);
    \end{tikzpicture}
    }$ and ${
    \begin{tikzpicture}
    \filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
    \end{tikzpicture}
    }$ alternate on each process $p\in {P}$: if $e_1 < \cdots < e_n$ are the events in $E_p \cap
        \theta^{-1}(\{{
    \begin{tikzpicture}
    \filldraw[fill=white,draw=black] rectangle (5pt,5pt);
    \end{tikzpicture}
    },{
    \begin{tikzpicture}
    \filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
    \end{tikzpicture}
    }\})$, then $\theta(e_i) = {
    \begin{tikzpicture}
    \filldraw[fill=white,draw=black] rectangle (5pt,5pt);
    \end{tikzpicture}
    }$ if $i$ is odd, and $\theta(e_i) = {
    \begin{tikzpicture}
    \filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
    \end{tikzpicture}
    }$ if $i$ is even.

2.  For all $e \in E$, $\theta(e)\in\{{
    \begin{tikzpicture}
    \filldraw[fill=white,draw=black] rectangle (5pt,5pt);
    \end{tikzpicture}
    },{
    \begin{tikzpicture}
    \filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
    \end{tikzpicture}
    }\}$ iff there exists $f \in E$ such that $M,e,f \models \pi$ and $\theta(e) = \theta(f)$.

The first property is trivial to check with a CFM. Using Lemma \[lem:trad-loop-free\], we show that the second property can also be checked with a CFM. First, from $\pi$ we construct a ${{\textup{PDL}_{\mathsf{sf}}}}[\emptyset]$ event formula $\psi$ over ${P}$ and $\Sigma \times \Theta$ such that, for all $M'= (E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda\times\theta)\in{\mathbb{MSC}({P},\Sigma\times\Theta)}$ and events $e \in E$, we have $M',e \models \psi$ iff the following holds: $\theta(e)\in\{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$ iff there is $f \in E$ such that $\alpha(M'),e,f \models \pi$ and $\theta(e) = \theta(f)$. Namely, we define $$\psi = ({
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\;\vee\; {
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}) \Longleftrightarrow
  \Bigl[\bigl( {{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}} \;\wedge {\mathop{\langle \hat\pi \rangle} {{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}}}\bigr) \vee
  \bigl( {{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}} \;\wedge {\mathop{\langle \hat\pi \rangle} {{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}}}\bigr)\Bigr]$$ where the state formula ${\mathit{col}}\in \{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$ is an abbreviation for $\bigvee_{a \in \Sigma} (a,{\mathit{col}})$ and $\hat\pi$ is obtained from $\pi$ by replacing state formulas $a$ with $\bigvee_{{\mathit{col}}\in \Theta} (a,{\mathit{col}})$. Now, the language for the second condition is $\{M' \in{\mathbb{MSC}({P},\Sigma\times\Theta)} \mid$ every event of $M'_\psi$ is labeled with $1\}$, for which we can easily give a CFM using the transducer ${{\mathcal{A}}_{\psi}}$ from $\Sigma \times \Theta$ to $\{0,1\}$ given by Lemma \[lem:trad-loop-free\].

We deduce that there is a transducer ${\mathcal{A}}'$ such that ${\llbracket {\mathcal{A}}' \rrbracket}=\{(M',M')\mid M'\in K\}$. We let ${{\mathcal{A}}_{\varphi}} = {\mathcal{A}}''\circ{\mathcal{A}}'\circ{\mathcal{A}}$. Notice that ${\llbracket {{\mathcal{A}}_{\varphi}} \rrbracket}=\{(\alpha(M'),\beta(M'))\mid M'\in K\}$. From the following two claims, we deduce immediately that ${\llbracket {{\mathcal{A}}_{\varphi}} \rrbracket}=\{(M,M_\varphi)\mid M\in{\mathbb{MSC}({P},\Sigma)}\}$.

\[cl:forest\] For all $M\in{\mathbb{MSC}({P},\Sigma)}$, there exists $M'\in K$ with $\alpha(M')=M$.

Let $M=(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)\in{\mathbb{MSC}({P},\Sigma)}$. Let $E_1=\{e \in E \mid M,e \models \varphi\}$ and $E_0=E\setminus E_1$. Consider the graph $G = (E, \{(e,f) \mid M,e,f \models \pi\})$. Since $\pi = {{\mathsf{min}~} {\pi'}}$ or $\pi = {{\mathsf{max}~} {\pi'}}$, every vertex has outdegree at most 1, and, by Lemma \[lem:monotone\], there are no cycles except for self-loops. So the restriction of $G$ to $E_0$ is a forest, and there exists a $2$-coloring $\chi \colon E_0 \to \{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] circle (2.8pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] circle (2.8pt);
\end{tikzpicture}
}\}$ such that, for all $e,f \in E_0$ with $M,e,f \models \pi$, we have $\chi(e) \neq \chi(f)$. This is illustrated in Figure \[fig:Gpi\]. Moreover, there exists $\theta \colon E \to \Theta$ such that $\theta(e) = \chi(e)$ for $e \in E_0$, and $\theta(e)\in\{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$ for $e \in E_1$ is such that Condition 1 of the definition of $K$ is satisfied. It is easy to see that Condition 2 is also satisfied. Indeed, if $\theta(e)\in\{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$, then $e\in E_1$ and $M,e,e\models\pi$. Now, if $\theta(e)\notin\{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$, then $e\in E_0$ and either $M,e\not\models{\mathop{\langle \pi \rangle}}$ or, by definition of $\theta$, we have $\theta(e)\neq\theta(f)$ for the unique $f$ such that $M,e,f\models\pi$. (Claim \[cl:forest\])

= \[white, draw=black, line width=0.5pt, fill, circle, inner sep=0, minimum size = 6pt\] = \[gray, draw=black, line width=0.5pt, circle, fill, inner sep=0, minimum size = 6pt\] = \[white, draw=black, line width=0.5pt, fill, rectangle, inner sep=0, minimum size = 6pt\] = \[gray, draw=black, line width=0.5pt, rectangle, fill, inner sep=0, minimum size = 6pt\]

(0.5,0) – (14.5,0); iin [3,4,6,7,13,14]{} [ (ei) at (i,0) ; ]{} iin [2,5,8,9,11,12]{} [ (ei) at (i,0) ; ]{} (e1) at (1,0) ; (e10) at (10,0) ;

(e1) edge\[loop above\] node [$\pi$]{} (e1) (e10) edge\[loop above\] node [$\pi$]{} (e10) (e2) edge\[bend left\] node [$\pi$]{} (e1) (e4) edge\[bend left\] node [$\pi$]{} (e2) (e3) edge\[bend right\] node\[above\] [$\pi$]{} (e2) (e11) edge\[bend left\] node [$\pi$]{} (e10) (e9) edge\[bend right\] node\[below\] [$\pi$]{} (e10) (e7) edge\[bend right\] node\[below\] [$\pi$]{} (e9) (e5) edge\[bend left\] node [$\pi$]{} (e6) (e6) edge\[bend left\] node [$\pi$]{} (e8) (e8) edge\[bend left\] node [$\pi$]{} (e10) (e12) edge\[bend left\] node [$\pi$]{} (e14);

\[cl:beta\] For all $M'\in K$, we have $\beta(M')=M_\varphi$, where $M=\alpha(M')$.

Let $M'=(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda\times\theta)\in K$ and $M=\alpha(M')$. Suppose towards a contradiction that $M_\varphi\neq\beta(M)=(E,{\rightarrow},{\lhd},{\mathit{loc}},\gamma)$. By Condition 2, for all $e \in E$ such that $\gamma(e) = 0$, we have $M,e \not\models \varphi$. So there exists $f_0 \in E$ such that $\gamma(f_0) = 1$ and $M,f_0 \not\models
  \varphi$. Notice that $\theta(f_0)\in\{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$. For all $i \in
  {\mathbb{N}}$, let $f_{i+1}$ be the unique event such that $M,f_i,f_{i+1} \models
  \pi$. Such an event exists by Condition 2, and is unique since $\pi = {{\mathsf{min}~} {\pi'}}$ or $\pi = {{\mathsf{max}~} {\pi'}}$. Note that, for all $i$, $\theta(f_{i+1}) =
  \theta(f_i) \in \{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$. Suppose $f_0 {<_{\mathsf{proc}}}f_1$ (the case $f_1 {<_{\mathsf{proc}}}f_0$ is similar). By Condition 1, there exists $g_0$ such that $f_0 {<_{\mathsf{proc}}}g_0 {<_{\mathsf{proc}}}f_1$ and $\{\theta(f_0),\theta(g_0)\}=\{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$. For an illustration, see Figure \[fig:beta\]. Again, for all $i \in
  {\mathbb{N}}$, let $g_{i+1}$ be the unique event such that $M,g_i,g_{i+1} \models
  \pi$. Note that all $f_0,f_1,\ldots$ have the same color, in $\{{
\begin{tikzpicture}
\filldraw[fill=white,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
},{
\begin{tikzpicture}
\filldraw[fill=gray!90,draw=black] rectangle (5pt,5pt);
\end{tikzpicture}
}\}$, and all $g_0,g_1,\ldots$ carry the complementary color. Thus, $f_i \neq g_j$ for all $i,j \in {\mathbb{N}}$. But, by Lemma \[lem:monotone\], this implies $f_0 {<_{\mathsf{proc}}}g_0
  {<_{\mathsf{proc}}}f_1 {<_{\mathsf{proc}}}g_1 {<_{\mathsf{proc}}}\cdots$, which contradicts the fact that we deal with finite MSCs. (Claim \[cl:beta\])

(0.5,0) – (14.5,0); iin [1,3,5,7,9,11,13]{} [ (ei) at (i,0) ; ]{} iin [2,4,6,8,10,12,14]{} [ (ei) at (i,0) ; ]{} (inf) at (15,0.8) [$\textcolor{red}\cdots$]{};

(f0) at (1,-0.5) [$f_0$]{}; (f1) at (5,-0.5) [$f_1$]{}; (f2) at (11,-0.5) [$f_2$]{}; (g0) at (2,-0.5) [$g_0$]{}; (g1) at (8,-0.5) [$g_1$]{}; (g2) at (14,-0.5) [$g_2$]{};

(e1) edge\[bend left\] node [$\pi$]{} (e5) (e2) edge\[bend left\] node [$\pi$]{} (e8) (e5) edge\[bend left\] node [$\pi$]{} (e11) (e8) edge\[bend left\] node [$\pi$]{} (e14) (e11) edge\[bend left\] node [$\pi$]{} (inf);

This concludes the proof of Lemma \[lem:det-loop\].

The general case is more complicated. We first show how to rewrite an arbitrary loop formula using loops on paths of the form ${{\mathsf{max}~} {\pi}}$ or $({{\mathsf{max}~} {\pi}})\cdot{{\xleftarrow{+}}}$. Intuitively, this means that loop formulas will only be used to test, given an event $e$ such that $e' = {\max {\llbracket {\pi} \rrbracket} (e)}$ is well-defined and on the same process as $e$, whether $e' {<_{\mathsf{proc}}}e$, $e' = e$, or $e {<_{\mathsf{proc}}}e'$. Indeed, we have $M,e \models {\mathsf{Loop}(({{\mathsf{max}~} {\pi}})\cdot{{\xleftarrow{+}}})}$ iff $e {<_{\mathsf{proc}}}{\max {\llbracket {\pi} \rrbracket} (e)}$.

\[lem:loops\] For all ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ path formulas $\pi$, $${\mathsf{Loop}(\pi)}
    \equiv {\mathsf{Loop}({{\mathsf{max}~} {\pi}})} \lor
      \left({{\mathop{\langle \pi^{-1} \rangle}}} \land {{\mathsf{Loop}(({{\mathsf{max}~} {\pi}}) \cdot {{\xleftarrow{+}}})}}
      \land {\lnot {\mathsf{Loop}(({{\mathsf{min}~} {\pi}}) \cdot {{\xleftarrow{+}}})}}\right)
      \, .$$

The result follows from Lemma \[lem:image\]. Indeed, if we have $M,e \models {\mathsf{Loop}(\pi)}$ and $M,e \not\models {\mathsf{Loop}({{\mathsf{max}~} {\pi}})}$, then ${\min {\llbracket {\pi} \rrbracket} (e)} {\leq_{\mathsf{proc}}}e {<_{\mathsf{proc}}}{\max {\llbracket {\pi} \rrbracket} (e)}$ and $M,e \models {\mathop{\langle \pi^{-1} \rangle}}$, hence $M,e \models {{\mathop{\langle \pi^{-1} \rangle}}}
  \land {{\mathsf{Loop}(({{\mathsf{max}~} {\pi}}) \cdot {{\xleftarrow{+}}})}}
  \land {\lnot {\mathsf{Loop}(({{\mathsf{min}~} {\pi}}) \cdot {{\xleftarrow{+}}})}}$. Conversely, if $M,e \models {\mathsf{Loop}({{\mathsf{max}~} {\pi}})}$, then $M,e \models {\mathsf{Loop}(\pi)}$, and if $M,e \models ({{\mathop{\langle \pi^{-1} \rangle}}}
  \land {{\mathsf{Loop}(({{\mathsf{max}~} {\pi}}) \cdot {{\xleftarrow{+}}})}}
  \land {\lnot {\mathsf{Loop}(({{\mathsf{min}~} {\pi}}) \cdot {{\xleftarrow{+}}})}})$, then $M,e \models {\mathop{\langle \pi^{-1} \rangle}}$ and ${\min {\llbracket {\pi} \rrbracket} (e)} {\leq_{\mathsf{proc}}}e
  {<_{\mathsf{proc}}}{\max {\llbracket {\pi} \rrbracket} (e)}$, hence $M,e,e \models \pi$, i.e., $M,e \models
  {\mathsf{Loop}(\pi)}$.

Notice that, since ${{\mathsf{min}~} {\pi}} \equiv {{\mathsf{max}~} {({{\mathsf{min}~} {\pi}})}}$, the formula ${\mathsf{Loop}(({{\mathsf{min}~} {\pi}}) \cdot {{\xleftarrow{+}}})}$ can also be seen as a special case of a ${\mathsf{Loop}(({{\mathsf{max}~} {\pi'}}) \cdot {{\xleftarrow{+}}})}$ formula.

\[thm:PDLp-to-CFM\] For all ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ event formulas $\varphi$, there exists a transducer ${{\mathcal{A}}_{\varphi}}$ such that ${\llbracket {{\mathcal{A}}_{\varphi}} \rrbracket} = \{(M,{{M}_{\varphi}}) \mid M \in {\mathbb{MSC}({P},\Sigma)}\}$.

By Lemma \[lem:loops\], we can assume that all loop subformulas in $\varphi$ are of the form ${\mathsf{Loop}(({{\mathsf{max}~} {\pi}})\cdot{{\xleftarrow{+}}})}$ or ${\mathsf{Loop}({{\mathsf{max}~} {\pi}})}$ (recall that ${{\mathsf{min}~} {\pi}} \equiv {{\mathsf{max}~} {({{\mathsf{min}~} {\pi}})}}$). We prove Theorem \[thm:PDLp-to-CFM\] by induction on the number of loop subformulas in $\varphi$. The base case is stated in Lemma \[lem:trad-loop-free\].

Let $\psi = {\mathsf{Loop}(\pi')}$ be a subformula of $\varphi$ such that $\pi'$ contains no loop subformulas and ${\mathsf{Comp}(\pi')} \subseteq {\mathsf{id}}$. Let us show that there exists ${{\mathcal{A}}_{\psi}}$ such that ${\llbracket {{\mathcal{A}}_{\psi}} \rrbracket} = \{(M,{{M}_{\psi}}) \mid M \in {\mathbb{MSC}({P},\Sigma)}\}$. If $\pi'={{\mathsf{max}~} {\pi}}$, then we apply Lemma \[lem:det-loop\]. Otherwise, $\pi'=({{\mathsf{max}~} {\pi}})\cdot{{\xleftarrow{+}}}$ for some ${{\textup{PDL}_{\mathsf{sf}}}}[\emptyset]$ path formula $\pi$. So we assume from now on that $\psi={\mathsf{Loop}(({{\mathsf{max}~} {\pi}})\cdot{{\xleftarrow{+}}})}$.

We start with some easy remarks. Let $p\in{P}$ be some process and $e\in E_p$. A necessary condition for $M,e\models\psi$ is that $M,e\models{\mathop{\langle \pi \rangle}}\wedge\neg{\mathsf{Loop}({{\mathsf{max}~} {\pi}})}$. Also, it is easy to see that $M,e\models{\mathsf{Loop}({{\mathsf{min}~} {({{\xrightarrow{+}}}\cdot\pi^{-1})}})}$ is a sufficient condition for $M,e\models\psi$.

We let $E_p^{\pi}$ be the set of events $e\in E_p$ satisfying ${\mathop{\langle \pi \rangle} {p}}$. For all $e\in
  E_p^{\pi}$, we let $e'={\llbracket {{{\mathsf{max}~} {\pi}}} \rrbracket}(e)\in E_p$. The transducer ${\mathcal{A}}_\psi$ will establish, for each $e\in E_p^{\pi}$, whether $e'{<_{\mathsf{proc}}}e$, $e'=e$, or $e {<_{\mathsf{proc}}}e'$, and it will output $1$ if $e {<_{\mathsf{proc}}}e'$, and $0$ otherwise. The case $e'=e$ means $M,e\models{\mathsf{Loop}({{\mathsf{max}~} {\pi}})}$ and can be checked with the help of Lemma \[lem:det-loop\]. So the difficulty is to distinguish between $e' {<_{\mathsf{proc}}}e$ and $e {<_{\mathsf{proc}}}e'$ when $M,e\models{\mathop{\langle \pi \rangle}}\wedge\neg{\mathsf{Loop}({{\mathsf{max}~} {\pi}})}$.

The following two claims rely on Lemma \[lem:monotone\]. Recall that $\psi={\mathsf{Loop}(({{\mathsf{max}~} {\pi}})\cdot{{\xleftarrow{+}}})}$.

\[claim:minimal\] Let $f$ be the minimal event in $E_p^{\pi}$ (assuming this set is nonempty). Then, $M,f\models\psi$ iff $M,f\models{\mathsf{Loop}({{\mathsf{min}~} {({{\xrightarrow{+}}}\cdot\pi^{-1})}})}$.

The right to left implication holds without any hypothesis. Conversely, assume $f{\xrightarrow{+}}f'={\llbracket {{{\mathsf{max}~} {\pi}}} \rrbracket}(f)$. Then, $M,f,f \models {{\xrightarrow{+}}}\cdot\pi^{-1}$, and $g = {\llbracket {{{\mathsf{min}~} {({{\xrightarrow{+}}}\cdot\pi^{-1})}}} \rrbracket}(f) {\leq_{\mathsf{proc}}}f$. This is illustrated in Figure \[fig:minimal\]. Moreover, $M,g \models {\mathop{\langle \pi \rangle}}$ and by minimality of $f$ in $E_p^{\pi}$, we conclude that $g = f$. (Claim \[claim:minimal\])

\(f) at (1,0) [$f$]{}; (fp) at (5,0) [$f'$]{}; (g) at (0,0) [$g$]{}; (eq) at (0.5,0) [$=$]{};

(1.2,-0.1) edge\[purple,thick,font=\] (3,-0.1) (3,-0.1) edge\[bend left,purple,thick,-&gt;,font=\] node [${{\mathsf{min}~} {({{\xrightarrow{+}}}\cdot\pi^{-1})}}$]{} (g);

\(f) edge\[-&gt;\] node [$+$]{} (fp);

\(f) edge\[bend left\] node [$\max \pi$]{} (fp);

\[claim:consecutive\] Let $e,f$ be consecutive events in $E_p^{\pi}$, i.e., $e,f\in E_p^{\pi}$ and $M,e,f\models{{\xrightarrow{\neg{\mathop{\langle \pi \rangle}}}}}$.

1.  If $M,e\not\models\psi$, then $[M,f\models\psi$ iff $M,f\models{\mathsf{Loop}({{\mathsf{min}~} {({{\xrightarrow{+}}}\cdot\pi^{-1})}})}]$.

2.  If $M,e\models\psi$, then $[M,f\not\models\psi$ iff $M,f\models{\mathsf{Loop}({{\mathsf{max}~} {\pi}})}\vee
          {\mathsf{Loop}({{\mathsf{max}~} {(({{\mathsf{max}~} {\pi}})\cdot{{\xrightarrow{\neg{\mathop{\langle \pi \rangle}}}})}}})}]$.

We show the two statements.

1.  Assume that $M,e\not\models\psi$. Again, the right to left implication holds without any hypothesis. Conversely, assume that $M,e\not\models\psi$ and $M,f\models\psi$, i.e., $e'={\llbracket {{{\mathsf{max}~} {\pi}}} \rrbracket}(e){\leq_{\mathsf{proc}}}e$ and $f {<_{\mathsf{proc}}}f'={\llbracket {{{\mathsf{max}~} {\pi}}} \rrbracket}(f)$. We have $M,f\models{\mathop{\langle {{\xrightarrow{+}}}\cdot\pi^{-1} \rangle}}$, and $g={\llbracket {{{\mathsf{min}~} {({{\xrightarrow{+}}}\cdot\pi^{-1})}}} \rrbracket}(f) {\leq_{\mathsf{proc}}}f$. Notice that $g\in E_p^{\pi}$, and $f {<_{\mathsf{proc}}}g'={\llbracket {{{\mathsf{max}~} {\pi}}} \rrbracket} (g)$. If $g {<_{\mathsf{proc}}}f$, we get $g{\leq_{\mathsf{proc}}}e$, and using Lemma \[lem:monotone\] (monotonicity), we obtain $g' {\leq_{\mathsf{proc}}}e' {\leq_{\mathsf{proc}}}e {<_{\mathsf{proc}}}f$, a contradiction. The situation is illustrated in Figure \[fig:consecutive1\]. Therefore, $g=f$ and $M,f\models{\mathsf{Loop}({{\mathsf{min}~} {({{\xrightarrow{+}}}\cdot\pi^{-1})}})}$.

    \(f) at (1,0) [$f$]{}; (fp) at (6.5,0) [$f'$]{}; (e) at (-2,0) [$e$]{}; (ep) at (-6,0) [$e'$]{};

    (notpsi) at (-2.1,-0.4) [$\neg\psi$]{}; (psi) at (1,-0.4) [$\psi$]{}; (g) at (-7,-0.1) [$g$]{}; (gp) at (5,-0.3) [$g'$]{};

    \(f) edge\[-&gt;\] node [$+$]{} (fp);

    \(e) edge\[-&gt;\] node [$\neg{\mathop{\langle \pi \rangle}}$]{} (f);

    (ep) edge\[-&gt;\] node [$\ast$]{} (e);

    \(f) edge\[bend left\] node [$\max \pi$]{} (fp);

    \(e) edge\[bend right=25\] node\[above\] [$\max \pi$]{} (ep);

    \(g) edge\[bend left=25\] node [$\max \pi$]{} (5,0);

    (1.2,-0.1) edge\[purple,thick,font=\] (3,-0.1) (3,-0.1) edge\[bend left=22,purple,thick,-&gt;,font=\] node [${{\mathsf{min}~} {({{\xrightarrow{+}}}\cdot\pi^{-1})}}$]{} (g);

2.  Assume that $M,e\models\psi$. The right to left implication holds easily: the first disjunct implies that $f'=f$ and the second disjunct implies $f'<f$. Conversely, assume that $M,e\models\psi$, $M,f\not\models\psi$ and $M,f\not\models{\mathsf{Loop}({{\mathsf{max}~} {\pi}})}$, i.e., $e{<_{\mathsf{proc}}}e'$ and $f' {<_{\mathsf{proc}}}f$. From Lemma \[lem:monotone\] we get $e'{\leq_{\mathsf{proc}}}f'$ and since $e,f$ are consecutive in $E_p^{\pi}$ we obtain $M,f',f\models{{\xrightarrow{\neg{\mathop{\langle \pi \rangle}}}}}$. Therefore, $M,f\models{\mathsf{Loop}(({{\mathsf{max}~} {\pi}})\cdot{\xrightarrow{\neg{\mathop{\langle \pi \rangle}}}})}
        \equiv{\mathsf{Loop}({{\mathsf{max}~} {(({{\mathsf{max}~} {\pi}})\cdot{\xrightarrow{\neg{\mathop{\langle \pi \rangle}}}})}})}$.

    \(e) at (1,0.3) [$e$]{}; (ep) at (4,0.3) [$e'$]{}; (fp) at (7,0.3) [$f'$]{}; (f) at (10,0.3) [$f$]{};

    \(a) at (1.1,-0.02) ; (b) at (9.9,-0.02) ;

    (notpsi) at (0.8,0.6) [$\psi$]{}; (psi) at (10.2,0.6) [$\neg\psi$]{};

    \(a) edge\[-&gt;\] node\[below\] [$\neg{\mathop{\langle \pi \rangle}}$]{} (b); (ep) edge\[-&gt;\] node [$\ast$]{} (fp); (e) edge\[-&gt;\] node [$+$]{} (ep); (fp) edge\[-&gt;\] node [$\neg{\mathop{\langle \pi \rangle}}$]{} (f);

    \(e) edge\[bend left\] node\[above\] [$\max \pi$]{} (ep);

    \(f) edge\[bend right\] node\[above\] [$\max \pi$]{} (fp);

This concludes the proof of the claim. (Claim \[claim:consecutive\]).

To conclude the proof of Theorem \[thm:PDLp-to-CFM\], consider the formulas $\varphi_1={\mathop{\langle \pi \rangle}}$, $\varphi_2={\mathsf{Loop}({{\mathsf{max}~} {\pi}})}$, $\varphi_3={\mathsf{Loop}({{\mathsf{min}~} {({{\xrightarrow{+}}}\cdot\pi^{-1})}})}$, and $\varphi_4={\mathsf{Loop}({{\mathsf{max}~} {(({{\mathsf{max}~} {\pi}})\cdot{\xrightarrow{\neg{\mathop{\langle \pi \rangle}}}})}})}$. By Lemmas \[lem:trad-loop-free\] and \[lem:det-loop\], we already have transducers ${\mathcal{A}}_{\varphi_i}$ for $i\in\{1,2,3,4\}$. We let ${\mathcal{A}}_\psi = {\mathcal{A}}\circ ({\mathcal{A}}_{\varphi_1} \times{\mathcal{A}}_{\varphi_2}
  \times{\mathcal{A}}_{\varphi_3}\times{\mathcal{A}}_{\varphi_4})$, where, at an event $f$ labeled $(b_1,b_2,b_3,b_4)$, the transducer ${\mathcal{A}}$ outputs $1$ if $b_3=1$ or if $(b_1,b_2,b_3,b_4)=(1,0,0,0)$ and the output was $1$ at the last event $e$ on the same process satisfying $\varphi_1$ (to do so, each process keeps in its state the output at the last event where $b_1$ was $1$), and $0$ otherwise.

Consider the formula $\varphi'$ over $\Sigma \times \{0,1\}$ obtained from $\varphi$ by replacing $\psi$ by $\bigvee_{a \in \Sigma} (a,1)$, and all event formulas $a$, with $a \in \Sigma$, by $(a,0) \lor (a,1)$. It contains fewer ${\mathsf{Loop}}$ operators than $\varphi$, so by induction hypothesis, we have a transducer ${{\mathcal{A}}_{\varphi'}}$ for $\varphi'$. We then let ${{\mathcal{A}}_{\varphi}} = {{\mathcal{A}}_{\varphi'}} \circ ({\mathcal{A}}_{\mathit{Id}} \times {{\mathcal{A}}_{\psi}})$, where ${\mathcal{A}}_{\mathit{Id}}$ is the transducer for the identity relation.

By Theorem \[thm:FO-to-PDLm-main\], every ${{\textup{FO}}[{\rightarrow},{\lhd},\le]}$ formula $\Phi(x)$ with a single free variable is equivalent to some ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ state formula, for which we obtain a transducer ${\mathcal{A}}_\Phi$ using Theorem \[thm:PDLp-to-CFM\]. It is easy to build from ${\mathcal{A}}_\Phi$ CFMs for the sentences $\forall x. \Phi(x)$ and $\exists x. \Phi(x)$. Closure of ${{\mathcal{L}}(\textup{CFM})}$ under union and intersection takes care of disjunction and conjunction.

Applications to Existentially Bounded MSCs {#sec:applications}
==========================================

Though the translation of ${\textup{EMSO}}$/${\textup{FO}}$ formulas into CFMs is interesting on its own, it allows us to obtain some difficult results for bounded CFMs as corollaries.

Existentially bounded MSCs
--------------------------

The first logical characterizations of communicating finite-state machines were obtained for classes of *bounded* MSCs. Intuitively, this corresponds to restricting the channel capacity. Bounded MSCs are defined in terms of linearizations. A *linearization* of a given MSC $M=(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ is a total order ${\preceq} \subseteq E \times
E$ such that ${\le} \subseteq {\preceq}$. For $B \in {\mathbb{N}}$, we call $\preceq$ $B$-bounded if, for all $g \in E$ and $(p,q) \in {\mathit{Ch}}$, $|\{(e,f) \in {{\lhd}} \cap (E_p \times E_q) \mid e \preceq g \prec f\}| \le B$. In other words, the number of pending messages in $(p,q)$ never exceeds $B$. There are (at least) two natural definitions of bounded MSCs: We call $M$ $\exists B$-bounded if $M$ has *some* $B$-bounded linearization. Accordingly, it is $\forall B$-bounded if *all* its linearizations are $B$-bounded.

The MSC from Figure \[fig:msc\] is $\exists 1$-bounded and $\forall
  4$-bounded. These bounds are tight: the MSC is not $\forall 3$-bounded, because the four send events for, say, channel $(p_1,p_3)$ can be scheduled before the first reception $g_0$.

As another example, consider the set of MSCs over two processes, $p$ and $q$, that consist of an arbitrary number of messages from $p$ to $q$ (and only messages from $p$ to $q$). This language is $\exists 1$-bounded (every message may be received right after it was sent), but it is not $\forall
  B$-bounded, no matter what $B$ is.

In the following, we will consider only $\exists B$-bounded MSCs. The set of $\exists B$-bounded MSCs is denoted by ${\mathbb{MSC}_{\exists B}({P},\Sigma)}$.

Below, we show the following results. First, for a given channel bound $B$, the set ${\mathbb{MSC}_{\exists B}({P},\Sigma)}$ is ${\textup{FO}}[{\rightarrow},{\lhd},\le]$-definable (essentially due to [@LohreyMuscholl04]). By Theorem \[thm:main\], we obtain [@GKM06 Proposition 5.14] stating that this set is recognized by some CFM. Second, we obtain [@GKM06 Proposition 5.3], a Kleene theorem for existentially bounded MSCs, as a corollary of Theorem \[thm:main\] in combination with a linearization normal form from [@ThiagarajanW02].

Let $M=(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ be some MSC, and $e_1 {\prec}e_2 \cdots {\prec}e_n$ a linearization of $M$. Given $e \in E$, we write ${\mathsf{type}}(e) = p$ if $e$ is an internal event on process $p$, ${\mathsf{type}}(e) = p!q$ if $e$ is a write on channel $(p,q)$, and ${\mathsf{type}}(e) = q?p$ if $e$ is a read from channel $(p,q)$. We associate with the linearization ${\preceq}$ a word ${M_{{\preceq}}}$ over the alphabet ${\Sigma_{\mathit{lin}}}= \Sigma \times (P \cup \{q?p, p!q \mid (p,q) \in {\mathit{Ch}}\})$. More precisely, we let ${M_{{\preceq}}} = a_1 \ldots a_n$ where $a_i = (\lambda \times {\mathsf{type}})(e_i)$. Note that $M$ can be retrieved from ${M_{{\preceq}}}$. We let ${\mathit{Lin}^B}(M) = \{{M_{{\preceq}}} \mid \text{${\preceq}$ is a $B$-bounded linearization of $M$}\}$.

\[EB-regular\] Let $B \in {\mathbb{N}}$ and $L$ be a set of $\exists B$-bounded MSCs. The following are equivalent:

1.  $L = {\mathbb{L}}({\mathcal{A}})$ for some CFM ${\mathcal{A}}$.

2.  $L = {\mathbb{L}}(\Phi)$ for some MSO formula $\Phi$.

3.  ${\mathit{Lin}^B}(L)$ is a regular language.

The proof given in [@GKM06] relies on the theory of Mazurkiewicz traces. Another major part of the proof is the construction of a CFM recognizing the set ${\mathbb{MSC}_{\exists B}({P},\Sigma)}$ of $\exists B$-bounded MSCs [@GKM06 Proposition 5.14]. We show that this CFM can in fact be obtained as a simple application of Theorem \[thm:main\]. Moreover, we give an alternative proof of $(3) \implies (1)$ (Section 5 in [@GKM06]).

A CFM for Existentially Bounded MSCs
------------------------------------

The set ${\mathbb{MSC}_{\exists B}({P},\Sigma)}$ of $\exists B$-bounded MSCs is in fact ${\textup{FO}}[{\lhd},{\rightarrow},\le]$-definable, and thus, we can apply Theorem \[thm:main\] to construct a CFM ${\mathcal{A}}_{\exists B}$ recognizing ${\mathbb{MSC}_{\exists B}({P},\Sigma)}$. We describe below a formula defining ${\mathbb{MSC}_{\exists B}({P},\Sigma)}$.

Let us first recall a characterization of $\exists B$-bounded MSCs. Let $M=(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ be an MSC. We define a relation ${\mathit{rev}_{B}} \subseteq E \times E$ which consists of the set of pairs $(f,g)$ such that $f$ is a receive event from some channel $(p,q)$ with corresponding send event $e {\lhd}f$, and $g$ is the $B$-th send on channel $(p,q)$ after event $e$. The relation ${\mathit{rev}_{B}}$ is illustrated in Figure \[fig:revb\] (represented by the dashed edges) for $B=1$ and an $\exists 1$-bounded MSC. It can be defined by the ${{\textup{PDL}_{\mathsf{sf}}}}[\cup]$ path formula $$\mathsf{rev}_B = \bigcup_{p\neq q} 
{{\lhd}_{p,q}^{-1}}\cdot \Big({\xrightarrow{\neg{\mathop{\langle {\lhd}_{p,q} \rangle}}}}\cdot
{\{{\mathop{\langle {\lhd}_{p,q} \rangle}}\}?} \Big)^B\,.$$ For completeness, let us also give a corresponding ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ formula: $$\begin{gathered}
  {\mathit{rev}_{B}}(x,y) := \exists z_0, z_1, \ldots, z_B.\
  z_0 {\lhd}x \land z_B = y \land
  \bigwedge_{1 \le i \le B} \exists x_i.\ z_i {\lhd}x_i \land x {\leq_{\mathsf{proc}}}x_i
   \\
  {}\land \bigwedge_{0 \le i < B-1} z_i {<_{\mathsf{proc}}}z_{i+1} \land
  \lnot (\exists z',x'.\ z_i {<_{\mathsf{proc}}}z' {<_{\mathsf{proc}}}z_{i+1} \land z' {\lhd}x' \land
  x {\leq_{\mathsf{proc}}}x') \, .\end{gathered}$$

$M$ is $\exists B$-bounded iff the relation $({<} \cup {\mathit{rev}_{B}})$ is acyclic.

Note that, if $({<} \cup {\mathit{rev}_{B}})$ contains a cycle, then it contains one of size at most $2|P|$. So $M$ is $\exists B$-bounded iff it satisfies the ${{\textup{PDL}_{\mathsf{sf}}}}[{\mathsf{Loop}},\cup]$ formula ${\xi}_{\exists B} = \neg{\mathop{\mathsf{E}\vphantom{a}}\nolimits}{\mathsf{Loop}(\mathsf{lt}_B)}$ where $$\mathsf{lt}_B = \bigcup_{2\leq n\leq |P|}
  \big( ({\lhd}\cup \mathsf{rev}_B)\cdot {{\xrightarrow{+}}} \big)^{n}
  \qquad\qquad {\lhd}= \bigcup_{p\neq q}{\lhd}_{p,q}\,.$$ Again, let us determine a corresponding ${\textup{FO}}[{\rightarrow},{\lhd},\le]$ formula: $$\Phi_{\exists B} =
  \bigwedge_{2 \le n \le 2|P|} \lnot \Big(
  \exists x_0, \ldots, x_{n}.\ x_0 = x_{n} \wedge
  \bigwedge_{0 \le i < n}
    x_i < x_{i+1} \lor {\mathit{rev}_{B}}(x_i,x_{i+1}) \Big) \, .$$

(p1) at (0,4) ; (p2) at (2,4) ; (p3) at (4,4) ; (p4) at (6,4) ; (p1) – (p2);(p2) – (p3);(p3) – (p4);

(q1) at (0,3) ; (q2) at (2,3) ; (q3) at (3,3) ; (q4) at (4,3) ; (q5) at (5,3) ; (q6) at (6,3) ; (q1) – (q2);(q2) – (q3);(q3) – (q4);(q4) – (q5);(q5) – (q6);

(r1) at (0,2) ; (r2) at (2,2) ; (r3) at (3,2) ; (r4) at (4,2) ; (r5) at (5,2) ; (r1) – (r2);(r2) – (r3);(r3) – (r4);(r4) – (r5); (s1) at (0,1) ; (s2) at (2,1) ; (s3) at (4,1) ; (s1) – (s2);(s2) – (s3);

(p1) – (q1);(p2) – (q2);(p3) – (q4);(p4) – (q6); (s1) – (r1);(s2) – (r2);(s3) – (r4); (q3) – (r3);(q5) – (r5);

(q1) – (p2);(q2) – (p3);(q4) – (p4); (r1) – (s2);(r2) – (s3); (r3) – (q5);

[background]{} [[ \[ create hullcoords/.code=[ in (hullcoord0) at (hullcoord); (hullcoord) at (hullcoord1); ]{}, create hullcoords \] ($(hullcoord1)!3mm!-90:(hullcoord0)$) in [1,...,]{} [ let 1 = ($(hullcoord\currentnode) - (hullcoord\previousnode)$), 1 = [atan2(1,1) + 90]{}, 2 = ($(hullcoord\nextnode) - (hullcoord\currentnode)$), 2 = [atan2(2,2) + 90]{}, = [Mod(2-1,360) - 360]{} in [arc \[start angle=1, delta angle=, radius=3mm\]]{} – ($(hullcoord\nextnode)!3mm!-90:(hullcoord\currentnode)$) ]{} ]{}; ]{}

[background]{} [[ \[ create hullcoords/.code=[ in (hullcoord0) at (hullcoord); (hullcoord) at (hullcoord1); ]{}, create hullcoords \] ($(hullcoord1)!3mm!-90:(hullcoord0)$) in [1,...,]{} [ let 1 = ($(hullcoord\currentnode) - (hullcoord\previousnode)$), 1 = [atan2(1,1) + 90]{}, 2 = ($(hullcoord\nextnode) - (hullcoord\currentnode)$), 2 = [atan2(2,2) + 90]{}, = [Mod(2-1,360) - 360]{} in [arc \[start angle=1, delta angle=, radius=3mm\]]{} – ($(hullcoord\nextnode)!3mm!-90:(hullcoord\currentnode)$) ]{} ]{}; ]{}

at (-1,4) [$p_1$]{}; at (-1,3) [$p_2$]{}; at (-1,2) [$p_3$]{}; at (-1,1) [$p_4$]{};

at (6.6,3.6) [${{\uparrow_B}}{e}$]{}; at (5.1,1.2) [${{\uparrow_B}}{f}$]{};

FO-definable Linearizations for Existentially Bounded MSCs
----------------------------------------------------------

We give a canonical $B$-bounded linearization of $\exists B$-bounded MSCs, adapted from [@ThiagarajanW02 Definition 13] where the definition was given for traces. We fix some total order $\sqsubseteq$ on $P$. Let $M=(E,{\rightarrow},{\lhd},{\mathit{loc}},\lambda)$ be an $\exists B$-bounded MSC, and let ${\le}_B = ({\le} \cup {\mathit{rev}_{B}})^\ast$ which is a partial order on $M$. Note that a linearization of $M$ is $B$-bounded iff it contains $\le_B$.

For $e \in E$, we define ${{\uparrow_B}}e = \{g \in E \mid e \le_B g\}$. Moreover, for $E' \subseteq E$, let ${\mathit{loc}}(E') = \{{\mathit{loc}}(e) \mid e \in E'\}$. Finally, given $e,f \in E$, let $e \parallel_B f$ if $e \not\le_B f$ and $f \not\le_B e$. We then define a relation ${{\prec_B}} \subseteq E \times E$ by $$\begin{array}{rcl}
e {\prec_B}f & \Longleftrightarrow~
\left(
\begin{array}{rl}
& e <_B f\\
\vee & e \parallel_B f ~\wedge~ \min ({{\mathit{loc}}({{\uparrow_B}}e \setminus {{\uparrow_B}}f)}) \sqsubset \min ({{\mathit{loc}}({{\uparrow_B}}f \setminus {{\uparrow_B}}e)})
\end{array}
\right).
\end{array}$$

Consider the MSC $M$ in Figure \[fig:revb\] and suppose $p_1 \sqsubset p_2 \sqsubset p_3 \sqsubset p_4$. We have ${{\mathit{loc}}({{\uparrow_B}}e \setminus {{\uparrow_B}}f)} = \{p_1,p_2\}$ and ${{\mathit{loc}}({{\uparrow_B}}f \setminus {{\uparrow_B}}e)} = \{p_3,p_4\}$. Since $p_1 \sqsubset p_3$, we obtain $e {\prec_B}f$.

The following result is due to [@ThiagarajanW02 Lemma 14]. It is stated there for traces, but the proof can be taken almost verbatim.

\[lem:linord\] The relation ${\prec_B}$ is a strict linear order on $E$.

Notice that, for all $e \neq f$, we have either $e {\prec_B}f$ or $f {\prec_B}e$, but not both. Indeed, for all $e \neq f$, we have ${{\mathit{loc}}({{\uparrow_B}}e \setminus {{\uparrow_B}}f)} \cap {{\mathit{loc}}({{\uparrow_B}}f \setminus {{\uparrow_B}}e)} =\emptyset$, and if $e \parallel f$, then the two sets are nonempty as ${\mathit{loc}}(e) \in {{\mathit{loc}}({{\uparrow_B}}e \setminus {{\uparrow_B}}f)}$ and ${\mathit{loc}}(f) \in {{\mathit{loc}}({{\uparrow_B}}f \setminus {{\uparrow_B}}e)}$.

It remains to show that ${\prec_B}$ is transitive. Let $e_1,e_2,e_3 \in E$ such that $e_1 {\prec_B}e_2 {\prec_B}e_3$. Note that $e_1,e_2,e_3$ are pairwise distinct. For distinct $i,j \in \{1,2,3\}$, fix an event $e_{ij}$ in ${{\uparrow_B}}{e_i} \setminus {{\uparrow_B}}{e_j}$ (if it exists) that is on the $\sqsubset$-minimal process in ${{\uparrow_B}}{e_i} \setminus {{\uparrow_B}}{e_j}$.

To prove $e_1 {\prec_B}e_3$, we distinguish several cases.

Case $e_1 <_B e_2 <_B e_3$:

:   As $<_B$ is transitive, we get $e_1 <_B e_3$.

Case $e_1 <_B e_2 \parallel_B e_3$:

:   This implies $e_3 \not \le_B e_1$. If $e_1 <_B e_3$, we are done. So suppose $e_1 \parallel_B e_3$. Since $e_2 {\prec_B}e_3$, we have ${{\mathit{loc}}(e_{23}) \sqsubset {\mathit{loc}}(e_{32})}$. From ${{\uparrow_B}}{e_2} \subseteq {{\uparrow_B}}{e_1}$, we deduce ${{\mathit{loc}}({{\uparrow_B}}e_2 \setminus {{\uparrow_B}}e_3)} \subseteq {{\mathit{loc}}({{\uparrow_B}}e_1 \setminus {{\uparrow_B}}e_3)}$. Thus, ${{\mathit{loc}}(e_{13}) \sqsubseteq {\mathit{loc}}(e_{23})}$. Similarly, ${{\mathit{loc}}(e_{32}) \sqsubseteq {\mathit{loc}}(e_{31})}$. We obtain ${\mathit{loc}}(e_{13}) \sqsubseteq {\mathit{loc}}(e_{23})
     \sqsubset {\mathit{loc}}(e_{32}) \sqsubseteq {\mathit{loc}}(e_{31})$.

Case $e_1 \parallel_B e_2 <_B e_3$:

:   This case is very similar to the previous one.

Case $e_1 \parallel_B e_2 \parallel_B e_3$:

:   Since $e_1 {\prec_B}e_2 {\prec_B}e_3$, we have ${{\mathit{loc}}(e_{12}) \sqsubset {\mathit{loc}}(e_{21})}$ and ${{\mathit{loc}}(e_{23}) \sqsubset {\mathit{loc}}(e_{32})}$. Suppose $e_1 \not \le_B e_3$ (otherwise, we are done). We have $e_3 \not \le_B e_1$, since $e_3 <_B e_1$ implies ${\mathit{loc}}(e_{32}) \sqsubseteq {\mathit{loc}}(e_{12})
     \sqsubset {\mathit{loc}}(e_{21}) \sqsubseteq {\mathit{loc}}(e_{23})$, a contradiction.

    So we can assume $e_1 \parallel_B e_3$. It remains to show ${{\mathit{loc}}(e_{13}) \sqsubset {\mathit{loc}}(e_{31})}$. First, one shows that $$\begin{aligned}
    {\mathit{loc}}(e_{13}) \sqsubseteq {\mathit{loc}}(e_{12})\,.\label{align:e12e13}\end{aligned}$$

    If $e_{12} \not\in {{\uparrow_B}}{e_3}$, then (\[align:e12e13\]) is immediate. So suppose $e_{12} \in {{\uparrow_B}}{e_3}$, i.e., $e_{12} \in {{\uparrow_B}}{e_3} \setminus {{\uparrow_B}}{e_2}$. Then, $$\begin{aligned}
    {\mathit{loc}}(e_{32}) \sqsubseteq {\mathit{loc}}(e_{12})\,.\label{align:e32e12}\end{aligned}$$ Let us consider two cases: If $e_{23} \in {{\uparrow_B}}{e_1}$, then ${\mathit{loc}}(e_{13}) \sqsubseteq {\mathit{loc}}(e_{23})$. Suppose, on the other hand, $e_{23} \not\in {{\uparrow_B}}{e_1}$. But this implies ${\mathit{loc}}(e_{21}) \sqsubseteq {\mathit{loc}}(e_{23})$. By (\[align:e32e12\]), we obtain ${\mathit{loc}}(e_{21}) \sqsubset {\mathit{loc}}(e_{12})$, which contradicts $e_1 {\prec_B}e_2$. We deduce that (\[align:e12e13\]) holds.

    To conclude the proof, we distinguish once more two cases:

    Case $e_{31} \in {{\uparrow_B}}{e_2}$:

    :   Then, ${\mathit{loc}}(e_{21}) \sqsubseteq {\mathit{loc}}(e_{31})$. Applying (\[align:e12e13\]), we obtain ${\mathit{loc}}(e_{13}) \sqsubset {\mathit{loc}}(e_{31})$.

    Case $e_{31} \not\in {{\uparrow_B}}{e_2}$:

    :   Then, ${\mathit{loc}}(e_{23}) \sqsubset {\mathit{loc}}(e_{32}) \sqsubseteq {\mathit{loc}}(e_{31})$. If $e_{23} \in {{\uparrow_B}}{e_1}$, then ${\mathit{loc}}(e_{13}) \sqsubseteq {\mathit{loc}}(e_{23}) \sqsubset {\mathit{loc}}(e_{31})$ and we are done. If $e_{23} \not\in {{\uparrow_B}}{e_1}$, then ${\mathit{loc}}(e_{21}) \sqsubseteq {\mathit{loc}}(e_{23})$, which implies ${\mathit{loc}}(e_{12}) \sqsubset {\mathit{loc}}(e_{31})$. By (\[align:e12e13\]), we obtain ${\mathit{loc}}(e_{13}) \sqsubset {\mathit{loc}}(e_{31})$.

This concludes the proof of Lemma \[lem:linord\].

Moreover, the reflexive closure ${\preceq_B}$ of ${\prec_B}$ contains $\le_B$, hence it is a $B$-bounded linearization of $M$. Finally, the relation ${\prec_B}$ is ${\textup{FO}}[{\rightarrow},{\lhd},\le]$-definable. Indeed, the strict partial order $<_B$ is ${\textup{FO}}[{\rightarrow},{\lhd},\le]$-definable since it can be expressed with the path formula $\mathsf{lt}_B$ given above. From its definition, we deduce that the relation ${\prec_B}$ is also ${\textup{FO}}[{\rightarrow},{\lhd},\le]$-definable.

We are now ready to give our alternative proof of the direction $(3) \implies (1)$ in Fact \[EB-regular\].

Let $L$ be a set of $\exists B$-bounded MSCs such that ${\mathit{Lin}^B}(L)$ is regular. There exists an EMSO sentence ${\Phi_{\mathit{lin}}}$ over ${\Sigma_{\mathit{lin}}}$-labeled words such that ${\mathit{Lin}^B}(L) = {\mathbb{L}}({\Phi_{\mathit{lin}}})$. Since ${\preceq_B}$ is ${\textup{FO}}[{\rightarrow},{\lhd},\le]$-definable, it is easy to translate ${\Phi_{\mathit{lin}}}$ into an ${\textup{EMSO}}[{\rightarrow},{\lhd},\le]$ formula $\Phi$ such that, for all $\exists B$-bounded MSC $M$, we have $M \models \Phi$ iff ${M_{{\preceq_B}}} \models {\Phi_{\mathit{lin}}}$. Let ${\mathcal{A}}$ be a CFM such that ${\mathbb{L}}({\mathcal{A}}) = {\mathbb{L}}(\Phi \land \Phi_{\exists B})$. Then, for all $M \in L$, $M$ is $\exists B$-bounded and ${M_{{\preceq_B}}} \models {\Phi_{\mathit{lin}}}$, hence $M\models\Phi \land \Phi_{\exists B}$, i.e., $M \in {\mathbb{L}}({\mathcal{A}})$. Conversely, if $M \in {\mathbb{L}}({\mathcal{A}})$, then $M$ is $\exists B$-bounded and ${\preceq_B}$ is a linearization of $M$. Moreover, ${M_{{\preceq_B}}} \in {\mathit{Lin}^B}(L)$, hence $M \in L$.

Conclusion {#sec:concl}
==========

In this paper, we showed that every ${\textup{FO}}[{\rightarrow},{\lhd},\leq]$ formula over MSCs is effectively equivalent to a CFM. As an intermediate step, we used a purely logical transformation of own interest, relating FO logic with a star-free fragment of PDL.

While star-free PDL constitutes a two-dimensional temporal logic over MSCs, we leave open whether there is a one-dimensional one, with a finite set of ${\textup{FO}}$-definable modalities, that is expressively complete for ${\textup{FO}}[{\rightarrow},{\lhd},\leq]$.

It will be worthwhile to see whether our techniques can be applied to other settings such as trees or Mazurkiewicz traces.

[^1]: It is open whether there is an equivalent one-dimensional one.

[^2]: Thanks to Sylvain Schmitz for pointing this out.

[^3]: In this case, $\Upsilon$ is a sentence whereas $x_1$ is free in the right hand side. Notice that $\equiv$ does not require the two formulas to have the same free variables.
