Message-Passing Automata Are Expressively Equivalent to EMSO Logic

Abstract. We study the expressiveness of finite message-passing automata with a priori unbounded FIFO 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.

• Type: Conference
• Year: 2004
• Where: CONCUR
• Authors: Benedikt Bollig, Martin Leucker
• Keywords: CONCUR 2004, Message-passing Automata, Monadic Second-order Logic, finite Message-passing Automata