Formal Models of Communicating Systems
Subtitle: Languages, Automata, and Monadic Second-Order Logic (Texts in Theoretical Computer Science. An Eatcs Series)
Edition: 1 edition
Publisher: Springer
Published: October 10, 2006
Language: eng
Format: Hardcover
Number of pages: 182
ISBN-13: 9783540329220
Subjects: General Theory of Computing; Computers - General Information; Computers; Computer Books: Languages; Computer Science; Logic; Programming - Software Development; Asynchronous cellular automata; Automata; Communicating systems; Computers / Computer Science; Finite automata; Finite-state machines; Formal methods; Graphs; Mazurkiewicz traces; Message sequence charts; Software engineering
First sentence: Nowadays, electronic devices largely depend on complex hardware and software systems.
Description: 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.