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 