Muller message-passing automata and logics

We study nonterminating message-passing automata whose behavior is described by infinite message sequence charts. As a first result, we show that Muller, Büchi, and termination-detecting Muller acceptance are equivalent for these devices. To describe the expressive power of these automata, we give a logical characterization. More precisely, we show that they have the same expressive power as the existential fragment of a monadic second-order logic featuring a first-order quantifier to express that there are infinitely many elements satisfying some property. This result is based on Vinner’s extension of the classical Ehrenfeucht-Fraïssé game to cope with the infinity quantifier.