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 