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 