  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.
