Formal Models of Communicating Systems

The close connection between automata and logic has ever been a fascinating subject of theoretical computer science. The origins of that area go back to B¨ uchi and Elgot, who showed at the beginning of the 60’s that formulas frommonadicsecond-orderlogicand?niteautomatahavethesameexpressive power. Since then, a large amount of research has been accomplished to extend those results to other settings such as in?nite words, trees, traces, and grids. The bene?ts of precise characterizations of state-based, operational automata modelsintermsofdescriptive logicalformalismsaretwofold.Ontheonehand, they allow us to derive algorithmic and logical properties of the model. On the other hand, from a software engineer’s perspective, fragments of monadic second-orderlogicmightbeusedtospecify thedesiredsystembehavior,which is then re?ected in an automata implementation. This book studies the relation between automata and monadic seco- order logic. In doing so, it focuses on classes of automata that describe the concurrent behavior of a distributed system. For example, we will bridge the gap between monadic second-order logic and channel systems, which c- municate via reliable or faulty ?fo (“?rst-in, ?rst-out”) queues. Moreover, we will study systems that synchronize when simultaneously accessing a common device. Due to the complexity of those communication paradigms, the formal treatment of related systems in terms of automata models and equivalent logical formalisms plays an important role in their synthesis and veri?cation.