The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Benedikt Bollig, Martin Leucker
Message-Passing Automata are expressively equivalent to EMSO logic
2004-02
We study the expressiveness of finite message-passing automata with a
priori unbounded channels and show them to capture exactly the class
of MSC languages that are definable in existential monadic
second-order logic interpreted over MSCs. Moreover, we prove the
monadic quantifier-alternation hierarchy over MSCs to be infinite and
conclude that the class of MSC languages accepted by message-passing
automata is not closed under complement. Furthermore, we show that
satisfiability for (existential) monadic seconder-order logic over
MSCs is undecidable.
