The following technical report is available from http://aib.informatik.rwth-aachen.de/:
Automata and Logics for Message Sequence Charts Benedikt Bollig AIB 2005-10
A message-passing automaton is an abstract model for the implementation of a distributed system whose components communicate via message exchange and thereby define a collection of communication scenarios called message sequence charts. In this thesis, we study several variants of message-passing automata in a unifying framework. We classify their expressiveness in terms of state-space properties, synchronization behavior, and acceptance mode and also compare them to algebraic characterizations of sets of message sequence charts, among them the classes of recognizable and rational languages.
We then focus on finite-state devices with global acceptance condition that communicate via a priori unbounded channels. We show them to be exactly as expressive as the existential fragment of monadic second-order logic over message sequence charts and to be strictly weaker than full monadic second-order logic. It turns out that message-passing automata cannot be complemented and that they cannot be determinized in general. Those results rely on a new proof technique, which allows to apply graph acceptors as introduced by Thomas to the framework of message sequence charts.